Game Hopping in Lean

• URL: http://arxiv.org/abs/2608.06261v1
• Date: Thu, 06 Aug 2026 16:52:16 GMT
• Title: Game Hopping in Lean
• Abstract summary: We present HOPSCOTCH, a Lean 4 framework for mechanizing sound, game-based cryptographic proofs.<n>Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm.<n>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.
• Score: 5.623680633781937
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt [8.739112129971362]
  Large language models (LLMs) have recently made substantial progress in formal proof generation.<n> Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds.<n>This paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation.
  arXiv  Detail & Related papers  (2026-09-05T18:49:38Z)
• BioZKFHE: Scalable Encrypted Biometric Identification via Verifiable Homomorphic Similarity Evaluation [20.524348401618735]
  BioZKFHE is a framework for scalable encrypted biometric identification via verifiable homomorphic similarity evaluation.<n>It combines BGV homomorphic computation with committee-mediated proof opening/decryption and smart-contract verification of opened proof batches.<n>Experiments on FaceNet and MobileFaceNet show near-lossless biometric utility, up to 67 percent encrypted-storage reduction, and about 22 to 44 seconds end-to-end proof-verified runtime.
  arXiv  Detail & Related papers  (2026-07-24T08:08:54Z)
• ShannonProver: Towards Automating Formal Cryptographic Proofs [14.266077895853288]
  ShannonProver is an agentic framework for automating cryptographic proofs.<n>It targets the setting in which a cryptographer provides the security model and a decomposition of the target theorem into Prov-level proof obligations.<n>We show that ShannonProver can automate substantial portions of cryptographic proof engineering for case studies.
  arXiv  Detail & Related papers  (2026-07-03T00:50:51Z)
• Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
  System extracts tactic usage distributions across 27 top-level areas of Mathlib.<n>It computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area.<n>It matches source and target proof states via GPU-accelerated NP-hard analogy.
  arXiv  Detail & Related papers  (2026-04-19T03:27:16Z)
• Anamorphic Encryption with CCA Security: A Standard Model Construction [32.95661036494699]
  Anamorphic encryption serves as a vital tool for covert communication, maintaining secrecy even during post-compromise scenarios.<n>We formalize the Anamorphic Key Encapsulation Mechanism (AKEM), encompassing both Public-Key (PKAKEM) and Symmetric-Key (SKAKEM) variants.<n>We provide a rigorous formal proof in the standard model, demonstrating resilience against a "dictator" who controls the decapsulation key.
  arXiv  Detail & Related papers  (2026-04-09T03:49:41Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• Cloning Games, Black Holes and Cryptography [50.022147589030304]
  We introduce a new toolkit for analyzing cloning games.<n>This framework allows us to analyze a new cloning game based on binary phase states.<n>We show that the binary phase variantally optimal bound offers quantitative insights into information scrambling in idealized models of black holes.
  arXiv  Detail & Related papers  (2024-11-07T14:09:32Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  Cross-modal Retrieval methods build similarity relations between vision and language modalities by jointly learning a common representation space. However, the predictions are often unreliable due to the Aleatoric uncertainty, which is induced by low-quality data, e.g., corrupt images, fast-paced videos, and non-detailed texts. We propose a novel Prototype-based Aleatoric Uncertainty Quantification (PAU) framework to provide trustworthy predictions by quantifying the uncertainty arisen from the inherent data ambiguity.
  arXiv  Detail & Related papers  (2023-09-29T09:41:19Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• Publicly-Verifiable Deletion via Target-Collapsing Functions [81.13800728941818]
  We show that targetcollapsing enables publiclyverifiable deletion (PVD) We build on this framework to obtain a variety of primitives supporting publiclyverifiable deletion from weak cryptographic assumptions.
  arXiv  Detail & Related papers  (2023-03-15T15:00:20Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.