这篇论文用具体数据告诉你，GPT和DeepSeek在形式化验证上还比不上ProVerif这些专业工具，但推理模式能把精确率拉到66%，可能当个预筛选过滤器。
一篇论文评估了GPT和DeepSeek在符号安全协议分析中的能力，使用130个混淆的AnB/AnBx协议涵盖388个安全目标，与ProVerif和OFMC工具对比。Chat模式召回率69%-81%，但精确率低于31%。推理模式将GPT精确率提升至66.5%，DeepSeek至45.4%，但仅检测到一半以上攻击。在保密性目标上，推理模式F1达到95.7%。各模型在认证目标上表现最差，且判断不稳定。
Evaluating Large Language Models for Symbolic Security Protocol Analysis
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.