A proof that, in the lab's model of an access point running its admission module, sign-in memory stays bounded however many devices connect

In the lab's model of an access point with its admission module, proved in Lean and run in its Python reference code, the half-received sign-in data never exceeds 64 KiB, with at most 4 sign-ins live at once, however many sessions an attacker opens.

Quantum-resistant Wi-Fi sign-in messages are large and arrive in pieces. An access point (AP) must hold the pieces until a message is complete, before it knows who sent it. The lab proves that, in its model of an access point running the admission module, the total memory held this way never exceeds a fixed budget, however many devices an attacker makes connect at once.

What it shows

Wi-Fi sign-in is the handshake a device runs before it may use a network. Quantum-resistant versions carry keys and encrypted values large enough that they are split into pieces and put back together at the access point. Until a message is complete and checked, the access point is storing data from a device it does not know.

The danger is memory. A cap on each connection does not help if an attacker opens many connections at once. The evidence file's title makes the same point: the proof covers an unbounded number of sessions, and it shows that the cap on each session alone does not hold the bound.

The guarantee

The claim quoted above states the guarantee. Under any schedule an attacker chooses, with any number of sessions, the total amount of half-received sign-in data held by the access point never exceeds a fixed budget, and only a few sign-ins are live at once. The proof is checked by Lean, a proof assistant in which a machine checks every step.

Why it matters, and to whom

This is for makers of enterprise access points and controllers, and for Wi-Fi chip firmware teams, who are preparing for quantum-resistant sign-in. Filling a server's memory with half-finished connections is a classic way to deny service: the synchronize (SYN) flood against internet servers is the best-known case. Larger sign-in messages make the problem worse for Wi-Fi, so a proved bound is worth having.

The cost of a hard limit

A hard limit has a cost. When the limit on live sign-ins is reached, the next device must wait or be refused. As built, this module does not solve that: sign-ins that start and never finish can hold every slot and lock honest devices out. The bound caps memory, not availability.

How it was checked

The proof is written in Lean and checked by its kernel. The evidence file records the command that builds the proof and runs the module's own check, a run on a clean copy of the code, and its time: 6.2 seconds. The same record shows that the wire-level part of the check, which would run real Wi-Fi software over a simulated radio, was blocked on the computer used, because that part needs Linux.

Testing the check

The lab also tested the check by breaking it on purpose, and the evidence file describes each test. It doubled the per-session buffer in the Python code, so that the code no longer matched the proof, and it inserted a placeholder that marks a step of the key proof as unfinished. Both times the check failed. A third test halved the budget in both the code and the proof, and the check failed again; the lab does not count that one as decisive.

What it does not claim

• It does not claim that every access point, or the lab's full set of repairs, has this bound. The lab's scope note in the evidence file says the bound holds for an access point running this one admission module, not for the full set of repairs as shipped, and that it was measured on the Python reference path, with no Wi-Fi frame crossing a radio.

• It does not claim a measurement over the air. No Wi-Fi frame crosses a radio in this check, and no wire-level number is published.

• It does not claim that capping memory before sign-in is new. Linux has a setting for the most memory used to reassemble fragments of network data. Defences against SYN floods include SYN caches and SYN cookies. Current Wi-Fi sign-in under Wi-Fi Protected Access, version three (WPA3), called Simultaneous Authentication of Equals (SAE), can require an anti-clogging token instead of accepting new expensive attempts, as Díaz describes. Client puzzles are another published defence. What this result adds is a machine-checked proof of the bound for an access point running one admission module, over any number of sessions, for sign-in messages of quantum-resistant size.

How to reproduce it

The evidence file names the command that re-runs the check. It needs the lab's code at the commit named in the evidence file and the Lean toolchain.

Two tests would make the result stronger. First, wire the module into the full set of repairs and run the same proof there. Second, on a Linux machine, flood a simulated access point with real sign-ins and measure the memory it holds, then try an honest sign-in while the limit is full. The second test would measure the lock-out on real software as well as the memory.

Formal statement

$$\begin{array}{c}\forall \text{schedules}:\\ {\sum }_{s\in \mathrm{live}}\mathrm{held}(s)\le B\\ |\mathrm{live}|\le k\end{array}$$

Here B is the memory budget and k is the largest number of sign-ins held at once; the claim above gives both values. The schedule, meaning who connects when and how many sessions exist, is chosen by the attacker.

Prior art

• Linux kernel documentation, "IP Sysctl" (the fragment reassembly memory limit): a setting for the most memory used to reassemble fragments
• Wikipedia, "SYN flood": the classic attack on half-open connection state, and defences such as SYN caches and SYN cookies
• Óscar Alfonso Díaz, "WPA3 Denial of Service: SAE Resource Exhaustion": the anti-clogging mechanism in current Wi-Fi sign-in
• Noureddine, Fawaz, Basar and Sanders, "Revisiting Client Puzzles for State Exhaustion Attacks Resilience": defences against attacks that exhaust connection state
• Lemon, "Resisting SYN Flood DoS Attacks with a SYN Cache" (USENIX BSDCon): a fixed table that bounds the memory held for half-open connections

Evidence

• The evidence file for this result
• The published claim, with its limits
• All our published files, each with a fingerprint you can check

Related results across the group

• The chip netlist whose area and delay are published matches its design: a formal equivalence proof
• Searching for combined Wi‑Fi sign-in attacks without hints: a budgeted search and a complete one
• Attacks on multi-link Wi-Fi key handling: none accepted by the lab's rule, all accepted by a naive one
• The same result on VerifyCore Labs, our parent lab

All results from OrbitalProof · The OrbitalProof home page