Evaluating Large Language Models for Symbolic Security Protocol Analysis

Source: arXiv:2607.20712 · Published 2026-07-22 · By Paolo Modesti, Syed Ahmed, Ioannis Sfyrakis, Derek Enodolomwanyi

TL;DR

This paper evaluates whether state-of-the-art Large Language Models (LLMs), specifically OpenAI GPT and DeepSeek, can perform symbolic security protocol analysis comparable to traditional formal verification tools like ProVerif and OFMC. The authors test models in both chat mode and a dedicated reasoning mode on a dataset of 130 obfuscated AnB/AnBx protocols comprising 388 security goals. They find that chat models achieve high recall (69-81%) but low precision (<31%), while reasoning models improve precision (up to 66.5% for GPT) but recall drops to about 50%. Authentication goals are the hardest for LLMs, especially injective/non-injective agreement, with under half of attacks detected. Confidentiality goals are an exception with reasoning models reaching F1 scores as high as 95.7%. Verdict stability varies, with GPT showing 89.7% inter-run agreement and DeepSeek 74.0%. Self-reported confidence of models is uniformly high but poorly calibrated to correctness. Overall, LLMs fall short of formal verification tools, and at best could be used as preliminary pre-screening filters to prioritize formal analysis.

Key findings

• Chat-mode LLMs achieve recall between 69% to 81% but precision below 31%, resulting in many false positives.
• Reasoning-mode LLMs trade recall for precision, with GPT reaching 66.5% precision and DeepSeek 45.4%, but detect just over half the attacks.
• DeepSeek’s reasoning mode raises precision from 27.2% (chat) to 45.4% while recall drops from 69.3% to just over 50%.
• LLMs perform worst on authentication goals, detecting under 50% of injective and non-injective agreement attacks.
• Confidentiality goals achieve high performance, with reasoning-mode LLMs reaching F1 scores up to 95.7%.
• Verdicts are unstable across runs, identical on 89.7% of goals for GPT but only 74.0% for DeepSeek.
• LLM self-reported confidence scores are mostly high (94-99%) even on incorrect or missed attacks, showing poor calibration.
• Formal tools ProVerif and OFMC exhibit over 94% agreement on ground-truth labels where coverage overlaps, supporting the benchmark reliability.

Threat model

The adversary assumed is the standard Dolev-Yao symbolic intruder who fully controls the network, intercepting, injecting, and modifying messages arbitrarily. The intruder cannot break underlying cryptography but can apply all symbolic deduction rules (public key encryption, symmetric keys, hashing). The models verify security goals under this attacker assumption. The LLM adversary model is implicit: the LLM must reason symbolically about protocol specifications without direct cryptographic attacks or oracle access. Importantly, the LLM is tested on obfuscated protocol specifications to prevent recognition-based shortcuts.

Methodology — deep read

The authors evaluate LLMs as symbolic security protocol verifiers, comparing their verdicts to state-of-the-art formal tools ProVerif and OFMC under the Dolev-Yao adversary model. The threat model assumes a powerful symbolic network intruder controlling communications but cannot break cryptography. The dataset comprises 130 canonical and industrial security protocols specified in AnB/AnBx notation, with 388 distinct security goals covering confidentiality and two types of authentication agreements. To avoid potential test leakage from known protocols, the specifications are obfuscated with type-aware renaming that preserves structure but removes identifier semantics. Ground truth is derived primarily from ProVerif results, augmented by OFMC one- and two-session runs where ProVerif is inconclusive, following a waterfall priority scheme.

Two LLM providers (OpenAI and DeepSeek) are tested in two modes each: chat mode (direct answers) and reasoning mode (chain-of-thought intermediate steps). GPT-5.2 and DeepSeek v4 Flash serve as chat models; GPT-5.4 and DeepSeek v4 Flash (reasoner endpoint) as reasoning models. Zero-shot prompting with a comprehensive system message defines the Dolev-Yao semantics, cryptographic operators, security goal types, and demands strictly formatted JSON outputs (goal_id, status, confidence, justification, optional 2-session trace). No few-shot examples are used, requiring the models to apply learned reasoning from training.

Each protocol is sent to the models via an automated Python pipeline that submits anonymized prompts and collects JSON verdicts. The pipeline pairs each LLM verdict with the formal ground truth and computes confusion matrix metrics: precision, recall, accuracy, F1-score, with emphasis on recall due to the high cost of missed attacks (false negatives). Evaluation runs are repeated thrice independently per model configuration to capture LLM output variability. Results are aggregated with cluster bootstrap over protocols to produce 95% confidence intervals, accounting for intra-protocol goal correlations.

The pipeline also assesses self-reported confidence calibration by grouping results by confidence bands and comparing accuracy within intervals. Inter-run consistency statistics quantify verdict stability. The system uses temperature=0.1 for chat mode to improve stability and instructs reasoning modes to devote higher effort to internal chain-of-thought computations.

Evaluation metrics are computed for overall results as well as disaggregated by security goal categories—confidentiality, injective/non-injective authentication, and channel types. The study additionally analyzes patterns of persistent false positives and false negatives, and compares costs and latency. The implementation and evaluation code is publicly available.

In a typical trial, an obfuscated AnB/AnBx dataset entry specifying a protocol's message sequence and security goals is converted into a JSON prompt and submitted to the LLM. The model responds with a JSON verdict classifying each security goal as "attack found" or "no attack", accompanied by a confidence score and textual reasoning. These are programmatically matched against the formal tool verdicts which serve as the ground truth to compute performance metrics.

Technical innovations

• A novel automated pipeline integrating protocol obfuscation, zero-shot JSON prompting, and multi-run evaluation of LLMs for symbolic security protocol analysis against formal verification baselines.
• A rigorous empirical comparison of chat (direct answer) versus reasoning (chain-of-thought prompting) model configurations from two independent LLM providers on a standard 130-protocol security benchmark.
• Quantitative evidence that explicit chain-of-thought reasoning substantially raises LLM precision at the cost of recall in security verdicts, clarifying the differing failure modes of chat and reasoning modes.
• An analysis showing that LLM self-reported confidence scores have negligible calibration with respect to correctness in the security protocol verification context.

Datasets

• AnBx protocol library v2025.09 — 130 protocols, 388 security goals — Public library with canonical and industrial protocols

Baselines vs proposed

• ProVerif (ground truth): treated as definitive, with 94.1% agreement on overlapping goals with OFMC 1-session and 97.8% with OFMC 2-session
• DeepSeek Chat: recall = 69.3%, precision = 27.2% vs DeepSeek Reasoning: recall ~50%, precision = 45.4%
• GPT Chat: recall = 81.3%, precision = 28.9% vs GPT Reasoning: recall ~50%, precision = 66.5%
• LLMs detect <50% of injective/non-injective authentication attacks (e.g., 38.5% for GPT on injective agreement)
• Reasoning-mode F1 on confidentiality goals up to 95.7%

Limitations

• LLM verdict stability is imperfect; inter-run agreement is below 90% for DeepSeek and about 90% for GPT, indicating non-deterministic outputs.
• The dataset is fixed and mostly canonical; real-world protocol complexity and diversity may be higher.
• Only two LLM providers and specific model versions are evaluated; results may not generalize across other models or future versions.
• No adversarial protocol manipulation or prompt attack tested; robustness to adversarial inputs remains unknown.
• Evaluation is limited to symbolic Dolev-Yao model; cryptographic or computational soundness aspects are not considered.
• The prompt is zero-shot with no few-shot examples; alternative prompt designs might impact model performance but were not studied here.

Open questions / follow-ons

• Can training or fine-tuning on formal protocol verification data improve LLM precision and recall substantially beyond zero-shot performance?
• How might few-shot in-context examples or different prompt engineering strategies affect LLM analysis stability and accuracy?
• What approaches could calibrate or better quantify LLM uncertainty to filter out overconfident incorrect verdicts?
• Can LLM-based symbolic analysis be combined with formal tools in a hybrid system to prioritize manual analysis or guide proof search?

Why it matters for bot defense

For bot-defense engineers and CAPTCHA practitioners, this study highlights the current limits of LLMs in precise symbolic reasoning tasks related to security protocol analysis. While LLMs show promise in rapidly scanning large protocol sets and recalling many attacks (good sensitivity), their poor precision and overconfident false positives limit their reliability as standalone verifiers. This suggests that in security-sensitive applications, LLMs could serve as lightweight pre-filters flagging protocols or interactions for thorough formal or manual scrutiny, but not replacements for deterministic formal verification tools. The poor calibration of LLM self-reported confidence also warns against relying solely on model scores as trust indicators, implying that additional post-processing or cross-validation would be required. Overall, this research indicates LLMs are not yet mature enough for fully automated security decision-making but can augment human-in-the-loop analysis pipelines.

Cite

@article{arxiv2607_20712,
  title={ Evaluating Large Language Models for Symbolic Security Protocol Analysis },
  author={ Paolo Modesti and Syed Ahmed and Ioannis Sfyrakis and Derek Enodolomwanyi },
  journal={arXiv preprint arXiv:2607.20712},
  year={ 2026 },
  url={https://arxiv.org/abs/2607.20712}
}

Read the full paper

• arXiv:2607.20712 (abstract)
• arXiv:2607.20712 (PDF)