符号协议分析是协议设计、安全分析和信息资产保护的关键技术。Tamarin 和 ProVerif 等多种现代工具已被证明在建模和验证真实协议方面非常成功，包括 TLS 1.3 和 5G AKA 等复杂协议。然而，为协议验证开发形式化模型并非易事，这阻碍了这些强大工具在实际协议分析中的广泛应用。
在这项工作中，我们旨在弥合这一差距，开发一种自动方法，利用大型语言模型 (LLM) 从自然语言文档中的协议描述生成符号协议模型。尽管 LLM 在各种代码生成任务中功能强大，但它在生成符号模型方面效果不佳（根据我们的实证研究）。因此，我们没有简单地应用 LLM，而是将符号协议建模任务仔细分解为几个阶段，以便逐步开发一系列形式化模型，最终生成正确的符号模型。具体来说，我们应用 LLM 进行语义解析，启用轻量级的人工交互进行消歧，并开发算法来转换中间模型，以生成最终的符号模型。为了确保生成的符号模型的正确性，每个阶段都基于形式化执行模型进行设计，并且模型转换经过验证是可靠的。据我们所知，这是第一项旨在从自然语言文档生成用于协议验证的符号模型的工作。我们还引入了一个符号协议模型生成基准，其中包含 18 个真实安全协议的文本描述及其相应的符号模型。然后，我们展示了我们工具的潜力，该工具成功生成了 18 个案例中 10 个中等规模的正确模型。