Confidence guided interface improves security protocol modeling accuracy
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
Cryptography and Security
Summary
Translating natural language descriptions of security protocols into precise, formal models is tricky and often needs experts to check the results. The authors noticed that mistakes mostly happen because the meaning can get lost, not just because of syntax errors. They created an intermediate step that shows key details about the protocol in a way humans can easily check. Their system highlights uncertain parts and helps users focus on what needs careful review before making the final formal model. This approach uses AI to draft models but keeps humans involved to ensure accuracy.
What this means in practice
- •For security protocol developers: Create verified formal models of protocols using AI drafts that guide expert review on uncertain semantic details.
- •For software security teams: Improve trustworthiness of automated protocol modeling by focusing human attention on key uncertain modeling choices.
Authors
Siqi Li, Yufan Cai, Hongshu Wang, Xinyue Zuo, Zhe Hou, Jin Song Dong
Abstract
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.