一句话：提出用 LLM 分阶段自动从自然语言文档生成安全协议的符号模型，并用可证可靠的模型变换保证正确性。
符号协议分析是协议设计与安全分析的重要技术，Tamarin、ProVerif 等工具已成功验证 TLS 1.3、5G AKA 等真实协议。然而，编写形式化模型门槛高，阻碍了这些工具的广泛使用。本文提出利用大语言模型（LLM）从自然语言文档自动生成符号协议模型。由于直接使用 LLM 效果不佳，作者将建模任务分解为多个阶段：LLM 进行语义解析，支持轻量人工交互消歧，并设计算法对中间模型进行变换以生成最终符号模型。每个阶段都基于形式化执行模型设计，模型变换被证明是可靠的。作者还构建了包含 18 个真实安全协议文本描述及对应符号模型的基准，工具在其中 10 个案例成功生成了中等规模的正确模型。
Symbolic protocol analysis serves as a pivotal technique for protocol design, security analysis, and the safeguarding of information assets. Several modern tools such as Tamarin and ProVerif have been proven successful in modeling and verifying real-world protocols, including complex protocols like TLS 1.3 and 5G AKA. However, developing formal models for protocol verification is a non-trivial task, which hinders the wide adoption of these powerful tools in practical protocol analysis. In this work, we aim to bridge the gap by developing an automatic method for generating symbolic protocol models using Large Language Models (LLMs) from protocol descriptions in natural language document. Although LLMs are powerful in various code generation tasks, it is shown to be ineffective in generating symbolic models (according to our empirical study). Therefore, rather than applying LLMs naively, we carefully decompose the symbolic protocol modeling task into several stages so that a series of formal models are incrementally developed towards generating the final correct symbolic model. Specifically, we apply LLMs for semantic parsing, enable lightweight manual interaction for disambiguation, and develop algorithms to transform the intermediate models for final symbolic model generation. To ensure the correctness of the generated symbolic model, each stage is designed based on a formal execution model and the model transformations are proven sound. To the best of our knowledge, this is the first work aiming to generate symbolic models for protocol verification from natural language documents. We also introduce a benchmark for symbolic protocol model generation, with 18 real-world security protocol's text description and their corresponding symbolic models. We then demonstrate the potential of our tool, which successfully generated correct models of moderate scale in 10 out of 18 cases. Our tool is released at [1].