ShannonProver 将密码学主定理拆解为中间博弈与引理并生成 EasyCrypt 证明脚本，在 ChaChaPoly1305 与 MEE-CBC 案例上把专家数周至数月的证明工作压缩到数小时内完成
核心概要
该工作提出 ShannonProver，一个在密码学家已建模协议与安全定义的前提下，把主定理分解为中间博弈与引理并构造 EasyCrypt 证明脚本的智能体系统，并在一个涵盖教科书原语、已部署标准化协议与近期 NIST 提案的新 EasyCrypt 引理数据集上评估，在 ChaChaPoly1305 与 MEE-CBC 等案例中于数小时内完成历史上需专家数周至数月的证明开发。
Fig. 10: Per-lemma API cost for the ChaCha20-Poly1305 project, grouped by proof shape ( P / I / G ). Bar color compares ShannonProver with the baseline. For concision ( C ), maintainability/readability ( M ), and semantic proof idiom ( S ), a filled green dot denotes an agent proof comparable to or better than the expert proof, while a hollow gray circle denotes an expert advantage. Stars mark the two agent proofs described in Appendix D .
arXiv深度剖析
提出 ShannonProver，一个面向密码学证明的智能体系统：输入由密码学家建模的协议及其安全定义，系统将主定理分解为中间博弈与引理，并为这些引理构造 EasyCrypt 证明脚本。 此前机器可检验证明把瓶颈从人工验证转移到证明撰写本身——即使高层证明计划已知，仍需把计划隐含的每个细节显式写出，对专家也很费力；该工作把这一证明工程负担交由智能体承担。 论文摘要层面给出的系统描述与流程说明；具体实现细节、智能体组件与提示设计未在加载文本中展开。
构建了一个新的 EasyCrypt 引理数据集作为评测基准，覆盖教科书原语、已部署的标准化协议以及近期 NIST 提案，并包含取自此前未在线公开语料的专家案例研究。 相对于既有评测资源，该基准把范围扩展到标准化部署协议与最新 NIST 提案，并引入此前不可得的专家案例语料。 摘要明确说明基准的覆盖范围与语料来源；具体引理数量、难度分层与统计信息未在加载文本中给出。
在 ChaChaPoly1305 与 MEE-CBC 等案例研究上，ShannonProver 在数小时内完成历史上需要专家数周至数月的证明开发。 该结果把智能体自动化从一般性证明辅助推进到真实密码学协议案例的端到端证明开发时间尺度。 摘要报告的是案例研究层面的时间对比（数小时对专家数周至数月），属于作者自述的案例结果；未提供逐案例的详细计时、成功率或与基线的系统对照。
论文提出一条加速密码学研究的路径：当智能体自动化证明工程负担后，密码学家可以更快迭代新构造、更早获得机器可检验的保证，并让协议从设计到部署的周期更短。 这一展望把证明自动化的价值定位从单纯的验证效率，扩展到研究迭代速度与部署节奏。 属于作者基于上述案例结果提出的方向性判断，而非在加载文本中被独立验证的结论。
启示与展望
该工作面向的设定是：密码学家已经完成协议与安全定义的建模，ShannonProver 在此前提下承担把主定理分解为中间博弈与引理并生成 EasyCrypt 证明脚本的工作。因此它直接服务的是形式化密码学研究者与需要机器可检验保证的协议设计者，尤其是使用 EasyCrypt 的工作流。其可扩展的方向包括：把证明工程自动化后用于更快迭代新构造、更早获得机器可检验保证，以及缩短协议从设计到部署的周期；新建的引理基准也为后续方法提供了可比较的评测对象。
加载文本为摘要层面的内容，未包含图表、逐案例计时、成功率、与基线的系统对照以及智能体内部组件与提示设计的细节，因此无法从现有材料判断该方法在不同难度引理上的稳定性与失败模式。基准中教科书原语、标准化协议与 NIST 提案各自的引理数量与难度分布也未给出，读者若关心评测的覆盖面与可比性，需要查阅原文的数据集说明。此外，'数小时对专家数周至数月'的对比来自作者自述的案例研究，其计时口径与专家基线如何界定，属于仍需在原文中确认的开放问题。