大模型
arxiv.org ·
评估大型语言模型在符号安全协议分析中的表现
该 arXiv 论文（v2，已发表于 Electronics 2026）以 ProVerif 和 OFMC 为基准，测试 GPT 与 DeepSeek 在 chat 与 reasoning 模式下对 130 个混淆 AnB/AnBx 协议、388 个安全目标的分析能力。结果显示：chat 模式召回高但精度低（GPT 72.7% recall / 27.3% precision），reasoning 模式转为精度高、召回低（GPT 66.5% precision / 54.5% recall）；恒判 secure 的平凡预测器准确率达 77.1%，仅 GPT reasoning 超过；认证类目标表现最差，机密性 F1 最高 95.7%；多次运行判定不稳定，自报置信度与正确性无显著相关。作者指出结果仅基于单一 zero-shot prompt 和两家模型提供商，泛化性有限，LLM 尚不能匹配形式化验证，最多可作预筛过滤器。
AI推荐理由 arXiv 论文（v2，2026-09-17 修订，已发表于 Electronics 2026, 15, 4141），对 GPT 与 DeepSeek 在 chat/reasoning 两种模式下分析 130 个混淆 AnB/AnBx 协议、388 个安全目标的表现做了可复现的量化评测，并以 ProVerif 和 OFMC 为基准。具体新信息包括：chat 模式高召回低精度（GPT 72.7% recall / 27.3% precision），reasoning 模式转为高精度低召回（GPT 66.5% precision / 54.5% recall）；目标集不平衡，恒判 secure 的平凡预测器准确率 77.1%，仅 GPT reasoning 超过；认证类目标表现最差，机密性 F1 最高 95.7%；多次运行判定不稳定（GPT reasoning 89.7% 一致，DeepSeek chat 仅 61.6%）；自报置信度与正确性无显著相关。局限明确：仅单一 zero-shot prompt、两家模型提供商，泛化性受限，结论是 LLM 尚不能替代形式化验证，最多可作预筛过滤器。对 AI 安全应用与 Agent 可靠性评估有参考价值，但非官方首发、非产品发布，故兴趣分未给更高。
78
正文
Computer Science > Cryptography and Security
arXiv:2607.20712 (cs)
[Submitted on 22 Jul 2026 (v1), last revised 17 Sep 2026 (this version, v2)]
Title:Evaluating Large Language Models for Symbolic Security Protocol Analysis
Authors:Paolo Modesti, Syed Ahmed, Ioannis Sfyrakis, Derek Enodolomwanyi
View a PDF of the paper titled Evaluating Large Language Models for Symbolic Security Protocol Analysis, by Paolo Modesti and 3 other authors
View PDF
HTML (experimental)
Abstract:Security protocols 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. Each provider uses a single model in both modes, switching reasoning on and off, so both contrasts isolate reasoning itself. Chat models achieve 72.7% recall at 27.3% precision for GPT and 69.3% recall at 27.2% precision for DeepSeek. Reasoning models reverse 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 lifts precision from 27.3% to 64.8% for GPT and from 27.2% to 44.4% for DeepSeek on the consolidated verdict. The goal set is imbalanced, with 89 vulnerable goals against 299 secure ones; a trivial always-secure predictor scores 77.1% accuracy, which only GPT reasoning exceeds. 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 reasoning, 74.0% for DeepSeek reasoning, 70.1% for GPT chat, and 61.6% for DeepSeek chat. Self-reported confidence is uniformly high yet shows no meaningful correlation with correctness. All results rest on a single zero-shot prompt and two model providers, which limits generalisability. On this benchmark, LLMs do not match formal verification, but may serve, at best, as pre-screening filters.
Comments:
Subjects:
Cryptography and Security (cs.CR); Artificial Intelligence (cs.AI)
ACM classes:
D.2.4
Cite as:
arXiv:2607.20712 [cs.CR]
(or
arXiv:2607.20712v2 [cs.CR] for this version)
https://doi.org/10.48550/arXiv.2607.20712
Focus to learn more
arXiv-issued DOI via DataCite
Journal reference:
Electronics 2026, 15, 4141
Related DOI:
https://doi.org/10.3390/electronics15184141
Focus to learn more
DOI(s) linking to related resources
Submission history
From: Paolo Modesti [view email]
[v1]
Wed, 22 Jul 2026 20:29:59 UTC (82 KB)
[v2]
Thu, 17 Sep 2026 17:11:00 UTC (90 KB)
Full-text links:
Access Paper:
View a PDF of the paper titled Evaluating Large Language Models for Symbolic Security Protocol Analysis, by Paolo Modesti and 3 other authors
View PDF
HTML (experimental)
TeX Source
view license
Ancillary-file links:
Ancillary files (details):
calibration_pooled_chat.csv
calibration_pooled_deepseek.csv
calibration_pooled_gpt.csv
Current browse context:
cs.CR
new
|
recent
| 2026-07
Change to browse by:
cs
cs.AI
References & Citations
NASA ADS
Google Scholar
Semantic Scholar
export BibTeX citation
Loading...
BibTeX formatted citation
×
loading...
Data provided by:
Bookmark
Bibliographic Tools
Bibliographic and Citation Tools
Bibliographic Explorer Toggle
Bibliographic Explorer (What is the Explorer?)
Connected Papers Toggle
Connected Papers (What is Connected Papers?)
Litmaps Toggle
Litmaps (What is Litmaps?)
scite.ai Toggle
scite Smart Citations (What are Smart Citations?)
Code, Data, Media
Code, Data and Media Associated with this Article
alphaXiv Toggle
alphaXiv (What is alphaXiv?)
Links to Code Toggle
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub Toggle
DagsHub (What is DagsHub?)
GotitPub Toggle
Gotit.pub (What is GotitPub?)
Huggingface Toggle
Hugging Face (What is Huggingface?)
ScienceCast Toggle
ScienceCast (What is ScienceCast?)
Demos
Demos
Replicate Toggle
Replicate (What is Replicate?)
Spaces Toggle
Hugging Face Spaces (What is Spaces?)
Spaces Toggle
TXYZ.AI (What is TXYZ.AI?)
Related Papers
Recommenders and Search Tools
Link to Influence Flower
Influence Flower (What are Influence Flowers?)
Core recommender toggle
CORE Recommender (What is CORE?)
Author
Venue
Institution
Topic
About arXivLabs
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Which authors of this paper are endorsers? |
Disable MathJax (What is MathJax?)