Source-linked AI summary
LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?
Tianjian Liu, Shicheng Feng, Jin'ao Shang, Xiaoting Lyu, Bin Wang, Zonghua Zhang, Lei Xue, Wei Wang
TL;DR
Security-property specification for cryptographic symbolic protocol verification remains insufficiently understood, despite requiring tool-checkable lemmas and expert effort. The paper evaluates LLM-generated lemmas with CRoST, finding variable coverage and practical limitations on complex protocols, scaling, and verification cost.
Problem
Security-property specification for existing protocol models remains largely manual, and evidence about LLM capability across cryptographic symbolic protocol verification tasks is limited.
Source: §I · pp. 1–2Method
The paper systematically evaluates LLM-generated lemmas and proposes CRoST, a proof-skeleton-based coverage metric whose rationale is tested theoretically and empirically.
Source: §I · p. 2Results
CRoST varies across LLMs and property families; complex multi-phase protocols show stage-point confusion, while more generated lemmas yield diminishing returns and higher verification runtime.
Source: §VII · pp. 10–11Takeaways & Limitations
Few-shot prompting is often needed for syntactically valid Tamarin lemmas, while verification cost and failure on complex protocols remain practical constraints.
Source: §VII · pp. 10–11The 18-protocol benchmark covers secrecy, authentication, and sanity, so results may not generalize to larger collections or other property families; generation randomness may also vary CRoST scores.
Source: C. Threats to Validity · p. 10
Abstract
from arXiv · showhide
Large language models (LLMs) have shown strong potential for assisting software and security analysis tasks, yet their effectiveness in cryptographic symbolic protocol verification remains insufficiently understood. In this paper, we conduct the first systematic evaluation of the capability of state-of-the-art LLMs in cryptographic symbolic protocol verification. To quantify this capability, we propose \textsc{CRoST} (Coverage Rate of Solve Tree), a proof-based metric derived from the verifier's proof skeleton that measures the similarity between generated lemmas and reference lemmas. We then establish the rationale of \textsc{CRoST} through both theoretical analysis and empirical validation. The evaluation results show that state-of-the-art models achieve 38.82\% coverage on average, with 14.4\% of generated lemmas exceeding 80\% coverage, indicating that LLMs can already generate useful lemmas to a certain extent. However, they still exhibit non-trivial failure modes on complex multi-phase protocols, show diminishing returns under naive scaling, and incur substantial verification overhead. These findings clarify the practical potential and limitations of LLMs for protocol verification and motivate future work on complex real-world protocols.
I. INTRODUCTION
The paper studies whether LLMs can generate tool-checkable security properties for existing protocol models, addressing a task that remains largely manual. It introduces CRoST to evaluate generated lemmas and examines LLM performance across CSPV tasks.
I. INTRODUCTION
- Security-property specification remains largely manual, and the paper evaluates whether LLMs can generate tool-checkable lemmas for existing protocol models.The study examines capability boundaries and performance across CSPV task types.Source: §I · pp. 1–2
- The paper proposes CRoST, a proof-based metric derived from Tamarin’s proof skeleton, and justifies it through theoretical analysis and mutation-based evaluation.The study also reports stronger LLM performance on existential propositions and identifies stage-point confusion and time overhead as bottlenecks.Source: §I · p. 2
A. Symbolic Model
- Symbolic verification models cryptographic primitives as ideal black boxes while allowing adversaries to intercept, replay, modify, and inject messages.The Dolev-Yao adversary is limited to symbolic inference rules derived from cryptographic operators.Source: A. Symbolic Model · p. 2
B. Security Properties
- The benchmark considers secrecy, authentication, and sanity properties of protocol executions.Secrecy protects sensitive data, authentication links acceptance to a genuine peer action, and sanity checks intended executability or consistency.Source: B. Security Properties · p. 2
C. Tamarin Prover
- Tamarin expresses protocols with multiset rewriting rules and specifies properties as lemmas over timepoints and action facts.It distinguishes all-traces claims from exists-trace claims; the evaluation selects Tamarin for its modeling and proof support and SAPIC+ integration.Source: C. Tamarin Prover · p. 2
III. METHODOLOGY
The methodology evaluates generated lemma sets against expert-written reference lemmas for the same protocol theories. It uses solve-level coverage from Tamarin proof skeletons because a security property can have multiple lemma forms that text similarity cannot reliably compare.
A. Motivation
- A single security property may have multiple Tamarin lemma forms, making direct comparison of generated and reference lemmas difficult.The same secrecy property may be written as one lemma or split into two role-specific lemmas.Source: A. Motivation · p. 3, Figure 3 · p. 3
- Text similarity is unreliable for semantic equivalence, while truth-table comparison does not generally apply to quantified lemmas over events and timepoints.Tamarin’s proof skeleton records solve goals and case distinctions as a tree, providing a proof-based comparison basis.Source: A. Motivation · p. 3
- CRoST measures how much of a target lemma’s proof skeleton is covered by generated lemmas by comparing their root-to-solve paths.The algorithm extracts paths from target and generated proof trees, matches generated paths against target paths, and returns a coverage ratio.Source: A. Motivation · p. 3
- The analysis treats capability as covering a minimal sufficient set of solve obligations and relates greater coverage to the probability of covering such a set.It studies this relationship under a simplified random-overlap model.Source: A. Motivation · p. 4
B. Definitions and Assumptions
The definitions ground CRoST in solve-items extracted from Tamarin proof skeletons under a fixed protocol and proving configuration. They also formalize lemma-set coverage, sufficient solve-item sets, and a simplified random-overlap model.
B. Definitions and Assumptions
- For a fixed protocol and proving configuration, Tamarin produces a proof skeleton whose nodes include solve goals and whose edges encode case distinctions.The fixed configuration includes Tamarin version, flags, heuristics, and resource bounds; proof search is treated as deterministic under it.Source: B. Definitions and Assumptions · p. 4
- A lemma’s solve footprint is the set of normalized solve-items in its skeleton, with normalization renaming bound variables, removing local indices, and canonicalizing commutative constructs.The finite universe contains normalized solve-items observed under the fixed configuration.Source: B. Definitions and Assumptions · p. 4
- The proof-skeleton order relates a solve-item to itself or its descendants, capturing the reduction structure that produces subgoals.The order is defined under the fixed configuration κ.Source: B. Definitions and Assumptions · p. 4
- Target and generated lemma sets are compared through aggregated solve footprints, with solve-level coverage defined at the lemma-set level.The footprints of multiple lemmas are combined by union.Source: B. Definitions and Assumptions · p. 4
- Capability is the probability that a generated lemma set covers at least one minimal sufficient solve-item set for the target outcome.The random-overlap analysis models a fixed-size overlap as a uniformly sampled subset of the target footprint; exists-trace properties may have single-item minimal generators, unlike typical all-traces properties.Source: B. Definitions and Assumptions · p. 4
C. Predecessor Hits and Minimal-Generator Continuation
The continuation analysis asks whether a generated lemma set that hits a target predecessor proceeds to cover a complete minimal generator. Its estimated continuation probability is about 51.2% on average.
C. Predecessor Hits and Minimal-Generator Continuation
- Exists-trace skeletons can succeed through one witness branch, whereas all-traces skeletons must discharge every case split.The continuation probability captures whether a predecessor hit proceeds to full minimal-generator coverage.Source: Figure 4 · p. 5, C. Predecessor Hits and… · p. 5
- A predecessor-hit event occurs when the generated solve footprint overlaps at least one target-derived predecessor of a minimal-generator item.These predecessors are target solve-items whose reduction can lead to that item.Source: C. Predecessor Hits and… · p. 5
- A predecessor hit does not guarantee full minimal-generator coverage; the estimated average continuation probability is 0.513, or about 51.2%.The estimate comes from repeated runs of the generator under a fixed proving configuration.Source: C. Predecessor Hits and… · p. 5
D. Exists-trace Situation
In the singleton exists-trace setting, directly covering any singleton minimal-generator element is sufficient for success. When there is only one such generator, capability increases linearly with coverage.
D. Exists-trace Situation
- The simplest exists-trace case reaches the target outcome by reaching one solve-item from a singleton minimal generator along a witness branch.Figure 5 illustrates a generator C1 = {solve(a)}.Source: D. Exists-trace Situation · p. 5, Figure 5 · p. 5
- With one singleton minimal generator, capability increases linearly with coverage c.Directly covering any singleton minimal-generator element suffices for success.Source: D. Exists-trace Situation · p. 6
- When no singleton generator element is directly hit, bρ models the chance that predecessor-supported proof search continues to full minimal-generator coverage.The direct-hit event is defined as the generated footprint intersecting the set of singleton minimal-generator elements.Source: D. Exists-trace Situation · pp. 5–6
E. All-traces situation
For all-traces properties, a generator can be supported by hits on its solve-items or their target-derived predecessors, but the proof search may still diverge. A coverage-based lower bound is monotone, while its shape depends on the target proof-skeleton structure.
E. All-traces situation
- A generator is predecessor-supported when each of its elements is hit directly or through a target-derived predecessor; elements may have mixed support.Each element’s support set contains that element and its target-derived predecessors.Source: E. All-traces situation · p. 6
- Even when a minimal generator is predecessor-supported, proof search may diverge, so the lower bound includes a continuation probability.The continuation probability is defined at the minimal-generator level.Source: E. All-traces situation · p. 6
- The capability lower bound is monotone in solve-level coverage c = Cover(L; L⋆).The bound combines Lemma 3 with a computable lower bound under random overlap.Source: E. All-traces situation · p. 6
- The lower bound cannot generally be expressed from coverage c alone because support-set sizes depend on the target proof-skeleton structure.Source: E. All-traces situation · p. 6
- When n ≫ s_j,t, the approximation makes capability rise concavely with c, with larger support sets producing a faster rise.The coverage-driven shape follows by substituting the approximation into the bound.Source: E. All-traces situation · p. 6
A. Dataset
The evaluation uses expert-written protocol lemmas and mutation variants to assess LLM-generated security properties, syntax, proof-tree coverage, and verification cost. Results show that few-shot prompting improves syntax success, while generated lemmas show limited coverage gains under repeated sampling, task-dependent performance, phase-confusion failures, and substantial verification overhead.
A. Dataset
- The dataset contains 18 protocols and 90 expert-written lemmas, augmented with 54 mutation protocols; its reference properties cover secrecy, authentication, and sanity.The dataset is derived from AUTOSM1.Source: A. Dataset · p. 6
B. Results
- Few-shot prompting raises qwen3-coder-plus syntax success by 30.4 percentage points, and most models exceed 70% syntax success under few-shot prompting.Syntax success means Tamarin can parse and compile the generated lemmas without syntax errors; subsequent experiments use few-shot prompting.Source: B. Results · p. 7, Figure 6 · p. 7, Table I · p. 7
- Mutation testing is supporting evidence for CRoST’s rationale, not the primary evaluation metric, because handcrafted mutants require effort, may miss covert real-world flaws, and expose limited proof-search detail.The study uses controlled, verification-relevant fault proxies because real-world protocol vulnerabilities are scarce.Source: B. Results · p. 7
- CRoST coverage correlates positively with mutation flip rate (0.75; p-value = 0.005), supporting its use as a fine-grained indicator of how well generated lemmas capture security properties.Mutation testing treats a verified lemma that becomes falsified on a mutant protocol as detecting the injected vulnerability.Source: B. Results · p. 7, Figure 8 · p. 8
- Across 12 runs, cumulative generated lemmas increase from 239 to 2672, while CROST improves by only about 24 percentage points and largely plateaus after the 8th run.Lemma count is only weakly related to CROST, with substantial dispersion (p-value = 0.04825), indicating that quantity alone does not primarily explain capability differences.Source: B. Results · p. 8, Figure 9 · p. 8, Figure 10 · p. 8
- On average, SOTA LLMs perform better on authentication and sanity than secrecy properties, while the highest-scoring target lemmas are disproportionately sanity properties.The authors suggest that stronger performance on existential than universally quantified properties may explain this pattern.Source: B. Results · p. 8, Table III · p. 9, Figure 11 · p. 9
- In SSH-R, generated lemmas can preserve action-fact roles yet confuse protocol stages, linking a phase-2 event to a phase-1 witness and omitting the temporal relationship.This mismatch can prevent proof search from reaching target solve-tree paths, particularly in large multi-phase protocols with many stage-specific facts.Source: B. Results · p. 9, Figure 12 · p. 9
- Verifying generated lemmas incurs roughly a 4×−21× slowdown versus the baseline, with mean per-lemma verification time rising from 0.66s to 2.51–6.79s.The authors attribute overhead beyond generation to verification attempts on incorrect or low-utility lemmas and longer proof searches per lemma.Source: B. Results · pp. 9–10, Table V · p. 10
C. Threats to Validity
The benchmark covers 18 protocols and three property families, but protocol complexity and property distribution may limit how far the findings generalize. Prompt design, in-context examples, and decoding randomness may also affect generated lemmas and CRoST scores.
C. Threats to Validity
- The benchmark covers 18 protocols and the secrecy, authentication, and sanity property families.Protocol complexity and property distribution may affect observed results, particularly comparisons across property types.Source: C. Threats to Validity · p. 10
- The findings may not generalize to larger protocol collections or property families outside the benchmark.Source: C. Threats to Validity · p. 10
- Lemma generation is sensitive to prompt design, in-context examples, and decoding randomness.Source: C. Threats to Validity · p. 10
- Even with unified prompting and a shared evaluation pipeline, generation randomness may vary lemmas and resulting CRoST scores.Source: C. Threats to Validity · p. 10
A. Future work
The conclusion reports that LLM-generated lemmas show substantial variation and recurring difficulties on complex multi-phase protocols, while scaling lemma generation brings diminishing returns and verification overhead. The discussion distinguishes this property-generation task from earlier verifier automation and protocol-model generation, and identifies several directions for improvement.
A. Future work
- CRoST may falsely match unrelated lemmas at common, low-information solve items such as solve(!KU(x)).Proposed refinements include semantic-category filtering, context-consistency checks, and minimum-information thresholds.Source: A. Future work · p. 10
- Scaling to large, complex protocols requires addressing stage point confusion by aligning correspondence lemmas with phase-specific events and temporal relations.Source: A. Future work · p. 10
- Real-world vulnerability discovery requires an additional counterexample-explanation step.Source: A. Future work · p. 10
- The study is preliminary and adds no protocol-level or property-level features; richer features may improve lemma generation.Source: A. Future work · p. 10
VI. RELATED WORK
- Existing verifier automation is largely coarse-grained: Scyther instantiates generic claims, while Tamarin supports proof scalability rather than scenario-specific property engineering.Source: §VI · p. 10
- Prior LLM work targets symbolic model construction or syntax correctness, whereas this work studies tool-checkable lemma generation when the protocol model is available.Source: §VI · p. 10
VII. CONCLUSION
- CROST varies across LLMs and property families; complex multi-phase protocols show recurring stage point confusion, while more generated lemmas yield diminishing returns and coverage saturation.Verifying generated lemmas also incurs substantially higher runtime than verifying baseline target lemmas.Source: §VII · pp. 10–11