发表机构
UC Berkeley; University of Bristol; PQ Shield（加州大学伯克利分校; 布里斯托大学; PQ Shield）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究针对密码学证明人工验证难的问题，提出香农证明器框架。由密码学家提供安全模型等，系统自动构建证明脚本。在易加密形式化密码证明数据集上评估，可自动化部分证明工程，加速密码学研究。
AI 中文摘要
密码学证明的规模日益超出人工验证能力。机器检查的证明为可扩展的证明验证提供了一条途径，但为诸如易加密这样的表达性证明助手编写证明脚本仍然是一个主要瓶颈。本文提出了香农证明器，这是一个用于自动化密码学证明的代理框架。香农证明器针对密码学家提供安全模型和将目标定理分解为引理级证明义务的设置，而系统会自动为这些义务构建易加密证明脚本。我们在易加密中的形式化密码学证明数据集上评估了香农证明器。该数据集涵盖教科书原语、已部署的协议以及诸如美国国家标准与技术研究院提案等标准化工作，并包括从以前无法在线获取的语料库中提取的专家案例研究。我们表明，香农证明器可以为诸如ChaChaPoly1305和MEE-CBC等案例研究自动化密码学证明工程的大部分内容。更广泛地说，这项工作为加速密码学研究提出了一条途径：随着代理自动化证明工程负担，密码学家可以更快地对新结构进行迭代，更早地获得机器检查的保证，并更快地将可信协议从设计推向部署。
英文摘要
Cryptographic proofs are produced at a scale that increasingly exceeds the community's ability to verify them manually. Machine-checked proofs offer a path toward scalable proof verification, but they shift the bottleneck to writing the proofs themselves: even when the high-level proof plan is known, turning it into a proof script requires spelling out every detail the plan leaves implicit, which is laborious even for experts. This paper presents ShannonProver, an agentic system for automating cryptographic proofs. Given a protocol and its security definitions modeled by a cryptographer, ShannonProver decomposes the main theorem into intermediate games and lemmas, and constructs EasyCrypt proof scripts for those lemmas. We evaluate ShannonProver on a new dataset of lemmas in EasyCrypt. The benchmark spans textbook primitives, deployed standardized protocols, as well as recent NIST proposals, and includes expert case studies drawn from a corpus that has not previously been available online. On case studies such as ChaChaPoly1305 and MEE-CBC, ShannonProver completes within hours proof developments that historically took experts weeks to months. More broadly, this work suggests a path toward accelerating cryptographic research: as agents automate the proof-engineering burden, cryptographers can iterate more quickly on new constructions, obtain machine-checked assurance earlier, and bring protocols from design to deployment faster.
