{"id":"arxiv:2608.06261","kind":"preprint","title":"Game Hopping in Lean","authors":["Stefan Dziembowski","Grzegorz Fabiański","Daniele Micciancio","Rafał Stefański"],"author_count":4,"year":2026,"published":"2026-08-06","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2608.06261","nct_id":null,"source_url":"https://arxiv.org/abs/2608.06261","archive_url":"https://space-kitty.com/papers/arxiv:2608.06261","updated":"2026-08-06","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2608.06261","abstract":"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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.CR","cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}