摘要
安全协议验证依赖于ProVerif和OFMC等形式化工具。本研究评估了大型语言模型（LLM）是否能够进行相当的分析。我们在三次运行中，对130个经过混淆处理的AnB/AnBx协议（涵盖388个安全目标）分别使用GPT和DeepSeek的对话模式和推理模式进行了测试，并以ProVerif和OFMC的结果作为评分标准。每个提供商在两种模式下使用同一个模型，仅切换推理开关，因此两种对比均能单独隔离推理本身的影响。对话模式下，GPT的召回率为72.7%、精确率为27.3%，DeepSeek的召回率为69.3%、精确率为27.2%。推理模式则反转了这一权衡，GPT达到66.5%的精确率和54.5%的召回率，DeepSeek达到45.4%的精确率和57.3%的召回率。启用推理后，在综合判定上，GPT的精确率从27.3%提升至64.8%，DeepSeek从27.2%提升至44.4%。目标集合存在不平衡，89个脆弱目标对应299个安全目标；一个始终预测为安全的平凡预测器可得77.1%的准确率，仅有GPT推理模式超过了这一水平。所有模型在认证目标上表现最差：推理模式对单射和非单射一致性攻击的检测率均低于一半，而对话模式则在低精确率下过度标记这些攻击。机密性目标则是例外，推理模式下F1值高达95.7%。判定结果在各次运行间不稳定：GPT推理模式在89.7%的目标上判定一致，DeepSeek推理模式为74.0%，GPT对话模式为70.1%，DeepSeek对话模式为61.6%。各模型自我报告的置信度普遍偏高，但与正确性之间没有显著相关性。所有结果均基于单次零样本提示和两个模型提供商，这在一定程度上限制了泛化能力。在该基准测试中，LLM尚未达到形式化验证的水平，但最好也只能作为预筛选过滤器使用。
