sub-MTU XMSS formal proof of classical security in ROM

[TomWambsgans]

Lean4 proof (using VCVio) of 127 bits classical security (strong unforgeability), in the ROM, for the sub-MTU XMSS instance we use.

• The XMSS spec is ./doc/xmss/main.tex
• The lean4 statement is in ./formal/xmss/XmssSecurity/Statement.lean (around 500 LoC)
• The proof is arround 40K Loc

[alexanderlhicks]

Retrospective adversarial review

Disclosure: this review was prepared with assistance from an OpenAI Codex agent. The agent was explicitly asked not to trust or merely restate the earlier audit, but to justify and illustrate every issue, try to falsify each finding, search for omissions, distinguish fixed, retracted, pre-existing, and newly introduced issues, and explain Lean and VCVio mechanisms for a reader who knows leanVM and XMSS better than Lean. The review compared the earlier and final PR heads, built the Lean project, inspected the elaborated theorem and axiom footprint, traced the pinned VCVio query-bound and logging definitions, checked the paper and implementation against the formal game, ran targeted Rust and recursive-aggregation tests, and reproduced the malformed-signature panic. The findings below were rechecked against the merged tree at f5d6e5040d666981005371742a6f21640ce865a1.

The central result holds up. The public proposition remained unchanged through the final proof refactor, all 143 local proof modules are reachable from the root, and the root theorem depends only on propext, Classical.choice, and Quot.sound. I found no sorry, unsafe proof escape, VCVio semantic error, or arithmetic error that invalidates the stated Lean proposition. The new README proof-spine map is also a useful improvement.

The qualifications below concern the public claim surface and the boundary between the proved ideal scheme and leanVM's deployed system. I have separated small documentation changes from larger refinement and composition results that can reasonably be follow-up work.

1. What the checked 127-bit theorem means, and where the usual Winternitz loss went

HasHashQueryBound applies VCVio's structural IsQueryBoundP to the complete gameCore. A matching hash query decrements the budget, and every possible response continuation must satisfy the residual bound. Thus q includes key generation, adversarial hashing, signing, and final verification. Key generation alone contributes

Q_KG = 296 * 2^32 - 1

hash queries.

The proof establishes the sharper intermediate inequality

forgeAdvantage
  <= ((q - Q_KG) + 42) / 2^128
     + (q - Q_KG) / 2^128

before CappedExactFirstLane.lean weakens it to q / 2^127. I compiled a temporary root-level wrapper from the existing first-lane and second-lane theorems, so exporting this inequality requires no new reduction.

This also puts the informal 127.3-bit estimate in context. Dividing the sharp bound by the total budget gives a coefficient

2 - (2 Q_KG - 42) / q

in front of 2^-128. For example, fixing q = 5 Q_KG gives 128 - log2(1.6) = 127.3219 normalized bits. But the theorem quantifies over every q, and the coefficient tends to two as q grows. The currently proved uniform corollary therefore tends to exactly 127 bits. A uniform 127.3-bit theorem would require either an upper bound on q or a tighter probability inequality. This is consistent with the chat describing 127.3 as an intuition-based estimate, not a Lean theorem.

The formal proof appears to avoid the standard Winternitz chain-position loss in a principled ROM-specific way. A standard-model proof guesses the relevant epoch, chain, and chain position, then pays a 2^w hybrid to replace an internal chain value by a uniform value. Here the proof presamples the complete global chain-output table, proves distributional equivalence with key generation, transports it through a causal simulation, and monitors the first reveal or hit across all relevant positions. The first lane is charged by post-key-generation hazard queries plus 42 final coordinate probes, not by guessing and hybridizing over eight chain positions. The second lane covers encoding prehits and structural collisions. Unioning the two 128-bit lanes causes the final one-bit loss.

This does not contradict the standard-model analysis because the ROM supplies the global independence and programming structure used by the coupling. Please expose the sharp theorem and add a human-readable proof sketch explaining the global table, causal reveal monitor, absence of the chain-position hybrid, additive 42 probes, and final two-lane union. If a conventional attacker-resource claim is wanted, it should cancel the fixed key-generation cost and show other honest work explicitly rather than calling the total-game q attacker work.

2. The ideal full key is not yet refined to the seeded restricted Rust key

sampleSecret and precomputedKeygen sample the public parameter and all WOTS starts uniformly and compute the complete tree through the random oracle. Rust derives the public parameter, WOTS starts, and out-of-range filler nodes from one keyed-BLAKE2s seed under separate domains and constructs only an activation range.

Those are reasonable implementation choices, but they are not identical distributions. Relating them requires a PRF hybrid with explicit computational resources, plus a separate sparse-tree and activation-range refinement. This is especially important because the Lean adversary is otherwise arbitrary subject to an oracle-query bound, while a keyed-BLAKE2s PRF claim requires a computational resource model.

Please qualify the seed and restricted-key remarks, for example:

A seeded or restricted implementation is expected to be related to this ideal scheme through additional PRF and sparse-tree refinement arguments. Those arguments, and their concrete losses and resource assumptions, are not established by the present theorem.

The full hybrid can be tracked as follow-up work.

3. withLogging restricts admissible transcripts but does not enforce epoch consumption

The paper says that Sign rejects an already-used epoch and marks a fresh epoch used. The formal signer and Rust key do not implement that state transition.

QueryImpl.withLogging adds a WriterT layer. It appends each request and returned response to a log; it does not hold a consumed-epoch set or reject a request. gameCore checks SigningTranscript.Valid only after the adversary finishes. A repeated request can therefore receive a second signature and then make the completed execution lose. This is a sound representation of a game restricted to unique-epoch queries, but not a proof that the signer enforces that restriction.

Please distinguish those statements in the paper and README. A complete implementation result needs a persistent atomic signer state machine, with concurrency, restart, rollback, activation-range, and recovery behavior specified. It should also decide whether a capped attempt returning none consumes the epoch.

4. Export successful-signing correctness and align retry behavior

Strong unforgeability does not imply that signing works: an always-failing signer can be unforgeable vacuously. The proof contains a useful internal result, verifyFromCache_signWithEncoding, but the root exports no public correctness or availability theorem.

Please expose a theorem saying that a some signature produced by key generation and signing in the shared-oracle execution verifies for the same key, epoch, and message. The Lean signer stops after 2^23 failed encodings, while Rust loops until success. Please align or explicitly document that behavior. The < 2^-410 exhaustion estimate is numerically plausible, but remains prose until the sampling-with-replacement and consistent-cache semantics are proved.

5. State the aggregation boundary explicitly

The theorem gives one adversary one typed public key and asks for one typed forgery. It does not model a signer list, externally fixed common statement, zkDSL execution, recursive children, carried fixed-polynomial claims, native root discharge, or SNARK knowledge soundness. This is an expected scope boundary, not a defect in the single-key theorem, but aggregation is the repository's deployment goal.

Please add a short "Not proved here" paragraph to the formal README. The eventual composition theorem should say that aggregate acceptance for an externally supplied message, epoch, and authorized key set implies coverage by valid raw signatures, except with an explicit multi-user XMSS loss or a failure of the SNARK and deferred-claim assumptions. It should make verify_against the application acceptance boundary.

6. Record the remaining byte-level refinement boundary

The formalization already defines little-endian conversion, all four tweak domains, and exact random-oracle input bytes. That is valuable. The missing bridge is from Rust parsing, bincode serialization, and concrete BLAKE2s calls to the typed PublicKey, Signature, and verifier definitions.

There is currently no public-key or signature wire parser, canonical-serialization theorem, or executable relation to the Rust, Python, and zkDSL acceptance paths. Typed signature equality in the strong-forgery game is not itself a byte-level canonicality result.

Please document this boundary and track round-trip, canonicality, and verifier-refinement theorems. Shared vectors for tweak bytes, encoding acceptance and rejection, WOTS recovery, both Merkle child orders, public keys, signatures, and external aggregate statement binding would be a useful first increment across Lean, Rust, Python, and zkDSL.

7. Recast the quantum claim as open work

The Lean proof is classical. It does not establish NIST category 1 or approximately 64 quantum bits for this target-sum construction, and FIPS 205 or WOTS+ analyses do not automatically transfer to a different encoding.

There is also a missing condition in the displayed QROM loss discussion. For q_s > 0, making

(3 q_s / 2) * sqrt((q_H + q_s) / 2^192) <= 2^-32

requires

q_H + q_s <= 2^130 / (9 q_s^2).

The condition q_s <= 2^32 alone is insufficient. The first term, 8(q_s + q_H)^2 / 2^128, reaches one at q_s + q_H = 2^62.5, so a numerical claim needs the complete query regime.

Suggested replacement:

This work proves only classical ROM security for the ideal scheme. Establishing a QROM bound for the target-sum encoding, with explicit signing and quantum-query limits, remains open.

8. Repair the remaining paper quantifiers and proof pointer

The new README proof map is a genuine repair. The paper still defines maxima over adversaries and q, although a maximizer need not exist and the eligible adversary class is empty below the mandatory key-generation cost. The Lean statement avoids both problems with a universal implication. Please state it directly, or use suprema with an explicit empty-class convention.

The paper also points to Statement.lean as the proof, although that file intentionally contains only definitions. Please point to formal/xmss/XmssSecurity.lean for the root and XmssSecurity/Proof/ for the derivation. Replacing the remaining TODO with the two-lane proof sketch described above would also answer the natural cryptographic question about the absent standard-model Winternitz loss.

Correction to the earlier review

I withdraw the earlier concern about the root axiom guard. #print axioms follows the named theorem's transitive proof dependencies, which are exactly the declarations relevant to its logical trust footprint. In a controlled check, a theorem proved with native_decide reported a compiler-evaluation axiom, so the existing #guard_msgs would fail if such a dependency entered this theorem. An unused declaration elsewhere is not part of the proof and cannot affect it. No author action is requested on this point.

Current-main follow-ups filed separately

• #14: build the XMSS Lean formalization as a required CI check
• #15: return an error for malformed raw XMSS aggregation input instead of panicking
• #16: make the exclusive MAX_KEYS contract consistent
• #17: restore direct XMSS hash-layout and deterministic-key regression coverage

None of those four is attributed to the final formal-proof refactor: #14 is repository process, #15 and #16 are pre-existing implementation issues, and #17 was introduced by later mainline cleanup work.