AI 中文总结
HOPSCOTCH 是 Lean 4 中用于机械化基于游戏的密码学证明的框架，通过浅嵌入实现，已完成多项密码方案的形式化证明，其 GGM 证明为非恒定深度的首个机械化证明。
AI 中文摘要
我们提出了 HOPSCOTCH，这是一个用于机械化计算可靠的、基于游戏的密码学证明的 Lean 4 框架。安全定义被表述为有状态概率预言机之间的不可区分性，证明遵循标准的游戏跳跃范式。HOPSCOTCH 使用浅嵌入：预言机和归约是普通的 Lean 定义，能够与整个 Lean 生态系统直接集成，包括来自 Mathlib 的一般数学理论，例如有限群论。HOPSCOTCH 中的游戏跳跃证明被表示为显式形式化对象，其构造函数对应于游戏跳跃论证的标准步骤，使证明更易于构建、自动化和检查。我们证明了一个通用的计算可靠性定理，该定理通过针对证明所使用的假设构造归约并推导任何区分器优势的具体界来解释这些证明对象。预言机之间的观察等价性使用状态抽象方法建立：一种简单但强大的方法，支持诸如添加或忘记状态以及将 eager 采样替换为 lazy 采样等转换。我们通过对 encrypt-then-MAC 的 IND-CCA 安全性、基于 DDH 的 ElGamal 加密的安全性、一次性保密性到公钥 IND-CPA 安全性的蕴含以及 GGM 伪随机函数构造的形式化证明来说明该框架。据我们所知，最后一项是针对非恒定深度 GGM 的首个机械化证明。
英文摘要
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.
CommentsThe accompanying HOPSCOTCH artifact, is available under the MIT License at https://github.com/ravst/Hopscotch
