Source-linked AI summary
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
Siqi Li, Yufan Cai, Hongshu Wang, Xinyue Zuo, Zhe Hou, Jin Song Dong
TL;DR
Formal protocol models can be syntactically valid and verified while still misrepresenting the intended protocol, so semantic faithfulness is a key challenge in LLM-assisted modeling. The paper introduces a confidence-guided, human-auditable Protocol IR between natural-language interpretation and formal model generation. Generated models matched manual references more closely on protocol bodies than on security assumptions, supporting their use as drafts rather than replacements for manual models.
Problem
A formal model may be syntactically valid and verified yet encode the wrong protocol semantics, and constructing faithful models from natural-language requirements remains challenging.
Source: §1 · p. 2Method
The framework uses a confidence-guided Protocol IR as an auditable semantic checkpoint, then supports human review before generating and verifying formal models.
Source: §1 · pp. 2–3Results
Generated models matched manual references more closely on protocol bodies than on security assumptions, so they are useful semantic drafts but not direct replacements for manually developed models.
Source: §3.3 · p. 14Takeaways & Limitations
The reviewed IR makes critical modeling decisions inspectable and correctable before formal verification, while confidence-guided review directs attention to uncertain, high-risk fields.
Source: §1 · p. 3, §6 · p. 19The framework cannot guarantee that confidence-guided review finds every semantic error, and it does not prove the correctness of the IR-to-SAPIC+ translator.
Source: §5.2 · p. 19
Abstract
from arXiv · showhide
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.
1 Introduction
Formal verification can establish security guarantees only when the underlying model faithfully captures protocol semantics; a model may be syntactically valid and verified yet represent the wrong protocol. The paper proposes a confidence-guided Protocol IR as a human-auditable checkpoint and evaluates its construction, review, and generated models.
1 Introduction
- A model can compile and verify while misrepresenting protocol semantics, making semantic faithfulness the central modeling challenge.Formal verification results depend critically on the correctness of the underlying model.Source: §1 · p. 2
- Protocol IR makes security-critical modeling decisions explicit between natural-language descriptions and formal model generation.It records value provenance, initial knowledge, message structure, cryptographic checks, event placement, proof intent, compromise assumptions, and expected counterexamples.Source: §1 · pp. 2–3
- Confidence-guided inspection prioritizes uncertain fields whose errors could affect verification correctness over less critical descriptive fields.Signals include evidence support, consistency with other IR entries, and semantic risk.Source: §1 · p. 3
- The framework combines natural-language-to-IR construction, interactive review, formal-model generation, and backend verification and repair.Its evaluation examines generated IR fields, confidence-guided review, and resulting models and verification outcomes.Source: §1 · p. 3
2 Approach
The approach turns a natural-language protocol description into an auditable Protocol IR, lets users review its semantic decisions, then generates and verifies a formal model. Confidence signals focus review, while semantic changes during repair are routed back to the user.
2 Approach
- The workflow extracts protocol semantics into an IR, supports human review, generates SAPIC+ from the reviewed IR, and checks the model with Tamarin.When syntactic or backend-specific errors arise, the system attempts repair while preserving reviewed semantics.Source: §2 · p. 3, Figure 1 · p. 4
2.1 Protocol IR
- Protocol IR structures reviewable modeling choices, including fresh values, setup state, cryptographic vocabulary, messages, checks, events, proof targets, and compromise assumptions.Fresh values record their name, owner, and purpose; confusing fresh values with setup or long-term state can change the model's security meaning.Source: §2.1 · pp. 4–5
- Role-local actions connect messages to process transitions, while checks, events, proof targets, and compromise assumptions make security claims and attacker scope auditable.Events should follow relevant checks; the IR also records expected attacks and compromise rules.Source: §2.1 · p. 5
2.2 LLM-Based IR Construction
- The LLM produces a structured candidate IR rather than SAPIC+ code directly, attaching source evidence where possible and marking inferred or assumed fields.This lets users inspect both a field and the stated basis for it.Source: §2.2 · pp. 7–8
2.3 Confidence-Guided Human Review
- Review priority combines evidence confidence, consistency with other IR fields, and semantic impact to direct attention toward risky decisions.Fields affecting proof targets, events, checks, or compromise assumptions can receive high priority even when uncertainty is moderate.Source: §2.3 · pp. 8–9
2.4 Formal Model Generation from Reviewed IR
- Reviewed IR fields are translated systematically into SAPIC+ declarations, processes, messages, checks, events, lemmas, and compromise rules.Optional abstraction hints can assist proof engineering, while generation is intended to preserve reviewed semantics.Source: §2.4 · p. 9
2.5 Repair and Verification
- Syntactic repairs may be automated when supported by the reviewed IR, but repairs that change protocol meaning require user review of the affected IR field.Counterexamples are compared with the IR's expected attacks and compromise assumptions rather than automatically treated as modeling bugs.Source: §2.5 · pp. 9–10
3 Evaluation
The evaluation examines IR extraction, end-to-end SAPIC+ generation, alignment with manual models, and workflow cost. Results show that semantic accuracy, successful verification, and structural similarity do not by themselves ensure that generated models preserve the manual models’ security assumptions.
3.1 RQ1: IR Extraction Quality
- GPT-4o had the best average EMR among non-GPT-5.5 models at 51.9%, while GPT-5.5 reached near-perfect semantic accuracy but a 44.8% average WFR.EMR is exact matching at UI-visible cells; WFR checks whether role-local value uses have explicit sources.Source: §3.1 · p. 11, Table 1 · p. 12
3.2 RQ2: End-to-End SAPIC+ Model Generation
- 14 of 18 GPT-5.5-generated models met expected verification outcomes; DeepSeek’s 18 Tamarin-accepted models yielded only 9 expected outcomes.A case succeeds when Tamarin accepts the model and target properties verify or produce expected attacks.Source: Table 2 · p. 12, §3.2 · p. 12
3.3 RQ3: Generated versus Manual Models
- Setup and value provenance aligned best with manual models (F1 = 0.714), while verification checks aligned weakest (F1 = 0.478); generated models matched protocol bodies better than security assumptions.The comparison uses GPT-5.5-generated and manual models at the SAPIC+ level.Source: §3.3 · pp. 13–14
- Example preserves message structure (F1 1.00) despite differing session and compromise assumptions, while LAK06’s low message-structure and cryptographic-dependency precision (0.30, 0.36) reflects added branches and forwarding steps.Source: §3.3 · p. 14
- EDHOC and SSH expose causal errors that structural atom comparisons miss, including locally generated values treated as peer-provided inputs.The manual models instead separate role processes with explicit network input/output boundaries.Source: §3.3 · pp. 13–14
3.4 RQ4: Cost Analysis
- GPT-5.5 required an average of 0.7 IR edits per protocol, versus 72.3 for DeepSeek, 88.5 for GPT-4o, and 90.1 for Llama; runtime totals are outcome-conditioned and not directly comparable.Larger, more complex protocols required substantially more corrections than smaller ones.Source: §3.4 · p. 15
4 Case Study
The KEMTLS case shows how a flight-level description can lead to a semantically incorrect message structure in the raw IR. Human review separates the server flight into correctly protected steps, after which the generated model compiles and matches the reviewed target outcomes.
4 Case Study
- The raw IR places ServerHello, the server’s long-term KEM public key, and the nonce in one plaintext M2, obscuring that the certificate is sent later under the derived server handshake secret.The source’s “same flight” phrasing is the ambiguity behind the misinterpretation.Source: §4 · p. 15, Figure 4 · p. 16
- Review splits the flight into plaintext ServerHello M2 and encrypted ServerCert M3, then records that the client derives CHTS and SHTS before decrypting the certificate.The client recovers the server KEM public key before sending its KEM ciphertext and finished messages.Source: §4 · p. 16
- After review, the generated SAPIC+ model compiles cleanly and Tamarin matches all five reviewed KEMTLS target outcomes.The IR makes the message-structure decision inspectable before formal verification.Source: §4 · p. 16
5 Discussion
The non-standard cases use attack and platform scenarios to make security assumptions explicit and testable, while the paper notes that source ambiguity and unverified translation remain limitations. Future work proposes comparing generated models with their source descriptions.
5.1 Non-standard Cases
- Tamarin reproduces both MCP session-hijacking attacks; the authorization lemma fails because acceptance checks the session identifier without first checking sender authorization.The two modeled attacks involve injecting messages into a shared session queue and impersonating another session.Source: §5.1 · pp. 17–18, Figure 5 · p. 17
- Run-bound artifact selection prevents cross-run substitution but still admits a fork trace; trusted_origin blocks that trace while allowing a legitimate protected-branch deployment.All nine verification outcomes for the three artifact questions match expectations, assuming the checked metadata is authentic.Source: Figure 6 · p. 18, §5.1 · p. 18
- The workflow turns scenarios described through platform documentation, attacks, and mitigations into explicit policy variants and verification targets, separating attack reachability, safety, and legitimate execution.The cases include MCP session hijacking, GitHub Actions artifact provenance, and AWS external-ID delegation.Source: §5.1 · pp. 17–19
5.2 Limitations and Future Work
- The framework cannot fully interpret incomplete natural-language descriptions, depends on the LLM identifying relevant concepts and evidence, and does not prove the IR-to-SAPIC+ translator correct.The authors identify formal IR semantics and a verified or systematically validated translation procedure as stronger implementation requirements.Source: §5.2 · p. 19
- Future work proposes comparing generated models with the source description to flag unsupported behavior or assumptions and missing or reordered steps.The proposed review would check messages, checks, events, and compromise assumptions.Source: §5.2 · p. 19
6 Conclusion
The paper presents confidence-guided Protocol IR as an inspectable, correctable semantic checkpoint before formal verification. Its interface helps users focus review on uncertain and high-risk fields.
6 Conclusion
- Protocol IR makes critical modeling decisions inspectable, correctable, and auditable before formal verification.The confidence-guided interface helps users focus on uncertain and high-risk fields.Source: §6 · p. 19