Theorems & Bounds

1. Measured search

   $$\#\{\text{attacks tried}\}=8\text{rounds}\times 1400=11200,\#\{\text{attacks that got through}\}=0$$

   $$\#\{\text{attacks tried}\}=8\text{rounds}\times 1400=11200,$$$$\#\{\text{attacks that got through}\}=0$$

   11,200 attacks on our models, none got through

   An automated attacker, given no starting attacks, combined known attack moves up to ten steps deep against ten quantum-safe Wi-Fi sign-in designs as we model them. It ran in eight rounds, as the formula counts, and our checker, unchanged throughout, found no attack that got through. To show the search can find a real attack, we re-opened a known Wi-Fi flaw in one design, KRACK (a published attack that tricks a device into reusing a key), and the same search caught it. The limit: this is a search on a fixed budget, run on software models of our own designs, not a proof that no attack exists.

   The file it was checked fromThe same result on VerifyCore Labs

2. Checked by the Lean 4 kernel

   $$\forall \sigma \in {\mathrm{Ev}}^{\ast }:{\mathrm{mem}}_{\mathrm{AP}}({\mathrm{run}}_{G,c}(\sigma ))\le G=64\mathrm{KiB}(c=16\mathrm{KiB},N_{\max }=4);$$$$\forall B\exists \sigma :{\mathrm{mem}}_{\mathrm{AP}}({\mathrm{run}}_c^{\mathrm{no}\mathrm{quota}}(\sigma ))>B$$

   $$\forall \sigma \in {\mathrm{Ev}}^{\ast }:{\mathrm{mem}}_{\mathrm{AP}}({\mathrm{run}}_{G,c}(\sigma ))\le G=64\mathrm{KiB}$$$$(c=16\mathrm{KiB},N_{\max }=4);$$$$\forall B\exists \sigma :{\mathrm{mem}}_{\mathrm{AP}}({\mathrm{run}}_c^{\mathrm{no}\mathrm{quota}}(\sigma ))>B$$

   The access-point memory ceiling

   In our model of the admission-control module, no attacker schedule, however many sessions it opens, can push the access point past its 64 KiB pre-authentication budget. Capping each session alone is not enough: without the access-point quota, every budget can be broken. In our design the access point reserves four 16 KiB slots and refuses a fifth sign-in, which is also its weakness as built: four sign-ins that start and never finish hold every slot and lock other devices out. We have not measured a real access point, and the bound is for our reference module, not for every mechanism in the full design.

   The file it was checked fromThe same result on VerifyCore Labs

3. Measured check

   $$\#\{\text{test cases passed}\}=255,$$$$\#\{\text{key-check cases not exercised}\}=60,$$$$\text{ML-DSA: key generation only}$$

   $$\#\{\text{test cases passed}\}=255,$$$$\#\{\text{key-check cases not exercised}\}=60,$$$$\text{ML-DSA: key generation only}$$

   The standard's own test cases, run on the library we build on

   Run against the open-source liboqs library, NIST's own test cases give 255 pass, 60 not exercised, because the library offers no way to run those. For the signature algorithm only key generation is checked, not signing or verifying. This checks a library we did not write; it is not one of our own results.

   The file it was checked from

4. Computed bound

   $$\mathbb{E}[R]\ge 1+{\epsilon }_{\mathrm{SP}}\approx 1.000;\text{guard }1.48\text{vs fixed }4.00\Rightarrow \frac{4.00-1.48}{4.00-1.000}=84.0\%$$

   $$\mathbb{E}[R]\ge 1+{\epsilon }_{\mathrm{SP}}\approx 1.000;$$$$\text{guard }1.48\text{vs fixed }4.00\Rightarrow \frac{4.00-1.48}{4.00-1.000}=84.0\%$$

   Retransmissions against a computed floor

   A radio link that loses data resends it in rounds. In a modelled noisy channel at one signal level, with a budget of four rounds and a receiver that only answers yes or no after each round, no scheme that never wrongly confirms receipt can average fewer rounds than a computed lower limit allows. Our guard, the rule we wrote for when to stop resending, closes 84% of the gap in average rounds between always using all four rounds and that limit. The computed limit is close to a single round, so this mostly measures the guard against always using every round; it is not a claim that the guard approaches a physical limit.

   The file it was checked from

5. Checked by the Lean 4 kernel

   $$\text{recover first-copy path over a window }w⟹|{\mathcal{S}}_w|\ge 3^w>2^w;$$$$w=2:9>4$$

   $$\text{recover first-copy path over a window }w$$$$⟹|{\mathcal{S}}_w|\ge 3^w>2^w;$$$$w=2:9>4$$

   What a redundant-path receiver must remember

   Some Ethernet links send every frame along two paths and the receiver drops the duplicate (IEEE 802.1CB). A receiver that must also report which path delivered the first copy needs $3^w$ states for a window of w frames, strictly more than the $2^w$-state bitmap the standard describes. No clever encoding fits it in the bitmap.

   The file it was checked from

6. Measured check

   $$(|pk|,|ct|,|sk|{)}_{\text{Round-3 Kyber}}=(|ek|,|ct|,|dk|{)}_{\text{ML-KEM-768}}=(1184,1088,2400)\text{bytes}$$

   $$(|pk|,|ct|,|sk|{)}_{\text{Round-3 Kyber}}=(|ek|,|ct|,|dk|{)}_{\text{ML-KEM-768}}=(1184,1088,2400)\text{bytes}$$

   Sizes cannot tell round-3 Kyber from ML-KEM

   ML-KEM is the final US standard for quantum-safe key exchange; round-3 Kyber is the draft it grew out of, and their keys and ciphertexts are the same sizes, so sizes cannot tell them apart. We ran NIST's key-generation tests for ML-KEM-768 on a public Kyber repository and all five matched, although its README calls the code round 3. Only key generation was run, and nothing here says that repository's cryptography is wrong.

   The file it was checked from

Results with their own page · The OrbitalProof home page