LLM辅助的密码协议自动安全性证明：我们还有多远？
LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?
- Xi’an Jiaotong University（西安交通大学）
- Tianjin University（天津大学）
- Zhejiang Key Laboratory of Artificial Intelligence of Things (AIoT) Network and Data Security（浙江省物联网人工智能网络与数据安全重点实验室）
- CRSC Research & Design Institute Group Co., Ltd（中国航天科工集团第三研究院（注：CRSC通常指China Aerospace Science and Industry Corporation III, 但此处按字面翻译为 CRSC 研究设计院集团有限公司，若需通用名可译为 中国航天科工集团第三研究院））
- Sun Yat-sen University（中山大学）
- Shenzhen Loop Area Institute（深圳河套学院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
该研究首次系统评估前沿大语言模型的密码符号协议验证能力，提出基于证明的\textsc{CRoST}指标量化能力，证实其已能生成部分有用引理，但仍存在复杂协议失效等局限，为后续研究指明方向。
AI中文摘要：
大语言模型（LLM）已在辅助软件与安全分析任务中展现出巨大潜力，但其在密码符号协议验证中的有效性仍未得到充分研究。\n 本文首次对当前最先进LLM的密码符号协议验证能力开展系统性评估。为量化该能力，我们提出了\textsc{CRoST}（求解树覆盖率），这是一种基于证明的指标，源自验证器的证明框架，用于衡量生成引理与参考引理之间的相似度。我们通过理论分析与实证验证共同确立了\textsc{CRoST}的合理性。评估结果显示，当前最先进模型的平均覆盖率达38.82%，其中14.4%的生成引理覆盖率超过80%，表明LLM已能在一定程度上生成有用的引理。但它们在复杂多阶段协议上仍存在明显的失效模式，在简单缩放策略下收益递减，且会带来可观的验证开销。这些发现明确了LLM用于协议验证的实际潜力与局限性，也为未来面向复杂真实世界协议的研究提供了方向。
英文摘要：
Large language models (LLMs) have shown strong potential for assisting software and security analysis tasks, yet their effectiveness in cryptographic symbolic protocol verification remains insufficiently understood. In this paper, we conduct the first systematic evaluation of the capability of state-of-the-art LLMs in cryptographic symbolic protocol verification. To quantify this capability, we propose \textsc{CRoST} (Coverage Rate of Solve Tree), a proof-based metric derived from the verifier's proof skeleton that measures the similarity between generated lemmas and reference lemmas. We then establish the rationale of \textsc{CRoST} through both theoretical analysis and empirical validation. The evaluation results show that state-of-the-art models achieve 38.82\% coverage on average, with 14.4\% of generated lemmas exceeding 80\% coverage, indicating that LLMs can already generate useful lemmas to a certain extent. However, they still exhibit non-trivial failure modes on complex multi-phase protocols, show diminishing returns under naive scaling, and incur substantial verification overhead. These findings clarify the practical potential and limitations of LLMs for protocol verification and motivate future work on complex real-world protocols.
