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.20712v1 Announce Type: cross Abstract: Security protocol 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. Chat models reach 69 to 81% recall at precision below 31%. Reasoning models reverse this trade-off, reaching 66.5% precision for GPT and 45.4% for DeepSeek, but detect just over half the attacks. DeepSeek's two modes share one underlying model, so the comparison isolates reasoning itself, which raises precision from 27.2% to 45.4%. The GPT contrast spans a model-version change and is only suggestive. 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 but 74.0% for DeepSeek. Self-reported confidence is uniformly high yet shows no meaningful correlation with correctness. On this benchmark LLMs do not match formal verification, but may serve, at best, as pre-screening filters.