ShannonProver 将密码学主定理拆解为中间博弈与引理并生成 EasyCrypt 证明脚本，在 ChaChaPoly1305 与 MEE-CBC 案例上把专家数周至数月的证明工作压缩到数小时内完成
该工作提出 ShannonProver，一个在密码学家已建模协议与安全定义的前提下，把主定理分解为中间博弈与引理并构造 EasyCrypt 证明脚本的智能体系统，并在一个涵盖教科书原语、已部署标准化协议与近期 NIST 提案的新 EasyCrypt 引理数据集上评估，在 ChaChaPoly1305 与 MEE-CBC 等案例中于数小时内完成历史上需专家数周至数月的证明开发。