What this proves, and what it does not¶
The conceptual guide. If you read one page beyond the front door, read this one — it is the argument the tools implement, and the limits they cannot cross.
1. The size change is structural¶
An X25519 key share is 32 bytes and fits in a single frame. A category-3 post-quantum credential does not:
| Component | Bytes |
|---|---|
| ML-KEM-768 public key | 1,184 |
| ML-KEM-768 ciphertext | 1,088 |
| ML-DSA-65 public key | 1,952 |
| ML-DSA-65 signature | 3,309 |
| Total | 7,533 |
Reproduce: pqc-sizes credential --kem ML-KEM-768 --sig ML-DSA-65.
On an 802.11 management-frame path (384 usable bytes) that is 20 fragments. A receiver must therefore hold partial, attacker-influenced state across twenty frames before it can authenticate any of it.
Pre-quantum, authentication happened before meaningful state accumulated. That ordering is what made a decade of state-machine hardening stick. The size change inverts it.
2. Exposure is retention × concurrency¶
The instinctive fix is a per-object bound: "no single reassembly may exceed N bytes." That is the wrong shape. An attacker does not need one large object; they need many concurrent ones.
So the real quantity is retention × concurrency, and a cap has two
boundaries:
floor = the largest legitimate object you must accept
ceiling = memory budget ÷ worst-case concurrent contexts
- Choose a cap below the floor and you reject honest peers.
- Choose one above the ceiling and concurrent sessions exhaust the budget.
3. The interval can be empty¶
This is the part that surprises people. floor and ceiling are independent —
one comes from the protocol, the other from the deployment. Nothing guarantees
floor ≤ ceiling.
When floor > ceiling, no capacity cap is both feasible and safe. Not "pick
carefully": there is no value to pick.
$ pqc-sizes window --largest-object 12000 --budget 32768 --concurrency 3
EMPTY WINDOW: floor 12,000 B > ceiling 10,922 B (short by 1,078 B). No
capacity cap is both feasible and safe. Raise the budget to at least 36,000 B,
reduce concurrency to at most 2, or choose a smaller credential.
That is a design answer, available before any code is written, and it is arithmetic — which is why it can be checked in five seconds and gated in CI.
The same fact read the other way gives you a device's concurrency limit:
pqc-sizes sweep shows where the window collapses, so the limit is derived
rather than discovered in the field.
4. The bound, and why it is checked three times¶
Given a gate that admits a fragment only when the result stays within CAP,
residency is bounded by CAP for every fragment sequence. The ungated
datapath is unbounded.
That is a theorem, and it is checked in three independent systems:
| System | Trusted base | Reproduce |
|---|---|---|
| Lean 4 | the kernel alone — no mathlib, no imports | ./verify.sh |
| Yosys | a SAT solver over synthesizable RTL, unbounded k-induction | ./verify.sh |
| Integer C | 123 lines you can audit over coffee, no solver | make check |
Plus a demonstration on emulated ARMv7-M: the unrepaired design requests 1,562× the device's RAM and dies; the bounded one completes at a peak heap of 16,896 bytes, byte-identical under benign and attack traffic.
Redundancy is deliberate. A bound only one toolchain believes is a bound you are trusting that toolchain for.
5. Memory exhaustion is 1 of 39¶
Sizing tells you the buffer is safe. It says nothing about downgrade binding, key
reinstallation, fragment splicing, roaming forward secrecy or multi-link key
separation — all of which the size change reopens.
pqc-mfb enumerates 39 failure
families over 322 executed cases.
What none of this proves¶
This section matters more than the rest of the page.
Not that your implementation matches the model. Every theorem here is about a model: a four-line recurrence in Lean, a small Verilog module, a modelled state machine in the benchmark. Whether your code refines any of them is a separate obligation none of these tools discharge.
Not that a safe cap is enforced. A non-empty window means a safe cap exists. Nothing here inspects your code to check you apply it.
Not a security certification. A perfect benchmark score means 312 modelled cases handled. It is a signal, not an assurance, and the model inherits its own blind spots — a failure mode it cannot express is simply absent.
Not a vulnerability disclosure. Where a case names a published failure of similar shape, that is a pointer for the reader. It is not a claim that the case reproduces that CVE, and it asserts nothing about any vendor's product.
Not exhaustive. The 39 families are what one effort modelled. Absence from the list says nothing about the protocol.
Not peer-reviewed. Machine-checked is a different and narrower thing than reviewed.
Not a repair. The whole portfolio detects and measures. Closing the families is a separate closed codebase.
Why the tools refuse¶
Several tools decline to answer rather than answer badly. That is deliberate, and each case is a defect that was found and fixed:
farkas-checkreturnsREFUSEon arithmetic overflow. It once reported a certificate claimingx ≤ 2^62impliesx ≤ 1/4as VALID, because the comparison computed2^62 × 4and wrapped to zero. A false accept of a false implication is the worst thing a verifier can do.farkas-checkreturnsABSTAINfor a goal with all-zero coefficients.0·x ≤ dholds regardless of state, so verifying it establishes nothing.pqc-mfbreturnsINCOMPLETE, neverPASS, for an unanswered case. An empty submission once scored PASS at 0% coverage.pqc-sizes-jsthrows above2^53. IEEE doubles lose exactness there, and it once reported a higher safe concurrency than exact arithmetic allows.
A tool that answers every question is not more useful than one that declines the ones it cannot settle. It is less trustworthy.