该论文提出了CrypFormBench，一个用于评估大型语言模型（LLM）在密码方案形式化分析能力的综合性基准。手动形式化分析密码方案需要大量专业知识和劳动力，虽然已有模型检测工具（如Scyther、Tamarin）和计算安全工具（如CryptoVerif、EasyCrypt）提升了自动化程度，但它们仍依赖专家对方案进行抽象并编写特定形式化描述。LLM被视为有潜力的替代方案，但缺乏标准化评估方法。CrypFormBench同时覆盖符号安全与计算安全，评估LLM的五项核心能力：解释、生成、补全、转换和修正。基准包含700个实例，涵盖677个方案、7种主流形式化验证语言和160个安全属性。对9个最先进的LLM评估结果显示，大多数在解释和补全任务上表现良好（得益于代码感知优势），但在生成、转换和修正任务上表现不佳。总体性能有限，Claude-3.5得分最高（48.7/100）。论文进一步提供了实用指导，如少样本提示、Pass@K采样和轻量级微调，以缓解可执行性瓶颈并提升工具可用输出。该基准和分析为LLM辅助形式化密码分析提供了当前进展的客观视角和具体方向。