HOPSCOTCH Mechanizes Game-Hopping Crypto Proofs in Lean 4, Including the First Machine Proof of GGM at Non-Constant Depth

arXiv 2608.06261·low signalXBlueskyLinkedInCopy link

arXiv 2608.06261 (Aug 6) presents HOPSCOTCH, a Lean 4 framework for computationally sound game-based cryptographic proofs where oracles and reductions are ordinary Lean definitions, giving direct access to Mathlib's finite-group theory. A game-hopping proof becomes an explicit formal object whose constructors mirror the standard argument steps, and a general soundness theorem interprets those objects into reductions with concrete distinguisher-advantage bounds. Formalized examples include IND-CCA for encrypt-then-MAC, ElGamal from DDH, one-time secrecy to public-key IND-CPA, and the GGM PRF construction — the last being, to the authors' knowledge, the first mechanized GGM proof for non-constant depth.