Evaluating Large Language Models for Symbolic Security Protocol Analysis
Paolo Modesti, Syed Ahmed, Ioannis Sfyrakis, Derek Enodolomwanyi
Why It Matters
What makes this one worth your time
Understanding the capabilities and limitations of LLMs in security protocol analysis can guide future research and practical applications in cybersecurity.
LLMs show promise as pre-screening tools for security protocol analysis but fall short of formal verification standards.
Summary
This study evaluates the performance of Large Language Models (LLMs) in analyzing security protocols by comparing their results against established formal verification tools like ProVerif and OFMC across various security goals.
Key contributions
- A comparative analysis of LLMs against formal verification tools in the context of security protocol analysis.
- Quantitative performance metrics for LLMs in detecting security goals, including precision and recall rates.
- Insights into the limitations of LLMs, particularly in the context of authentication goals.
Notable insights
- The study reveals that reasoning models can significantly improve precision compared to chat models, highlighting the importance of model architecture in performance.
- The findings indicate that self-reported confidence levels of LLMs do not correlate with actual correctness, suggesting a need for better evaluation metrics.
Possible limitations
- The abstract does not address potential biases in the obfuscated protocols used for testing.
- The performance metrics may not generalize to other types of security protocols not covered in the study.
- Not stated in the abstract.
Abstract
arXiv:2607.20712v2 Announce Type: replace-cross Abstract: Security protocols verification relies on formal tools such as ProVerif and OFMC. This study evaluates whether large language models (LLMs) can perform comparable analysis. We test GPT and DeepSeek in chat and reasoning modes over three runs on 130 obfuscated AnB/AnBx protocols covering 388 security goals, scored against ProVerif and OFMC. Each provider uses a single model in both modes, switching reasoning on and off, so both contrasts isolate reasoning itself. Chat models achieve 72.7% recall at 27.3% precision for GPT and 69.3% recall at 27.2% precision for DeepSeek. Reasoning models reverse this trade-off, reaching 66.5% precision and 54.5% recall for GPT and 45.4% precision and 57.3% recall for DeepSeek. Enabling reasoning lifts precision from 27.3% to 64.8% for GPT and from 27.2% to 44.4% for DeepSeek on the consolidated verdict. The goal set is imbalanced, with 89 vulnerable goals against 299 secure ones; a trivial always-secure predictor scores 77.1% accuracy, which only GPT reasoning exceeds. All models perform worst on authentication goals: reasoning models detect well under half of injective and non-injective agreement attacks, whereas chat models over-flag them at low precision. Confidentiality is the exception, with F1 up to 95.7% in reasoning mode. Verdicts are unstable across runs: identical on 89.7% of goals for GPT reasoning, 74.0% for DeepSeek reasoning, 70.1% for GPT chat, and 61.6% for DeepSeek chat. Self-reported confidence is uniformly high yet shows no meaningful correlation with correctness. All results rest on a single zero-shot prompt and two model providers, which limits generalisability. On this benchmark, LLMs do not match formal verification, but may serve, at best, as pre-screening filters.