sub-MTU XMSS formal proof of classical security in ROM - #10
Open
TomWambsgans wants to merge 403 commits into
Open
sub-MTU XMSS formal proof of classical security in ROM#10TomWambsgans wants to merge 403 commits into
TomWambsgans wants to merge 403 commits into
Conversation
Define each algorithm once: the precomputed secret key stores its tables as evalWithAnswerFn replays of the statement's own chainWalk and treeNode against the recorded keygen cache, and the CacheView, CacheReplay and Wots.walk mirrors move behind the theorem into the proof. decodeDigest becomes a computable inline check of the two padding bits and the target sum, truncateHash a direct extractLsb', the transcript predicates get Decidable instances so gameCore is a plain do-block, and Adversary drops its unused scheme parameter. The statement shrinks from 713 to 599 lines; bridge lemmas in CacheReplayEval connect the replay formulation to the mirrors, and the full build stays green with the standard axiom footprint. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The reviewer-facing statement is now one 557-line module, XmssSecurity/Statement.lean, holding the instance, the algorithms, and the security experiment in dependency order; Statement/Spec.lean and Statement/Algorithms.lean are gone. Proof files that imported the Spec submodule now import the full statement, so the three by_cases on undecidable propositions in WotsExtraction become classical case splits to keep typeclass search away from the larger instance environment. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
HasClassicalSecurityBits becomes a plain forall over budgets and adversaries, replacing the forgeAtMost supremum. The random-oracle semantics is the single implementation romImpl, defined once in the statement and used directly by the proof in place of its duplicate xmssRomImpl, so forgeAdvantage is one simulateQ line and the ProbCompRuntime bundle is gone. forwardOracles forwards queries by liftM, the two Concrete blocks merge, and precomputedAuthenticationPath uses castSucc instead of an inline tactic. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
fieldBytes writes the 16 specification tweak bytes as tag || position || epoch || 0^7 with each field little endian, replacing the Tweak bit vector, encodeTweak, and hashDomainTweak, so the layout compares byte by byte against doc/xmss with no append-order reversal to undo. HashInputLemmas proves tweak injectivity by splitting the byte list at the field lengths, which is shorter than the previous BitVec extraction proofs. The byte layout is unchanged: the old extract lemmas placed tag at bits 0-7, position at 8-39, and epoch at 40-71, whose little-endian serialization is exactly these bytes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Scheme.sign takes only the secret key, the epoch, and the message: the signer never reads the public key, so the argument and the _publicKey binders it forced are gone from signingOracle, precomputedCappedSign, and the proof's lazy signers. The statement's import block shrinks from twelve lines to the three VCVio modules it visibly uses (LoggingOracle, RandomOracle.Simulation, QueryBound); the rest were transitive, and EncodingLemmas now owns the Mathlib.Data.BitVec import it needs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Lean4 proof (using VCVio) of 127 bits classical security (strong unforgeability), in the ROM, for the sub-MTU XMSS instance we use.