用大模型检测安全协议漏洞，效果不如专业工具，但可做初步筛查。
Evaluating Large Language Models for Symbolic Security Protocol Analysis
- 对比GPT和DeepSeek在对话与推理模式下分析130个混淆协议
- 推理模式精度最高达66.5%，但仅发现一半攻击，认证类漏洞检出率不足50%
- 适合需要快速初筛的开发者，不适用于关键系统验证
安全协议验证依赖ProVerif和OFMC等形式化工具。本研究评估大语言模型（LLMs）是否能实现类似分析。我们在130个混淆的AnB/AnBx协议上，对GPT和DeepSeek在对话与推理模式下进行三轮测试，覆盖388个安全目标，结果以ProVerif和OFMC为基准。对话模型召回率69%~81%，精度低于31%；推理模型将精度提升至GPT 66.5%、DeepSeek 45.4%，但仅检测到超过一半的攻击。尽管两版本模型共享同一基础架构，推理模式仍使精度从27.2%提升至45.4%。对于认证类目标，推理模型检出率均不足50%，而对话模型误报严重；保密性表现最优，推理模式下F1达95.7%。模型判断一致性差：GPT在89.7%目标上保持一致，DeepSeek仅为74.0%。模型自评信心普遍高，但与正确性无显著相关。在该基准上，当前大模型尚未达到形式化验证水平，最多可作为预筛选工具。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。