Search papers, labs, and topics across Lattice.
HOPSCOTCH is a Lean 4 framework designed for mechanizing game-based cryptographic proofs, leveraging a shallow embedding to integrate seamlessly with the Lean ecosystem and existing mathematical theories. The framework facilitates the construction and automation of proofs by representing game-hopping arguments as explicit formal objects, which enhances their inspectability and usability. A general computational soundness theorem is established, providing concrete bounds on the advantage of distinguishers, and the framework is exemplified through formalized proofs of various cryptographic security definitions, including the IND-CCA security of encrypt-then-MAC and the GGM pseudorandom-function construction.
Game-hopping proofs can now be mechanized in Lean with unprecedented clarity and integration, enabling more robust cryptographic security verification.
We present HOPSCOTCH, a Lean 4 framework for mechanizing computationally sound, game-based cryptographic proofs. Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm. HOPSCOTCH uses a shallow embedding: oracles and reductions are ordinary Lean definitions, enabling direct integration with the full Lean ecosystem, including general mathematical theories from Mathlib, such as finite-group theory. A game-hopping proof in HOPSCOTCH is represented as an explicit formal object whose constructors correspond to the standard steps of a game-hopping argument, making proofs easier to construct, automate, and inspect. We prove a general computational soundness theorem that interprets these proof objects by constructing reductions against the assumptions they use and deriving a concrete bound on the advantage of any distinguisher. Observational equivalence between oracles is established using a state-abstraction methodology: a simple yet powerful approach that supports transformations such as adding or forgetting state and replacing eager sampling with lazy sampling. We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction. To the best of our knowledge, the last is the first mechanized proof of GGM for non-constant depth.
