# Evaluating Large Language Models for Symbolic Security Protocol Analysis

arXiv: https://arxiv.org/abs/2607.20712 · HTML: https://mlsanity.com/paper/2607.20712/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 56 references that are in the map.
- First posted on arXiv 22 Jul 2026.

## Builds on (most cited first, 18 of 18)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT](https://mlsanity.com/paper/2302.11382/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [A Survey on Large Language Model (LLM) Security and Privacy: The Good, the Bad, and the Ugly](https://mlsanity.com/paper/2312.02003/) (2023)
- [NLP Evaluation in trouble: On the Need to Measure LLM Data Contamination for each Benchmark](https://mlsanity.com/paper/2310.18018/) (2023)
- [Data Contamination: From Memorization to Exploitation](https://mlsanity.com/paper/2203.08242/) (2022)
- [Chain-of-Thought Reasoning Without Prompting](https://mlsanity.com/paper/2402.10200/) (2024)
- [Many-Shot In-Context Learning](https://mlsanity.com/paper/2404.11018/) (2024)
- [Uncertainty Quantification and Confidence Calibration in Large Language Models: A Survey](https://mlsanity.com/paper/2503.15850/) (2025)
- [A Survey on Large Language Models for Mathematical Reasoning](https://mlsanity.com/paper/2506.08446/) (2025)
- [Prompt-Enhanced Software Vulnerability Detection Using ChatGPT](https://mlsanity.com/paper/2308.12697/) (2023)
- [LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights](https://mlsanity.com/paper/2502.07049/) (2025)
- [Chain-of-Thought Prompting of Large Language Models for Discovering and Fixing Software Vulnerabilities](https://mlsanity.com/paper/2402.17230/) (2024)
- [Beyond Majority Voting: LLM Aggregation by Leveraging Higher-Order Information](https://mlsanity.com/paper/2510.01499/) (2025)
- [To Ensemble or Not: Assessing Majority Voting Strategies for Phishing Detection with Large Language Models](https://mlsanity.com/paper/2412.00166/) (2024)
- [Thinking Before Constraining: A Unified Decoding Framework for Large Language Models](https://mlsanity.com/paper/2601.07525/) (2026)
- [CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes](https://mlsanity.com/paper/2606.25561/) (2026)

## Abstract (arXiv)

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.