发表机构
National University of Singapore; Beijing Normal-Hong Kong Baptist University; Griffith University（新加坡国立大学; 北京师范大学-香港浸会大学联合国际学院; 格里菲斯大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种人在回路的框架，利用大语言模型生成可审计的协议中间表示，并通过置信度引导的交互界面辅助用户检查关键语义，最终生成Tamarin可验证的安全协议形式化模型。
AI 中文摘要
大语言模型为将自然语言协议描述转换为形式化安全模型提供了有前景的接口，但其输出在没有专家验证的情况下仍难以信任。在本文中，我们提出了一种人在回路框架，用于生成可被Tamarin验证的安全协议形式化模型。我们的关键观察是，主要正确性瓶颈在于中间协议表示的语义准确性，而非其语法有效性。为解决此问题，我们引入了一种协议中间表示（IR），作为自然语言解析与形式化模型生成之间的人工可审计语义检查点。该IR显式捕获协议参与者、消息流、值来源、密码学操作、证明目标及妥协假设。我们进一步设计了一个交互式界面，该界面突出显示不确定字段，并基于模型置信度引导用户在模型生成前检查最关键的语义决策。我们的方法并非取代形式化方法专家，而是利用大语言模型生成可审计的语义草稿，同时利用验证工具检查所生成的形式化模型。代码和验证工件可在该https URL获取。
英文摘要
Large language models offer a promising interface for translating natural-language protocol descriptions into formal security models, but their outputs remain difficult to trust without expert validation. In this paper, we present a human-in-the-loop framework for generating Tamarin-verifiable formal models of security protocols. Our key observation is that the main correctness bottleneck is the semantic accuracy rather than the syntactic validity of the intermediate protocol representation. To address this problem, we introduce a protocol intermediate representation (IR) that serves as a human-auditable semantic checkpoint between natural-language parsing and formal model generation. The IR explicitly captures protocol participants, message flows, value provenance, cryptographic operations, proof targets, and compromise assumptions. We further design an interactive interface that highlights uncertain fields and guides users to inspect the most critical semantic decisions based on model confidence before model generation. Rather than replacing formal-methods experts, our approach uses LLMs to produce auditable semantic drafts while leveraging verification tools to check the resulting formal models. Code and verification artifacts are available at https://github.com/laplace1002/TamarinAgent.git.
