.png){kind=icon}
返回
Evaluating Large Language Models for Symbolic Security Protocol Analysis
.png){kind=icon}
OA
AI
DOI：10.3390/electronics15184141.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
安全协议验证依赖于形式化工具，如ProVerif和OFMC。本研究评估大型语言模型（LLMs）能否执行类似分析。我们在130个经过混淆的AnB/AnBx协议上对GPT和DeepSeek进行三轮测试，覆盖388个安全目标，并与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%。自报置信度普遍较高，但与正确性无显著相关性。所有结果基于单一零样本提示和两个模型提供者，限制了泛化性。在此基准上，LLMs未达到形式化验证水平，但可能作为预筛选过滤器使用。
Keyword:
security protocols
verification
large language models
