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∗ *
arXiv:2609.35434v1 [cs.CR] 28 Sep 2026
∗ Xi’an Jiaotong University, Xi’an, China
{tianjian.liu, jinao s}@stu.xjtu.edu.cn, {xiaoting.lyu, wei.wang}@xjtu.edu.cn † Tianjin University, Tianjin, China [email protected] ‡ Zhejiang Key Laboratory of Artificial Intelligence of Things (AIoT) Network and Data Security [email protected] § CRSC Research & Design Institute Group Co., Ltd [email protected] ¶ Sun Yat-sen University, Guangzhou, China [email protected] ∥ Shenzhen Loop Area Institute, Shenzhen, China *Corresponding authors: Lei Xue and Wei Wang. Abstract—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 CRO ST (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 CRO ST 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. Index Terms—LLM, Formal verification, Cryptographic protocol, Symbolic model
I. I NTRODUCTION Cryptographic protocols are designed to coordinate securitycritical interactions and achieve security goals such as secrecy and authentication. In symbolic models, these goals are formalized as security properties over protocol executions, enabling verification tools to reason about whether an active adversary can break them. This style of analysis has proved practically valuable by exposing subtle flaws in widely deployed or standardized protocols, e.g., PCS violations enabled by Signal’s session handling layer [1], multiple confirmed vulnerabilities in Apple/Samsung proximity tracking protocols [2], and critical attacks on the EMV payment standard [3].
However, as shown in Figure 1, completing a protocol verification typically involves (Step 1) formalizing the cryptographic protocol, (Step 2) defining security properties, and (Step 3) analyzing counterexample traces [4]. This process still requires substantial expert knowledge and manual effort [2], [5]–[7]. As reported by the Galois team [8], formally verifying the AES-256-GCM and SHA-384 implementations in AWS LibCrypto required approximately nine person-months of work by experienced proof engineers. symbolic model
verified
step 1
Protocol System
? step 2
Security Property
falsified
formal verification tools
step 3
analyze proof traces
timeout
Fig. 1. Symbolic model verification pipeline.
Recent advances in LLMs [9]–[13] suggest a possible route for automatically extracting unambiguous and analyzable specifications, thereby lowering the barrier to applying formal methods. Prior work on combining LLMs with symbolic model verification tools for cryptographic protocols has mainly studied the translation of natural-language protocol descriptions into tool-checkable symbolic models (Step 1) [14]. However, the complementary task of specifying security properties (Step 2) remains largely manual. Symbolic verifiers require explicit security goals as input, and these goals must be written as tool-checkable lemmas. Writing and refining such lemmas requires expert knowledge; it also determines what the verifier actually checks and how difficult the subsequent proof search becomes [15]–[18]. We therefore focus on securityproperty specification for already available protocol models,
and study whether LLMs can generate tool-checkable security properties in Cryptographic Symbolic Protocol Verification (CSPV) (Step 2). To answer this question, this paper presents a systematic empirical study that focuses on two research questions: • What are the capability boundaries of LLMs for security-property generation in CSPV? • How do LLMs perform across different task types in CSPV? There are two challenges in answering the above questions. First, due to the diversity of representations (We will give an example in Section III-A) for the same security property, it is difficult to measure the similarity between a generated security property and a target correct security property using simple text-based comparison. To capture deeper features of security properties in the verification process, we introduce a proofbased metric derived from Tamarin’s proof skeleton, which reflects security properties feature at the proof-search layer [15], [16]. We further justify the rationale and effectiveness of this metric through theoretical analysis and mutation-based empirical validation. Second, symbolic protocol verification tools such as Tamarin use domain-specific specification languages to describe protocols and their security properties. In such languages, security properties often involve temporal semantics, deeply nested logical structures, and protocol-specific constraints. These characteristics make it difficult for LLMs to generate syntactically correct security properties, even when the intended property is conceptually simple [19]. In this work, we therefore investigate the effect of few-shot prompting on LLM-based security property generation and evaluate whether lightweight in-context examples can improve syntactic validity and downstream verification performance. In summary, our contributions are as follows: • We present the first systematic empirical study of LLM capability in CSPV tasks of secrecy, authentication, and sanity. Our evaluation shows that LLMs exhibit stronger performance on existential propositions. • We propose a solve-level coverage metric named CRoST (Coverage Rate of Solve Tree) for quantifying security properties similarity, and validate its rationality through both theoretical analysis and mutation-based evaluation. • We unveil the main limitations and failure modes of mainstream LLMs when they are applied in CSPV tasks. We show that stage-point confusion in complex multiphase protocols and substantial time overhead are two major bottlenecks for using LLMs in CSPV. II. BACKGROUND A. Symbolic Model Symbolic verification [20] of cryptographic protocols is conducted under the Dolev-Yao adversary model. In this adversary model, cryptographic primitives are treated as ideal black boxes, and the adversary is allowed to intercept, replay, modify, and inject messages arbitrarily, while being limited to
symbolic inference rules derived from the algebraic properties of cryptographic operators [21]. B. Security Properties Cryptographic protocols are intended to guarantee security properties such as secrecy, authentication, and sanity. Secrecy captures scenarios in which sensitive data, such as session keys or private messages, should remain unavailable to the adversary [16], [22]. Authentication captures scenarios in which one party’s acceptance should correspond to a genuine prior action of its intended peer, rather than to an adversarial forgery or replay [16], [18], [23]. In protocol analysis, sanity is often used as a basic executability or consistency property, checking that the modeled protocol can complete an intended interaction and that security claims do not hold only vacuously [16]. C. Tamarin Prover In the symbolic verification tool Tamarin Prover [24], [25], protocols are specified using multiset rewriting rules of the form: [lhs] − [ActionFacts] → [rhs] Where lhs and rhs are multisets of facts representing the current protocol state. A rule can fire when the facts in lhs are available; firing the rule consumes the facts on the left and produces the facts on the right. The bracketed ActionFacts on the arrow are not part of the state; instead, they are recorded as observable events on the execution trace and form the basis for specifying security properties as lemmas. In Figure 2, the rule Reveal_ltk models long-term key compromise: it reuses a persistent key fact !Ltk(A,ltk), emits the event LtkReveal(A), and outputs the leaked key via Out(ltk). rule Reveal_ltk: [ !Ltk(A,ltk) ] // storing long-term key. --[ LtkReveal(A) ]->// Record the reveal event. [ Out(ltk) ] // Output the leaked key.
Fig. 2. Rewriting rule example.
Security properties in Tamarin are expressed as lemmas (Figure 3), which are first-order logic (FOL) with quantification over timepoints. Lemmas may quantify universally or existentially over timepoints and action facts, allowing the specification of both safety and reachability properties. Tamarin distinguishes between all-traces lemmas, which must hold for all possible executions, and exists-trace lemmas, which assert the existence of a witness trace [16]. In this work, we instantiate our evaluation on Tamarin as the target symbolic verifier for two reasons. First, among symbolic protocol verification tools, Tamarin offers particularly strong modeling expressiveness and proof support. It can handle rich equational theories, mutable state, and provides both automatic and interactive proof modes, which is important for complex, real-world protocol models [26]. Second, Tamarin integrates the SAPIC+ process calculus [27], a cross-tool modeling layer that can translate SAPIC+ specifications to Tamarin, ProVerif, and DeepSec. This allows protocol models developed in a multi-verifier workflow to be instantiated as Tamarin theories for our evaluation.
III. M ETHODOLOGY A. Motivation In this section, we assess how closely LLM-generated lemmas align with expert-written lemmas in expressing the intended security properties of a protocol. Our benchmark provides, for each protocol theory, a reference lemma set written by human experts, which we treat as the target specification. Based on this comparison, we first derive a metric CRoST from empirical observations about proof behavior and generation difficulty, and then justify its rationale in subsection III-B. To derive the metric, a key difficulty is that a Tamarin lemma is a quantified temporal FOL formula over action facts and their ordering on traces [16], [19]. There is rarely a canonical lemma form for a given security property: One security property can be expressed in various forms. For example, Figure 3 shows that the same secrecy property definition can be written either as a single overall lemma Secrecy, or equivalently split into two lemmas Secrecy_split_A and Secrecy_split_B that branch on role-specific reveal conditions. This poses a challenge for lemma evaluation metrics. // Same secrecy property, written in two forms. lemma Secrecy: "All A B m #i. Secret(A,B,m)@#i ==> not (Ex #r. K(m)@#r) | (Ex #r. Reveal(A)@#r) | (Ex #r. Reveal(B)@#r)" lemma Secrecy_split_A: "All A B m #i. Secret(A,B,m)@#i & not(Ex #r. Reveal(A)@#r) ==> not (Ex #r. K(m)@#r) | (Ex #r. Reveal(B)@#r)" lemma Secrecy_split_B: "All A B m #i. Secret(A,B,m)@#i & not(Ex #r. Reveal(B)@#r) ==> not (Ex #r. K(m)@#r) | (Ex #r. Reveal(A)@#r)"
Fig. 3. Alternative Tamarin specifications for the same secrecy property.
Text-level similarity metrics such as BLEU [28] are not reliable signals for whether two lemma sets define the same security property; metrics based on matching are known to correlate poorly with semantic or functional correctness in other generation settings [29]. A seemingly stronger alternative is to compare FOL components via truth tables [30]. However, Tamarin lemmas involve quantification over events and timepoints. Truth-table comparison is not applicable in general. We therefore adopt a proof-based comparison based on Tamarin’s proof artifacts. Given a protocol and a lemma, Tamarin’s automated proof search produces a proof skeleton (Figure 4) that explicitly records the encountered solve(...) goals and case distinctions [16] as tree structure. Intuitively, these solve obligations reflect which parts of the verifier’s reasoning space are exercised by a lemma specification. This is similar to proof-based criteria in software testing, where coverage quantifies how thoroughly executions
exercise a graph-structured behavior space [31]–[33]. From a software testing perspective, a useful coverage criterion should be measurable, reliable, and predictive. Motivated by this principle, we design CRoST as a proof-based coverage metric over Tamarin proof skeletons. Algorithm 1 computes CRO ST in three steps. Lines 1-10 define the procedure ExtractPaths, which traverses a proof tree and records every path. Lines 12-17 apply this procedure to all target and generated proof trees to build the path sets P ⋆ and P . Lines 19-23 then compare each target path against the generated paths and mark it as covered when a match is found. Finally, Lines 24-27 return the coverage ratio. Algorithm 1: CRoST: Coverage Rate of Solve Tree. Input: Target proof trees T ⋆ , generated proof trees T Output: CRoST score c ∈ [0, 1] 1 Function ExtractPaths(node, pref ix): 2 P ←∅ 3 if node is a solve node then 4 pref ix′ ← pref ix ∥ ⟨label(node)⟩ 5 P ← P ∪ {pref ix′ } 6 else 7 pref ix′ ← pref ix 9
foreach child ∈ Children(node) do P ← P ∪ ExtractPaths(child, pref ix′ )
10
return P
11
P ⋆ ← ∅, P ← ∅
8
// Extract all root-to-solve paths from target lemmas.
foreach tree ∈ T ⋆ do 13 foreach root ∈ Roots(tree) do 14 P ⋆ ← P ⋆ ∪ ExtractPaths(root, ⟨ ⟩)
12
// Extract all root-to-solve paths from generated lemmas.
foreach tree ∈ T do 16 foreach root ∈ Roots(tree) do 17 P ← P ∪ ExtractPaths(root, ⟨ ⟩)
15
18
covered ← ∅ // Compute covered target paths using subsequence matching (p ⪯ q).
foreach p ∈ P ⋆ do 20 foreach q ∈ P do 21 if p ⪯ q then 22 covered ← covered ∪ {p} 23 break
19
if |P ⋆ | = 0 then 25 return c ← 0 26 else 27 return c ← |covered| |P ⋆ |
24
Prior work has shown that proof-based coverage metrics can serve as a practical alternative to mutation-based coverage in formal verification, while yielding meaningful information about specification adequacy [31]. In the symbolic verification
of cryptographic protocols scenario, we go one step further by studying whether coverage also correlates with the similarity between generated lemmas and target lemmas. Goal and proof idea: Our goal is to evaluate an LLMgenerated lemma set by how effectively it reproduces the proof obligations required to establish a target security property in Tamarin. We use solve-level coverage to measure how much of the target lemma’s proof skeleton is covered by the generated lemma. In the following, we formalize (i) capability as covering a minimal sufficient set of solve obligations, i.e., a minimal generator of the sufficient-set family, and (ii) how increasing coverage raises the probability of covering at least one such minimal generator. We further quantify this relationship under a simple random-overlap model. B. Definitions and Assumptions
Definition 1 (Atomic solve-item and solve footprint). Each solve(c) node contains a goal/constraint term c. We apply a normalization function Norm(·) that (i) α-renames bound variables, (ii) erases proof-local indices/counters, and (iii) canonicalizes commutative constructs. A normalized atomic solve-item is u := Norm(c). Let U be the finite universe of normalized solve-items observed under the fixed configuration κ. The solve footprint of lemma L is S(L) := { Norm(c) ∈ U | solve(c) occurs in Skel(L) } ⊆ U. (1)
Proof-skeleton order over solve occurrences: After normalization, each solve(c) node is labeled by an atomic solve-item u = Norm(c). For x, y ∈ U, define iff
x = y or x is a descendant of y
S(L) ⊆ U.
S(L) :=
(3)
L∈L
Given a target lemma set L⋆ and a candidate generated lemma set L, let S ⋆ := S(L⋆ ),
S := S(L),
H := S ∩ S ⋆ .
(4)
We write n := |S ⋆ |,
k := |H|.
(5)
The solve-level coverage is defined as Cover(L; L⋆ ) :=
|S(L) ∩ S(L⋆ )| k = = c ∈ [0, 1]. |S(L⋆ )| n
(6)
Definition 3 (Minimal generators of the sufficient-set family). Under fixed P, κ, let F ⊆ 2U be the upward-closed family of solve-item sets sufficient for the target outcome. The minimal generators of F are the inclusion-minimal elements of F : Min(F) := { C ∈ F | ∄C ′ ⊊ C : C ′ ∈ F }.
Tool-grounded observables under a fixed proving configuration: We fix a protocol theory P and a proving configuration κ (Tamarin version, command-line flags, heuristic rules, and resource bounds). For any lemma L, let Skel(L) := Autoprove(P, L; κ) denote the proof skeleton produced by Tamarin under κ. We view Skel(L) as a finite rooted structure whose nodes include solve(c) goals and whose edges reflect explicit case distinctions in the skeleton output.
x ⪯κ y
lift the solve footprint from individual lemmas to the lemma-set level by union: [
(2)
This relation captures the solve-reduction structure induced by the proof tree: a node is below another precisely when it arises from reducing subgoals generated by it. Deterministic proof search policy: Under fixed κ, Tamarin’s automated proof search uses a fixed heuristic ranking to prioritize open constraints and proof methods. Operationally, we treat Skel(L) as the deterministic unfolding of the proof-search policy induced by κ, yielding a reproducible solve/case structure for a given (P, L). (B) Lemma-set abstraction for security properties: In practice, a target security property may be specified by a set of Tamarin lemmas rather than a single canonical lemma. Likewise, an LLM may generate multiple lemmas that jointly describe parts of the same intended property. Therefore, we treat a lemma set as the unit of comparison: multiple lemmas are abstracted into a property-level solve footprint, obtained by aggregating their normalized solve footprints. Definition 2 (solve-level coverage). For a finite lemma set L under the same protocol P and proving configuration κ, we
(7)
We write Min(F ) = {C1 , . . . , CM }. Equivalently, for any X ⊆ U, X∈F
⇐⇒
∃j ∈ {1, . . . , M } : Cj ⊆ X.
(8)
Each Cj represents a minimal sufficient set of normalized solve-items for the target outcome, i.e., no proper subset of Cj is sufficient. Typically |Cj | > 1 for all-traces properties, while exists-trace properties may admit |Cj | = 1. Figure 4 contrasts two typical skeleton shapes: exists-trace lemmas succeed by finding one witness branch, whereas all-traces lemmas require discharging all case splits. Definition 4 (Capability of a lemma generator). Let G be a lemma generator pipeline. Given a protocol context, G induces a distribution over finite lemma sets. The generation capability of G is the probability that the generated lemma set covers at least one minimal generator: Ability(G; F) := Pr S(L) ∈ F L∼G = Pr ∃j ∈ {1, . . . , M } : Cj ⊆ S(L) .
(9)
L∼G
L ∼ G means L is sampled from distribution induced by G. Sanity check: If Cover(L; L⋆ ) = 1, then by definition ⋆ S(L ) ⊆ S(L). If the target lemma set is sufficient, i.e., S(L⋆ ) ∈ F, then there exists some minimal generator Cj ⊆ S(L⋆ ). Consequently, Cj ⊆ S(L), which implies S(L) ∈ F . (C) A tractable random model: To quantitatively relate solve-level coverage to generation capability, we adopt a simplified conditional random model. Assumption 1 (Random overlap conditional on coverage). Fix a target lemma set L⋆ . In practice, the generated footprint S(L) may be correlated with S(L⋆ ) because both are induced by the same protocol theory and proving configuration. For a tractable analysis, however, we do not assume any favorable target-specific alignment. Conditioned only on the overlap size |H| = k, we model H as a uniformly random k-subset of S(L⋆ ), sampled without replacement. C. Predecessor Hits and Minimal-Generator Continuation Minimal-generator elements: For each Cj ∈ Min(F), let Cj = {uj,1 , uj,2 , . . . , uj,mj } ⊆ U,
mj := |Cj |.
(10)
(a) exists-trace: one successful branch suffices. (b) all-traces: all branches must be discharged. Fig. 4. Contrasting proof skeleton for exists-trace vs all-traces lemmas in Tamarin.
Predecessor sets: Using the proof-skeleton order ⪯κ , for each uj,k ∈ Cj let its target-derived predecessor set be Predκ (uj,k ) := { g ∈ S ⋆ | uj,k ⪯κ g, g ̸= uj,k }.
(11)
Intuitively, Predκ (uj,k ) contains target solve-items whose reduction can lead to the solve obligation uj,k . Definition 5 (Predecessor-hit event). For a generated lemma set L, let Hitj,k (L) = 1
iff
H ∩ Predκ (uj,k ) ̸= ∅.
be the set of solve-items that form singleton minimal generators. For example, Figure 5 illustrates the case where one such generator is C1 = {u1 }. Predκ(u1)={solve(b), solve(c), solve(d), solve(e)}
solve(d)
Estimation 1 (Predecessor-to-minimal-generator continuation probability). For each (j, h k), let i L∼G
Hitj,k (L) = 1 .
(13)
In our experiments under a fixed κ, we estimate ρj,k from repeated runs of G; for example, the average continuation probability is ρb ≈ 0.513, i.e., conditioned on a predecessor hit, the full minimal generator is covered about 51.2% of the time. Empirical predecessor-to-generator continuation probability: A predecessor hit does not fix the remaining proofsearch trajectory: the subsequent goal ordering and case splits may still diverge from the target skeleton. Therefore, even under a fixed configuration κ, hitting a predecessor does not guarantee covering the whole minimal generator. The central problem in this proof model can be viewed as analogous to probabilistic reachability in uncertain graphs [34]: a predecessor hit indicates a possible support path, while ρ estimates the probability that this path continues to full minimal-generator coverage. D. Exists-trace Situation We first focus on the simplest exists-trace situation, where the target outcome can be witnessed by reaching one solve-item from a singleton minimal generator. Let W := { u ∈ U | {u} ∈ Min(F) }
predecessor hit
solve(e)
(12)
That is, the generated lemma set hits at least one target predecessor of the minimal-generator element uj,k .
ρj,k := Pr Cj ⊆ H
solve(g)
(14)
solve(b)
solve(c)
possible proof paths proof skeleton paths
C1={solve(a)}
u1=solve(a)
prove path: 1. solve(d) - solve(b) - solve(a) 2. solve(e) - solve(b) - solve(a) 3. solve(g) - solve(c) - solve(a)
Fig. 5. Exists-trace witness shape with a singleton minimal generator. The minimal generator is C1 = {solve(a)}; reaching this solve-item along one witness branch suffices to establish the target outcome.
Lemma 1 (Capability equals hitting a singleton minimal generator). In the singleton exists-trace setting, the capability of G is Ability(G; F) = Pr ∃u ∈ W : u ∈ S(L) . L∼G
(15)
Lemma 2 (Closed-form capability from coverage in the singleton exists-trace case). Define the direct-hit event A := { H ∩ W ̸= ∅ },
(16)
i.e., the generated footprint directly covers at least one singleton minimal-generator element. Under Assumption 1, with k treated as a fixed overlap size, we write Prk [·] for the probability induced by drawing H uniformly from all k-subsets of S ⋆ . Let r := |W |. Then Pr[A] = 1 − k
n−r k n k
.
(17)
Let ρb denote the empirical continuation probability that, when no singleton minimal-generator element is directly hit, predecessor-supported proof search still continues to full minimal-generator coverage under fixed configuration κ. Then
the success probability is modeled as Ability(G; F) = Pr[A] + 1 − Pr[A] ρb k
k
= ρb + (1 − ρb) 1 −
n−r k n k
!
(18) .
For the special case r = 1, this reduces to Ability(G; F) = ρb + (1 − ρb) c.
A computable lower bound for Pr[Ej ] under random overlap: Under Assumption 1, H is a uniformly random ksubset of S ⋆ . For each element, define the miss event }. T Fj,t := { H ∩ Xj,t = ∅ S Then Ej = t ¬Fj,t and hence ¬Ej = t Fj,t . By a union bound,
(19)
Interpretation. In the singleton exists-trace setting, directly covering any singleton minimal-generator element is sufficient for success. If the generated footprint instead only reaches predecessor-supported items, ρb models the probability that this support continues to full minimal-generator coverage. When there is only one singleton minimal generator, capability increases linearly with coverage c.
Pr[Ej ] ≥ 1 −
mj X
Pr[Fj,t ].
Moreover, each miss probability has a hypergeometric closed form: n−s j,t
k n k
Pr[Fj,t ] =
with the convention that into (22) yields
a k
Pr[Ej ] ≥ 1 −
E. All-traces situation
t=1
This definition allows mixed evidence: some elements of Cj may be directly covered by H, while others may only be supported through predecessor hits. Continuation probability for an all-traces minimal generator: Even when Ej holds, the remaining proof-search trajectory may still diverge from the target skeleton. We therefore define a minimal-generator-level continuation probability: h i ρj := Pr Cj ⊆ S(L) L∼G
Ej
∈ [0, 1].
,
(23)
= 0 if a < k. Plugging (23) mj X t=1
We now consider the typical all-traces situation, where the target outcome may admit multiple minimal generators and each minimal generator may contain multiple solve-items. Mixed direct hits and predecessor hits: For each element uj,t ∈ Cj , define its support set as Xj,t := {uj,t } ∪ Predκ (uj,t ) ⊆ S ⋆ , sj,t := |Xj,t |. We say that uj,t is supported by the generated footprint if H hits either the element itself or one of its target-derived predecessors: Ej,t := { H ∩ Xj,t ̸= ∅ }. Accordingly, a minimal generator Cj is predecessor-supported if all of its elements are supported: mj \ Ej,t . Ej :=
(22)
t=1
n−sj,t k n k
.
(24)
Coverage-to-capability relation: Combining Lemma 3 and (24), and substituting k = cn, we obtain the following monotone lower bound: ( !) Ability(G; F) ≥ max j∈[M ]
ρj
1−
mj X t=1
n−sj,t c·n n c·n
.
(25)
Interpretation. The lower bound is monotone in the solvelevel coverage c = Cover(L; L⋆ ). However, the support-set sizes sj,t depend on the target proof-skeleton structure, so the bound cannot in general be reduced to a closed-form expression purely in terms of c. When analyzing protocol-level coverage over a large lemma set, it is natural to have n = |S ⋆ | ≫ sj,t . In this regime, with k = cn, the combinatorial term admits the approximation n−sj,t k n k
≈
k 1− n
sj,t
= (1 − c)sj,t .
(26)
Substituting (26) into Eq. (25) yields the following coveragedriven shape: ( !) Ability(G; F) ≳ max
j∈[M ]
ρj
mj X 1− (1 − c)sj,t
.
(27)
t=1
This approximation suggests that capability increases with coverage in a concave manner through the terms 1−(1−c)sj,t , and that larger support sets lead to a faster rise as c increases. IV. E XPERIMENT
(20)
A. Dataset
Lemma 3 (Capability lower bound via predecessor-supported minimal generators). For any j ∈ {1, . . . , M }, Ability(G; F) ≥ Pr Cj ⊆ S(L) ≥ ρj · Pr Ej . L∼G
L∼G
Consequently, Ability(G; F) ≥ max ρj · Pr Ej . j∈[M ]
L∼G
Proof. The first inequality holds because Ability(G; F) = Pr ∃j ′ : Cj ′ ⊆ S(L) , L∼G
which dominates any fixed witness j. For the second inequality, write Pr[Cj ⊆ S(L)] = Pr[Cj ⊆ S(L) | Ej ] Pr[Ej ] + Pr[Cj ⊆ S(L) | ¬Ej ] Pr[¬Ej ] ≥ ρj Pr[Ej ],
(21)
using the definition of ρj in (20) and non-negativity of probabilities.
Our dataset is derived from AUTO SM1 [14], which include 18 protocols and 90 human-expert-written lemmas from different cryptography scenarios. We have added 54 mutation protocols based on this dataset, which will be explained further in section IV-B. For each protocol theory P , the dataset includes a reference lemma set that specifies intended security properties. The properties can be classified by secrecy, authentication, and sanity. B. Results To answer the two research questions raised in the introduction (section I), we organize the evaluation around the following five sub-questions. 1 https://github.com/zerrymore/AutoSM
RQ1. How well do LLMs produce syntactically valid specifications in CSPV? RQ2. How effective is CRoST as an evaluation metric? RQ3. What are the capability boundaries of LLMs in CSPV? RQ4. How do LLMs perform across different task types in CSPV? RQ5. What is the computational cost of using LLMs in CSPV? RQ1. How well do LLMs produce syntactically valid specifications in CSPV? Since Tamarin uses a domain-specific specification language rather than a general-purpose programming language such as Python, C, or Java, publicly available examples are relatively limited [15], [16], [35], [36]. In practice, this challenge often appears first at the syntactic level. LLMs may fail to produce lemma specifications that are well-formed and toolcheckable [19]. We therefore begin by investigating whether LLMs can reliably produce usable lemma specifications, and whether few-shot prompting (in-context learning) [37], [38] can improve syntactic validity and downstream verification performance by providing a small number of demonstrations in the form of multiset rewriting rules with 1–4 corresponding lemmas. We start with a comparison between zero-shot and few-shot prompting on the same set of rule inputs. The syntax success means that the generated lemmas can be parsed and compiled by Tamarin without syntax errors. Figure 6 shows the results for qwen3-coder-plus. Compared with zero-shot prompting, few-shot prompting improves the syntax success rate by 30.4 percentage points. This indicates that few-shot prompting can significantly improve the syntax success rate.
Fig. 6. Zero-shot vs. few-shot syntax success for qwen3-coder-plus.
Table I summarizes the syntax success rates across models; the majority exceed 70% under few-shot prompting, providing a necessary foundation for the later evaluation that focuses on proof-search behavior and security property coverage rather than surface syntax. In all subsequent experiments, we use few-shot prompting as the default generation setting.
TABLE I S YNTAX S UCCESS R ATE BY M ODEL .
Model
Generated Syntax Success Rate (%)
grok-4 claude-sonnet-4.5 gpt-5.2-codex claude-opus-4.5 gemini-3-flash-preview gpt-5.2 claude-haiku-4.5 qwen-plus deepseek-v3.2 gpt-4 qwen3.5-plus qwen3-coder-plus
75 245 118 166 95 204 290 78 230 74 218 139
74 241 114 155 86 169 230 57 166 46 135 82
98.67 98.37 96.61 93.37 90.53 82.84 79.31 73.08 72.17 62.16 61.93 58.99
Since real-world cryptographic protocol vulnerabilities are scarce, we adopt mutation testing to assess whether CRO ST is a rational metric [40]. Specifically, we inject a suite of simple, explicit flaws into protocol rules (Table II), generated with Gemini-3-Pro and manually vetted by human experts. These vulnerabilities are designed as controlled, verificationrelevant fault proxies. Since security properties characterize the intended security behavior of a protocol, any vulnerability should violate at least one of them. Therefore, if a lemma captures the target property well, a local perturbation that breaks that property should cause the verification result to flip, allowing us to test whether CRO ST responds appropriately to property-breaking changes. As illustrated in Figure 7, if a lemma is verified on the original protocol but becomes falsified on a mutant, we treat the injected vulnerability as detected by that lemma. We then use the resulting flip rate over mutants to assess the validity of CRO ST. What needs to be explained here is mutation testing itself can serve as an indicator of lemma-generation capability, but it has practical limitations [41], [42]. Constructing protocol flaws requires substantial manual effort, and real-world vulnerabilities are often covert, making handcrafted mutants unlikely to cover the full spectrum of lemma capability. Moreover, flipbased outcomes provide limited visibility into the verifier’s fine-grained proof search behavior. Therefore, we use mutation testing here only as supporting evidence for the rationality of CRO ST, rather than as our primary evaluation metric [43].
Protocol Rules
Vulnerability injection
Generated Security Property
Mutation Protocol Rules
lemma A: verified lemma B: falsified
flip !
Re-verify
Generated Security Property lemma A: verified lemma B: verified
Formal verification
Generated Security Property lemma A: verified lemma B: verified
Fig. 7. Mutation test experiment sketch.
RQ2. How effective is CRoST as an evaluation metric? In section III, we prove the relationship between CRoST and security properties similarity. Furthermore, we designed mutation experiments [39] to further prove the rationality of CRoST.
We tested lemmas generated by current state-of-the-art (SOTA) LLMs. Figure 8 shows a strong positive correlation between CRoST coverage and flip rate (correlation coefficient = 0.75, p-value = 0.005). This evidence supports the validity of CRoST as a fine-grained, tool-grounded indicator for how well generated lemmas capture security properties.
TABLE II S IMPLE MODIFICATIONS TO CONSTRUCT VULNERABLE PROTOCOL VARIANTS .
Type
Operation description
Direct leakage
Add Out(...) to directly release a secret value. Weak key derivation Modify key-derivation inputs to include public constants, making the derived key predictable/computable by the adversary. Removed Delete signature/MAC verification guards verification (e.g., dropping an Eq(verify(...), true)-style check), enabling message forgery. Weakened binding Break identity/nonce binding by replacing a bound variable with an unconstrained one. Missing freshness Remove freshness-related checks so that recheck played messages can be accepted without detection. Incomplete message Remove authentication-critical fields (e.g., a nonce) from transmitted messages, preventing the receiver from validating sanity/freshness. Broken message Change message tags/formats so expected flow parsing/transition rules no longer match, disrupting sanity. Missing response Directly delete a required output/response.
Fig. 9. Lemma count vs. CRO ST. Each point is an LLM.
from 239 to 2672, while CRO ST improves by only about 24 percentage points and largely plateaus after the 8th run. This indicates diminishing returns and coverage saturation: additional sampling mainly produces redundant or weak variants that contribute little new solve-path coverage. Therefore, improving CSPV performance requires generating more informative lemmas that contribute incremental solve-path coverage, rather than increasing the raw number of candidates.
Fig. 10. Cumulative sampling and CRO ST.
Fig. 8. CRoST coverage vs. lemma flip rate under mutation testing.
RQ3. What are the capability boundaries of LLMs in CSPV? With the validity of CRO ST established in RQ2, we next examine the capability boundary of LLMs in CSPV. A natural hypothesis is that higher CRO ST scores may be driven mainly by generating more lemmas, i.e., stronger models simply explore more candidates and thus cover more solve-tree paths [44]. Figure 9 evaluates the relationship between the number of generated lemmas and CRO ST. We observe less correlation with substantial dispersion (p-value = 0.04825). This suggests that CSPV capability differences are not explained primarily by lemma quantity. To further probe the boundary under repeated sampling, we run the same pipeline multiple times with a fixed LLM deepseek-v3.2 and track cumulative statistics (Figure 10). Across 12 iterations, cumulative generated lemmas increase
RQ4. How do LLMs perform across different task types in CSPV? We treat major security-attribute families as distinct task types in CSPV (secrecy, authentication, and sanity), and report per-task CRO ST to characterize capability differences and model biases across tasks. The results in Table III indicate that, on average, SOTA LLMs perform better on authentication and sanity properties than on secrecy properties. Figure 11 offers a different, lemmalevel perspective. The highest-scoring target lemmas are disproportionately concentrated in sanity properties. A plausible explanation is that secrecy and authentication properties are often expressed as all-traces universally quantified lemmas, whereas sanity properties are more commonly formulated as exists-trace existential lemmas. This suggests that current LLMs are generally more effective at generating existential security properties than universally quantified ones. To understand the failure modes of SOTA LLMs, we conduct a focused case study on the top4 LLMs by overall CRO ST (claude-sonnet-4.5, claude-opus-4.5, gemini-3-flash-
Fig. 11. Top4 LLMs’ CRO ST on target lemma.
TABLE IV AVERAGE OUTPUT TOKENS PER CALL .
TABLE III CRO ST BY S ECURITY P ROPERTY (%).
Model claude-sonnet-4.5 claude-opus-4.5 gemini-3-flash-preview deepseek-v3.2 top4 LLMs qwen3.5-plus gpt-5.2-codex gpt-5.2 claude-haiku-4.5 grok-4 qwen3-coder-plus gpt-4 qwen-plus
Overall Secrecy Authentication Sanity
LLM
46.11 35.94 29.36 27.46 38.82 25.37 24.91 22.60 22.46 15.63 12.46 6.28 5.28
claude-sonnet-4.5 claude-opus-4.5 gemini-3-flash-preview deepseek-v3.2
30.91 42.10 35.78 20.51 33.90 9.32 27.50 14.87 8.44 14.87 7.07 6.67 2.54
55.85 20.02 24.28 24.25 40.56 36.48 21.55 25.98 19.90 7.32 21.24 3.24 6.83
39.97 39.83 30.74 35.47 39.95 28.34 20.78 27.44 35.89 22.85 5.37 3.54 6.40
Avg Output Tokens 1143 691 455 844
AcceptS (phase 1), instead of the target AcceptP (phase 1) to AcceptS (phase 1), and forgets the temporal relationship. This phase mismatch breaks the intended correspondence structure. Client
Server
AcceptP
AcceptS
AcceptP2
AcceptS2
correct order
preview, and deepseek-v3.2), and analyze representative failures on lemma generation. Case study. Stage point confusion in large protocols. To concretely illustrate failure modes of LLMs to generate lemma, we present a case study on the multi-phase Authenticated Key Exchange (AKE) protocol SSH-R. Its target properties are bound to stage-specific action facts. In SSH-R, client-side authentication proceeds in two stages: the first stage is marked by the action fact AcceptP and corresponds to transport-layer key exchange plus server authentication, while the second stage is marked by AcceptP2 and corresponds to user authentication plus final key confirmation. Accordingly, the target lemmas are stage-specific rather than generic agreement templates: AcceptP (phase 1) is bound to a prior AcceptS witness, AcceptS2 (phase 2) is bound to a prior AcceptP2. We observed that the generated lemmas still demonstrate a reasonable understanding of the roles of action facts. That is, LLMs are often able to distinguish whether an action fact corresponds to key establishment, authentication, or message confirmation, and thus tend to preserve the high-level functional intent of the protocol. More importantly, however, LLMs also exhibit a representative form of stage-point confusion in generated lemmas. In Figure 12, while the LLM captures the high-level intent of agreement/authentication, it misaligns stage points by relating AcceptP2 (phase 2) to
LLMs failure order
Fig. 12. Example of an LLM failure mode in the basic SSH protocol.
This issue is particularly damaging for large protocols with many phase-specific action facts induced by multi-round message flows and composed cryptographic primitives. A single stage point mix-up can prevent proof search from reaching the target solve-tree paths, resulting in substantial coverage loss for the affected lemma family. This case study indicates that current LLMs often fail to precisely align stage-specific events with their temporal constraints, which makes them struggle with CSPV tasks on more complex protocols. RQ5. What is the computational cost of using LLMs in CSPV? We measure cost from two aspects: (i) LLM token output during lemma generation, and (ii) runtime for formally verifying generated lemmas. All experiments were executed on Intel(R) Core(TM) i9-14900 (2.00 GHz), 24 cores, 32GB RAM, with Tamarin configured as +RTS -N -RTS --auto-sources [16]. For token accounting, we use the Python tiktoken library for consistent counting across LLMs. The prompt length is fixed at 1049 tokens for all calls; Table IV reports average output tokens only. For runtime, we report the total time spent verifying generated lemmas, and compare it against verifying the original
target lemmas as a baseline. Formal analysis of realistic protocol LLMs can be time- and memory-intensive, making verification runtime a key usability factor for CSPV.
Third, for real-world vulnerability discovery, an additional step is needed to provide counterexample explanation. Fourth, incorporating richer features of protocols and security properties may further improve LLM-based lemma TABLE V generation. Our current study is only a preliminary evaluation V ERIFICATION RUNTIME OF GENERATED LEMMAS . and does not introduce additional protocol-level or propertySetting Lemmas Total Time (s) Mean (s/lemma) level features, leaving this as an important direction for future work. Baseline (target lemmas) 91 59.91 0.66 claude-sonnet-4.5 claude-opus-4.5 gemini-3-flash-preview deepseek-v3.2
245 166 95 230
1267.76 1127.33 238.24 1151.46
5.17 6.79 2.51 5.01
Compared to the baseline, verifying generated lemmas incurs roughly a 4×−21× slowdown. This suggests that, beyond generation cost, the dominant overhead in CSPV can stem from verification attempts on incorrect or low-utility lemmas. Improving lemma quality to reduce wasted verification effort (e.g., by increasing effective coverage gains) is therefore an important direction. The mean per-lemma verification time also increases from 0.66s to 2.51–6.79s, indicating that generated lemmas also tend to induce longer formal proof-search cost per lemma. C. Threats to Validity External validity. Our benchmark covers 18 protocols and three major property families: secrecy, authentication, and sanity. However, protocol complexity and property distribution may affect the observed results, especially in RQ4 where we compare model performance across different security-property types. Therefore, the results may not fully generalize to larger protocol collections or to property families not covered by our benchmark. Internal validity. LLM-based lemma generation is sensitive to prompt design, in-context examples, and decoding randomness. Although we use a unified prompting strategy and the same evaluation pipeline across models, the inherent randomness of LLM generation may still introduce variability in the generated lemmas and the resulting CRoST scores. V. D ISCUSSION A. Future work Our findings suggest several directions for future work. First, CRoST can still produce false positives when proof paths contain common low-information solve items, such as solve(!KU(x)); an unrelated generated lemma may cover the target lemma at such points. Future work can introduce stricter constraints into CRoST computation—such as semantic-category filtering of solve items, context-consistency checks, or minimum-information thresholds—to reduce erroneous matches on common solve items and obtain more precise coverage estimates. Second, scaling CSPV to large, complex protocols requires addressing stage point confusion: future methods should explicitly represent protocol phase structure and constrain generated correspondence lemmas to align stage-specific events and temporal relations with protocol semantics.
VI. R ELATED W ORK Automatic security proofs for cryptographic protocols are not a new research problem [45]. Symbolic protocol verifiers provide some basic automation, but it is largely limited to coarse, pre-defined property templates rather than scenariospecific, high-level guarantees. For example, Scyther [46] can automatically instantiate generic secrecy and authentication claims for protocol variables and locally generated values, enabling basic checks without fully hand-writing every claim. But this automation is largely confined to generic, coarse-grained security goals and does not address scenario-specific, complex protocols. Similarly, Tamarin [16] supports automation aimed at proof scalability, such as auto-sources lemmas that are automatically generated to facilitate proving secrecy of protected subterms (e.g., secrets occurring under hashes/encryptions) and to mitigate proof-search blowups due to partial deconstructions [17], [47]. However, such automation primarily targets proof-search scalability and does not resolve the central property-engineering challenge: deciding which high-level guarantees should be verified in a given scenario and encoding them precisely as tool-checkable lemmas that are provable or refutable under the chosen protocol model and verification setting. Recent work has begun to combine LLMs with symbolic protocol verification to reduce the modeling barrier, i.e., generating tool-checkable symbolic models directly from naturallanguage protocol descriptions. [14] studies how to synthesize symbolic protocol models (centered on SAPIC+ and multiset rewriting rules) from natural-language documents via a staged pipeline with formally constrained transformations. This line of work primarily targets the generation of protocol rewriting rules (model construction), rather than the generation of security properties/lemmas (property engineering). CryptoFormalEval [48] provides a simple evaluation of LLMs in symbolic reasoning. However, they do not provide a method for leveraging LLM capabilities beyond syntax, so their results remain at the level of syntax correctness. Complementary to those directions, our work focuses on the setting where the protocol model is already available and examines how well LLMs can generate tool-checkable lemmas. VII. C ONCLUSION Our work shows that few-shot prompting is often necessary to obtain syntactically valid Tamarin lemmas; CRO ST varies substantially across LLMs and property families, and complex
multi-phase protocols exhibit recurrent failure modes such as stage point confusion. Moreover, under fixed prompting and pipeline settings, increasing the number of generated lemmas yields diminishing returns and coverage saturation. Finally, verifying LLM-generated lemmas incurs substantially higher runtime than verifying baseline target lemmas, highlighting verification cost as a practical constraint. DATA AVAILABILITY The data supporting the results of this paper are publicly available at Zenodo2 . R EFERENCES [1] C. Cremers, C. Jacomme, and A. Naska, “Formal analysis of sessionhandling in secure messaging: lifting security from sessions to conversations,” in Proceedings of the 32nd USENIX Conference on Security Symposium, ser. SEC ’23. USA: USENIX Association, 2023. [2] X. Liu, C. Zuo, Q. Hou, P. Ren, J. Wu, Q. Zhao, and S. Guo, “A thorough security analysis of ble proximity tracking protocols,” in Proceedings of the 34th USENIX Conference on Security Symposium, ser. SEC ’25. USA: USENIX Association, 2025. [3] D. Basin, R. Sasse, and J. Toro-Pozo, “The emv standard: Break, fix, verify,” in 2021 IEEE Symposium on Security and Privacy (SP), 2021, pp. 1766–1781. [4] S. Andova, C. Cremers, K. Gjøsteen, S. Mauw, S. F. Mjølsnes, and S. Radomirović, “A framework for compositional verification of security protocols,” Inf. Comput., vol. 206, no. 2–4, p. 425–459, Feb. 2008. [Online]. Available: https://doi.org/10.1016/j.ic.2007.07.002 [5] C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe, “A comprehensive symbolic analysis of tls 1.3,” in Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, ser. CCS ’17. New York, NY, USA: Association for Computing Machinery, 2017, p. 1773–1788. [Online]. Available: https://doi.org/10.1145/3133956.3134063 [6] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, “Hacl*: A verified modern cryptographic library,” in Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, ser. CCS ’17. New York, NY, USA: Association for Computing Machinery, 2017, p. 1789–1806. [Online]. Available: https://doi.org/10.1145/3133956.3134043 [7] C. Cremers, A. Dax, and A. Naska, “Formal analysis of spdm: security protocol and data model version 1.2,” in Proceedings of the 32nd USENIX Conference on Security Symposium, ser. SEC ’23. USA: USENIX Association, 2023. [8] M. Dodds, “Formally verifying industry cryptography,” IEEE Security & Privacy, vol. 20, no. 3, pp. 65–70, 2022. [9] L. Pan, A. Albalak, X. Wang, and W. Wang, “Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning,” in Findings of the Association for Computational Linguistics: EMNLP 2023, H. Bouamor, J. Pino, and K. Bali, Eds. Singapore: Association for Computational Linguistics, Dec. 2023, pp. 3806–3824. [Online]. Available: https://aclanthology.org/2023.findings-emnlp.248/ [10] K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “Leandojo: Theorem proving with retrieval-augmented language models,” in Advances in Neural Information Processing Systems, A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, Eds., vol. 36. Curran Associates, Inc., 2023, pp. 21 573–21 612. [Online]. Available: https://proceedings.neurips.cc/paper files/paper/ 2023/file/4441469427094f8873d0fecb0c4e1cee-Paper-Datasets and Benchmarks.pdf [11] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and I. Polosukhin, “Attention is all you need,” in Proceedings of the 31st International Conference on Neural Information Processing Systems, ser. NIPS’17. Red Hook, NY, USA: Curran Associates Inc., 2017, p. 6000–6010. 2 https://doi.org/10.5281/zenodo.20996406
[12] J. M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. Polu, “Proof artifact co-training for theorem proving with language models,” in The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. [Online]. Available: https://openreview.net/forum?id=rpxJc9j04U [13] A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu, “Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,” in The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. [Online]. Available: https://openreview.net/forum?id=SMa9EAovKMC [14] Z. Mao, J. Wang, J. Sun, S. Qin, and J. Xiong, “Llm-aided automatic modeling for security protocol verification,” in Proceedings of the IEEE/ACM 47th International Conference on Software Engineering, ser. ICSE ’25. IEEE Press, 2025, p. 642–654. [Online]. Available: https://doi.org/10.1109/ICSE55347.2025.00197 [15] S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The tamarin prover for the symbolic analysis of security protocols,” in Computer Aided Verification, N. Sharygina and H. Veith, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 696–701. [16] The Tamarin Team, Tamarin Prover Manual, Tamarin Prover Project, 2024. [Online]. Available: https://tamarin-prover.com/manual/ [17] V. Cortier, S. Delaune, and J. Dreier, “Automatic generation of sources lemmas in tamarin: Towards automatic proofs of security protocols,” in Computer Security – ESORICS 2020, L. Chen, N. Li, K. Liang, and S. Schneider, Eds. Cham: Springer International Publishing, 2020, pp. 3–22. [18] S. Celi, J. Hoyland, D. Stebila, and T. Wiggers, “A tale of two models: Formal verification of kemtls via tamarin,” in Computer Security – ESORICS 2022, V. Atluri, R. Di Pietro, C. D. Jensen, and W. Meng, Eds. Cham: Springer Nature Switzerland, 2022, pp. 63–83. [19] Z. Ma, C. Wen, Z. Su, X. Liang, C. Tian, S. Qin, and M. Yang, “Bridging natural language and formal specification–automated translation of software requirements to ltl via hierarchical semantics decomposition using llms,” in 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2025, pp. 1208–1220. [20] R. Castaño, V. Braberman, D. Garbervetsky, and S. Uchitel, “Model checker execution reports,” in 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2017, pp. 200– 205. [21] D. Dolev and A. Yao, “On the security of public key protocols,” IEEE Trans. Inf. Theor., vol. 29, no. 2, p. 198–208, Sep. 2006. [Online]. Available: https://doi.org/10.1109/TIT.1983.1056650 [22] B. Blanchet, “Security protocol verification: Symbolic and computational models,” in Principles of Security and Trust, P. Degano and J. D. Guttman, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 3–29. [23] G. Lowe, “A hierarchy of authentication specifications,” in Proceedings 10th Computer Security Foundations Workshop, 1997, pp. 31–43. [24] B. Schmidt, “Formal analysis of key exchange protocols and physical protocols,” PhD thesis, ETH Zurich, 2012. [Online]. Available: https://doi.org/10.3929/ethz-a-009898924 [25] B. Schmidt, S. Meier, C. Cremers, and D. Basin, “Automated analysis of diffie-hellman protocols and advanced security properties,” in 2012 IEEE 25th Computer Security Foundations Symposium, 2012, pp. 78–94. [26] C. Cremers. (2024) Security protocol analysis tools. [Online]. Available: https://people.cispa.io/cas.cremers/tools/index.html [27] V. Cheval, C. Jacomme, S. Kremer, and R. Künnemann, “SAPIC+: protocol verifiers of the world, unite!” in 31st USENIX Security Symposium (USENIX Security 22). Boston, MA: USENIX Association, Aug. 2022, pp. 3935–3952. [Online]. Available: https://www.usenix. org/conference/usenixsecurity22/presentation/cheval [28] K. Papineni, S. Roukos, T. Ward, and W.-J. Zhu, “Bleu: a method for automatic evaluation of machine translation,” in Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, P. Isabelle, E. Charniak, and D. Lin, Eds. Philadelphia, Pennsylvania, USA: Association for Computational Linguistics, Jul. 2002, pp. 311–318. [Online]. Available: https://aclanthology.org/P02-1040/ [29] M. Evtikhiev, E. Bogomolov, Y. Sokolov, and T. Bryksin, “Out of the bleu: how should we assess quality of the code generation models?” J. Syst. Softw., vol. 203, p. 111741, 2022. [Online]. Available: https://api.semanticscholar.org/CorpusID:251371647 [30] Y. Yang, S. Xiong, A. Payani, E. Shareghi, and F. Fekri, “Harnessing the power of large language models for natural language to first-order
logic translation,” in Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), L.-W. Ku, A. Martins, and V. Srikumar, Eds. Bangkok, Thailand: Association for Computational Linguistics, Aug. 2024, pp. 6942–6959. [Online]. Available: https://aclanthology.org/2024.acl-long.375/ [31] E. Ghassabani, A. Gacek, M. W. Whalen, M. P. E. Heimdahl, and L. Wagner, “Proof-based coverage metrics for formal verification,” in Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’17. IEEE Press, 2017, p. 194–199. [32] N. Tihanyi, Y. Charalambous, R. Jain, M. A. Ferrag, and L. C. Cordeiro, “A new era in software security: Towards self-healing software via large language models and formal verification,” in 2025 IEEE/ACM International Conference on Automation of Software Test (AST), 2025, pp. 136–147. [33] D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, T. Lemberger, and M. Tautschnig, “Verification witnesses,” ACM Trans. Softw. Eng. Methodol., vol. 31, no. 4, Sep. 2022. [Online]. Available: https://doi.org/10.1145/3477579 [34] X. Ke, A. Khan, and L. L. H. Quan, “An in-depth comparison of s-t reliability algorithms over uncertain graphs,” Proc. VLDB Endow., vol. 12, no. 8, p. 864–876, Apr. 2019. [Online]. Available: https://doi.org/10.14778/3324301.3324304 [35] G. Tuccio, L. Bulla, M. Madonia, A. Gangemi, and M. Mongiovı̀, “GRAMMAR-LLM: Grammar-constrained natural language generation,” in Findings of the Association for Computational Linguistics: ACL 2025, W. Che, J. Nabende, E. Shutova, and M. T. Pilehvar, Eds. Vienna, Austria: Association for Computational Linguistics, Jul. 2025, pp. 3412–3422. [Online]. Available: https://aclanthology.org/2025.findings-acl.177/ [36] F. Jiao, Z. Teng, B. Ding, Z. Liu, N. Chen, and S. Joty, “Exploring self-supervised logic-enhanced training for large language models,” in Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), K. Duh, H. Gomez, and S. Bethard, Eds. Mexico City, Mexico: Association for Computational Linguistics, Jun. 2024, pp. 926–941. [Online]. Available: https://aclanthology.org/2024.naacl-long.53/ [37] T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. HerbertVoss, G. Krueger, T. Henighan, R. Child, A. Ramesh, D. M. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C. Berner, S. McCandlish, A. Radford, I. Sutskever, and D. Amodei, “Language models are few-shot learners,” in Proceedings of the 34th International Conference on Neural Information Processing Systems, ser. NIPS ’20. Red Hook, NY, USA: Curran Associates Inc., 2020. [38] S. Min, X. Lyu, A. Holtzman, M. Artetxe, M. Lewis, H. Hajishirzi, and L. Zettlemoyer, “Rethinking the role of demonstrations: What makes in-context learning work?” in Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, Y. Goldberg, Z. Kozareva, and Y. Zhang, Eds. Abu Dhabi, United Arab Emirates: Association for Computational Linguistics, Dec. 2022, pp. 11 048– 11 064. [Online]. Available: https://aclanthology.org/2022.emnlp-main. 759/ [39] M. Krichen, “A survey on mutation testing,” in Bio-Inspired Computing, V. Sakalauskas, A. Bajaj, A. Abraham, K. R. Madhavi, and P. Manghirmalani Mishra, Eds. Cham: Springer Nature Switzerland, 2025, pp. 210–219. [40] S. J. Kaufman, R. Featherman, J. Alvin, B. Kurtz, P. Ammann, and R. Just, “Prioritizing mutants to guide mutation testing,” in 2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE), 2022, pp. 1743–1754. [41] R. Just, D. Jalali, L. Inozemtseva, M. D. Ernst, R. Holmes, and G. Fraser, “Are mutants a valid substitute for real faults in software testing?” in Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, ser. FSE 2014. New York, NY, USA: Association for Computing Machinery, 2014, p. 654–665. [Online]. Available: https://doi.org/10.1145/2635868.2635929 [42] M. Papadakis, D. Shin, S. Yoo, and D.-H. Bae, “Are mutation scores correlated with real fault detection? a large scale empirical study on the relationship between mutants and real faults,” in 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), 2018, pp. 537–548.
[43] Y. T. Chen, R. Gopinath, A. Tadakamalla, M. D. Ernst, R. Holmes, G. Fraser, P. Ammann, and R. Just, “Revisiting the relationship between fault detection, test adequacy criteria, and test set size,” in Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’20. New York, NY, USA: Association for Computing Machinery, 2021, p. 237–249. [Online]. Available: https://doi.org/10.1145/3324884.3416667 [44] J. Kaplan, S. McCandlish, T. Henighan, T. B. Brown, B. Chess, R. Child, S. Gray, A. Radford, J. Wu, and D. Amodei, “Scaling laws for neural language models,” ArXiv, vol. abs/2001.08361, 2020. [Online]. Available: https://api.semanticscholar.org/CorpusID:210861095 [45] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. H. Drielsma, P. C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron, “The avispa tool for the automated validation of internet security protocols and applications,” in Computer Aided Verification, K. Etessami and S. K. Rajamani, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 281–285. [46] C. J. F. Cremers, “The scyther tool: Verification, falsification, and analysis of security protocols,” in Computer Aided Verification, A. Gupta and S. Malik, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 414–418. [47] D. Basin, J. Dreier, and R. Sasse, “Automated symbolic proofs of observational equivalence,” in Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, ser. CCS ’15. New York, NY, USA: Association for Computing Machinery, 2015, p. 1144–1155. [Online]. Available: https://doi.org/10.1145/2810103. 2813662 [48] C. Curaba, D. Denis, and A. Minisini, “Cryptoformaleval: Integrating large language models and formal verification for automated cryptographic protocol vulnerability detection,” in The First Workshop on System-2 Reasoning at Scale, NeurIPS’24, 2024. [Online]. Available: https://openreview.net/forum?id=hqvJT2pOxu