According to a new study published on arxiv.org, large language models do not yet match the capabilities of formal verification tools for analyzing security protocols. The research evaluated GPT and DeepSeek models in both chat and reasoning modes across three runs on 130 obfuscated protocols covering 388 security goals, comparing their performance against established tools ProVerif and OFMC.
The study found that chat models achieved 72.7% recall at 27.3% precision for GPT and 69.3% recall at 27.2% precision for DeepSeek. According to the paper, reasoning models reversed 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 mode lifted precision from 27.3% to 64.8% for GPT and from 27.2% to 44.4% for DeepSeek on consolidated verdicts.
The research notes that all models performed worst on authentication goals, with reasoning models detecting “well under half of injective and non-injective agreement attacks.” Confidentiality proved the exception, achieving F1 scores up to 95.7% in reasoning mode. Verdict stability varied significantly: identical results appeared on 89.7% of goals for GPT reasoning but only 61.6% for DeepSeek chat.
According to arxiv.org, the researchers concluded that “on this benchmark, LLMs do not match formal verification, but may serve, at best, as pre-screening filters.”