本文针对一个此前缺乏系统认识的问题展开研究：大语言模型（LLM）在密码协议的符号化验证（symbolic protocol verification）中究竟能起到多大作用。作者指出，LLM 已在软件工程与安全分析任务中表现出较强潜力，但其在密码协议形式化验证这一高度专业化、对正确性要求极严的领域中的实际能力尚不明确，因此开展了（据作者所述）首次系统性评估。 核心方法上，论文提出了一种基于证明的度量指标 CRoST（Coverage Rate of Solve Tree，求解树覆盖率）。该指标从验证器生成的证明骨架（proof skeleton）出发，衡量 LLM 自动生成的引理（lemma）与人工参考引理之间的相似程度，从而把“LLM 辅助验证的效果”量化为可比较的覆盖率数值。作者通过理论分析与实证验证两条路径论证了 CRoST 这一指标的合理性，使其不只是经验性的打分，而具备一定的解释依据。 实验结果显示：当前最先进的模型在协议验证任务上平均仅达到 38.82% 的覆盖率，但其中有 14.4% 的生成引理覆盖率超过 80%，说明 LLM 已经能够在一定程度上产出对验证真正有用的引理，并非完全无效。与此同时，论文揭示了三类明显的失败模式：一是面对复杂的多阶段协议时表现不佳；二是在朴素地扩大模型规模或采样规模时收益递减，暗示单纯 scaling 难以解决问题；三是产生可观的验证开销，即 LLM 生成的候选引理需要形式化验证器反复求解，代价高昂。 论文的贡献可归纳为：给出首个系统性的 LLM 协议验证能力评估、提出并验证 CRoST 度量、量化当前能力上限与失败模式，并据此为面向真实复杂协议的后续研究指明方向（如更好的引理筛选、搜索策略与开销控制）。该工作适合形式化方法与协议安全研究者、以及尝试把 LLM 引入验证工具链的工程团队阅读。