该论文研究如何让大语言模型（LLM）可靠地参与安全协议的形式化建模。背景是：安全协议（如认证与密钥交换协议）的安全性通常需要借助 Tamarin 这类形式化验证工具来证明，而把自然语言写的协议描述（RFC、规范文档）翻译成可验证的形式化模型，长期依赖形式化方法专家手工完成，成本高、门槛高。LLM 看起来是天然的翻译接口，但其输出在没有专家校验的情况下难以信任。 作者的核心观察是：真正的正确性瓶颈不在中间协议表示的语法是否合法，而在于语义是否准确——即模型是否错误理解了参与者、消息流向、密钥来源、加密假设或攻击者能力。基于这一判断，论文提出一个人机协同（human-in-the-loop）框架，用于生成可被 Tamarin 验证的安全协议形式化模型。 方法上，作者设计了一种协议中间表示（Protocol IR），作为自然语言解析与形式模型生成之间的“可人工审计的语义检查点”。该 IR 显式刻画六个关键维度：协议参与者、消息流、取值来源与溯源（value provenance）、密码学操作、证明目标（proof targets）以及妥协假设（compromise assumptions，例如长期密钥泄露、会话密钥泄露等攻击者能力设定）。在此基础上，作者进一步设计交互式界面，依据模型自身的置信度（confidence）突出显示不确定字段，引导用户优先检查对最终安全性结论影响最大的语义决策，之后才进入形式模型生成与验证阶段。 论文的定位不是取代形式化方法专家，而是让 LLM 产出可审计的语义草稿，再由 Tamarin 等验证工具对生成的形式模型进行机器检查，形成“LLM 起草 + 人工审计 + 工具验证”的闭环。作者公开了代码与验证工件（GitHub 仓库 TamarinAgent）。摘要未给出具体实验数据、评测基准或定量结果，因此实际提升幅度与局限性需查阅全文确认。