Evaluating Large Language Models for Symbolic Security Protocol Analysis

• URL: http://arxiv.org/abs/2607.20712v1
• Date: Wed, 22 Jul 2026 20:29:59 GMT
• Title: Evaluating Large Language Models for Symbolic Security Protocol Analysis
• Abstract summary: This study evaluates whether Large Language Models (LLMs) can perform comparable analysis.<n>We test GPT and DeepSeek in chat and reasoning modes over three runs on 130 obfuscated AnB/AnBx protocols.
• Score: 1.0499611180329804
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: 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.

Related papers

• State of Thought Enables Endogenous Reasoning [48.902117018115256]
  Test-time reasoning has emerged as a major approach to improving the capabilities of Large Language Models (LLMs)<n>We propose State of Thought, a new reasoning paradigm that enables endogenous reasoning in LLMs.<n>We show that SoT consistently improves mean-baseline accuracy while reducing generated tokens by 62.6% and end-to-end latency by 44.6%.
  arXiv  Detail & Related papers  (2026-09-13T05:55:03Z)
• Adversarial Robustness of Phishing Email Detection: A Comparative Study of TF-IDF + Logistic Regression and Fine-Tuned DistilBERT [0.0]
  This paper reports a comparison of two phishing-detection approaches a TF-IDF + Logistic Regression baseline and a fine-tuned DistilBERT transformer trained on a unified corpus of 82,255 emails.<n>Both models exceeded 98% accuracy on clean data yet degraded sharply under adversarial testing.<n>The results show that clean-data accuracy does not predict adversarial robustness, and adversarial testing should be a standard part of phishing-detection evaluation.
  arXiv  Detail & Related papers  (2026-07-20T18:28:07Z)
• Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
  We describe our PointArena 2026 solution, which achieves 77.2% overall accuracy and ranks second on the benchmark.<n>The ap proach targets three failure modes. First, agent-driven syn thesis builds large semantic and anchor-relative candidate pools.<n>Second, a determinis tic steerable-data pipeline creates a verified 10,000-sample main set, plus reserve samples, using masks, templates, and path verification.
  arXiv  Detail & Related papers  (2026-06-29T06:39:03Z)
• Understanding and Mitigating Premature Confidence for Better LLM Reasoning [76.16007941549857]
  Long chains of thought (CoT) from current language models frequently contain logical gaps and unjustified leaps.<n>We find such a signal in how the model's confidence evolves during reasoning.<n>We exploit this in progressive confidence shaping, a reinforcement learning objective that trains models to update their confidence as they reason rather than commit early.
  arXiv  Detail & Related papers  (2026-05-23T04:42:45Z)
• Do Language Models Know When They'll Refuse? Probing Introspective Awareness of Safety Boundaries [0.0]
  Large language models are trained to refuse harmful requests, but can they accurately predict when they will refuse before responding?<n>We investigate this question through a systematic study where models first predict their refusal behavior, then respond in a fresh context.<n>Using signal detection theory (SDT), we find that all models exhibit high introspective sensitivity (d' = 2.4-3.5), but sensitivity drops substantially at safety boundaries.
  arXiv  Detail & Related papers  (2026-03-31T20:49:34Z)
• Lie to Me: How Faithful Is Chain-of-Thought Reasoning in Reasoning Models? [0.0]
  Chain-of-thought (CoT) reasoning has been proposed as a transparency mechanism for large language models in safety-critical deployments.<n>This study tests 12 open-weight reasoning models spanning 9 architectural families on 498 multiple-choice questions.<n>Across 41,832 inference runs, overall faithfulness rates range from 39.7% (Seed-1.6-Flash) to 89.9% (DeepSeek-V3.2-Speciale) across model families.
  arXiv  Detail & Related papers  (2026-03-23T21:21:37Z)
• Powerful Training-Free Membership Inference Against Autoregressive Language Models [3.9380576851378657]
  We present EZ-MIA, a membership inference attack that exploits a key observation: memorization manifests most strongly at error positions.<n>We introduce the Error Zone (EZ) score, which measures the directional imbalance of probability shifts at error positions.<n>Results establish that privacy risks of fine-tuned language models are substantially greater than previously understood.
  arXiv  Detail & Related papers  (2026-01-17T16:59:41Z)
• Does Inference Scaling Improve Reasoning Faithfulness? A Multi-Model Analysis of Self-Consistency Tradeoffs [0.0]
  Self-consistency has emerged as a popular technique for improving large language model accuracy on reasoning tasks.<n>We investigate a fundamental question that has not been studied before: does inference scaling improve reasoning faithfulness?<n>We conduct a comprehensive empirical study across four frontier models (GPT-5.2, Claude Opus 4.5, Gemini-3-flash-preview, and DeepSeek-v3.2) on 100 GSM8K mathematical reasoning problems.
  arXiv  Detail & Related papers  (2026-01-10T04:20:00Z)
• CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
  We show that correctness of a solution is encoded as a geometrically separable signature within the trajectory of hidden activations.<n>ClUE consistently outperforms LLM-as-a-judge baselines and matches or exceeds modern confidence-based methods in reranking candidates.
  arXiv  Detail & Related papers  (2025-10-02T02:14:33Z)
• MedOmni-45°: A Safety-Performance Benchmark for Reasoning-Oriented LLMs in Medicine [69.08855631283829]
  We introduce Med Omni-45 Degrees, a benchmark designed to quantify safety-performance trade-offs under manipulative hint conditions.<n>It contains 1,804 reasoning-focused medical questions across six specialties and three task types, including 500 from MedMCQA.<n>Results show a consistent safety-performance trade-off, with no model surpassing the diagonal.
  arXiv  Detail & Related papers  (2025-08-22T08:38:16Z)
• Benchmarking Reasoning Robustness in Large Language Models [76.79744000300363]
  We find significant performance degradation on novel or incomplete data.<n>These findings highlight the reliance on recall over rigorous logical inference.<n>This paper introduces a novel benchmark, termed as Math-RoB, that exploits hallucinations triggered by missing information to expose reasoning gaps.
  arXiv  Detail & Related papers  (2025-03-06T15:36:06Z)
• How Easy is It to Fool Your Multimodal LLMs? An Empirical Analysis on Deceptive Prompts [54.07541591018305]
  We present MAD-Bench, a benchmark that contains 1000 test samples divided into 5 categories, such as non-existent objects, count of objects, and spatial relationship. We provide a comprehensive analysis of popular MLLMs, ranging from GPT-4v, Reka, Gemini-Pro, to open-sourced models, such as LLaVA-NeXT and MiniCPM-Llama3. While GPT-4o achieves 82.82% accuracy on MAD-Bench, the accuracy of any other model in our experiments ranges from 9% to 50%.
  arXiv  Detail & Related papers  (2024-02-20T18:31:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.