Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.35434

LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?

Tianjian Liu·Shicheng Feng·Jin'ao Shang·Xiaoting Lyu·Bin Wang·Zonghua Zhang·Lei Xue·Wei Wang
View original source ↗Read source document ↗Export metadata ↓

Abstract

Large language models (LLMs) have shown strong potential for assisting software and security analysis tasks, yet their effectiveness in cryptographic symbolic protocol verification remains insufficiently understood. In this paper, we conduct the first systematic evaluation of the capability of state-of-the-art LLMs in cryptographic symbolic protocol verification. To quantify this capability, we propose \textsc{CRoST} (Coverage Rate of Solve Tree), a proof-based metric derived from the verifier's proof skeleton that measures the similarity between generated lemmas and reference lemmas. We then establish the rationale of \textsc{CRoST} through both theoretical analysis and empirical validation. The evaluation results show that state-of-the-art models achieve 38.82\% coverage on average, with 14.4\% of generated lemmas exceeding 80\% coverage, indicating that LLMs can already generate useful lemmas to a certain extent. However, they still exhibit non-trivial failure modes on complex multi-phase protocols, show diminishing returns under naive scaling, and incur substantial verification overhead. These findings clarify the practical potential and limitations of LLMs for protocol verification and motivate future work on complex real-world protocols.

Explore related subjects

cs.CRcs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tianjian Liu, Shicheng Feng, Jin'ao Shang, Xiaoting Lyu, Bin Wang, Zonghua Zhang, Lei Xue, Wei Wang. 2026-09-28. LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?. https://arxiv.org/abs/2609.35434

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

SoK: Cryptocurrency Mixing and Anonymity - Architectures, Threat Models, Operational Aspects and Security

Public blockchains record transaction histories that enable address clustering, taint analysis, and cross-service attribution, thereby motivating the development of mixers and privacy layers. Our work presents a structured scoping review of 22 representative systems, defining a common unlinkability objective and five adversary archetypes. We evaluate these systems against a taxonomy of attack surfaces, including chain analysis, timing inference, custodial compromise, coordination abuse, network metadata, and trusted execution compromise. While nominal anonymity-set size and cryptographic strength characterize privacy in theory, effective anonymity in practice depends on transaction denominations, cover traffic, relayer behavior, and compliance-interface design. Distinguishing nominal from effective anonymity, we derive four core lessons: (1) Privacy is strongest when integrated into everyday transactions, since standalone mixing creates an easily profiled user subset; (2) Trust points, including operators, peer quorums, and hardware enclaves, must be explicit so users know who can break privacy; (3) Network metadata, including gas funding and timing, must be treated formally as protocol data in privacy evaluations; and (4) Compliance should use auditable cryptographic predicates for selective disclosure rather than broad operator discretion. Ultimately, our systematization clarifies the strengths, failures, and future requirements of blockchain privacy architectures.

cs.CR↗
arXiv2026

Decoding One Safety Trigger Token for Balancing Safety and Usability in Large Language Models

Large Language Models (LLMs) have been extensively used across diverse domains, including virtual assistants, automated code generation, and scientific research. However, they remain vulnerable to jailbreak attacks, which manipulate the models into generating harmful responses despite safety alignment. Recent studies have shown that current safety-aligned LLMs undergo shallow safety alignment. In this work, we conduct an in-depth investigation into the underlying mechanism of this phenomenon and reveal that it manifests through learned ''safety trigger tokens'' that activate the model's safety patterns when paired with the specific input. Through both analysis and empirical verification, we further demonstrate the high similarity of the safety trigger tokens across different harmful inputs. Accordingly, we propose D-STT, a simple yet effective defense algorithm that identifies and explicitly decodes safety trigger tokens of the given safety-aligned LLM to activate the model's learned safety patterns. In this process, the safety trigger is constrained to a single token, which effectively preserves model usability by introducing minimum intervention in the decoding process. Extensive experiments across diverse jailbreak attacks and benign prompts demonstrate that D-STT significantly reduces output harmfulness while preserving model usability and incurring negligible response time overhead, outperforming ten baseline methods.

cs.CR↗
arXiv2026

A traffic analysis attack against Introduction Protocol and Onion Services

Tor onion services rely on long-lived introduction circuits to support anonymous rendezvous between clients and services. Although Tor incorporates defenses against traffic analysis, the introduction protocol retains deterministic routing structure that can be exploited by an adversary. We present a practical intersection attack against Tor introduction circuits that over repeated interactions can identify each hop from the introduction point toward the onion service while requiring observation at only one relay per stage. The attack repeatedly probes the target service and intersects sets of destination IP addresses observed within narrowly bounded INTRODUCE1-RENDEZVOUS2 intervals, without assuming global visibility or access to packet payloads. Our traffic-analysis technique identifies with certainty the next relay in the path to target at each stage, thereby revealing a gap in Tor's privacy model, which is intended to resist traffic-analysis attacks in which an adversary uses traffic patterns to determine which points in the network to observe or attack. We evaluate the attack's feasibility through live-network experiments using a self-operated onion service and relays. To support data minimization, we implement a Tor-compatible plugin that computes intersections online over pseudonymized data retained only in volatile memory. Our experiments show reliable convergence in practice, with convergence rate influenced by relay consensus weight and time-varying background traffic. We further assess practicality under a partial-global adversary model and discuss the implications of geographic concentration in Tor relay selection weight across cooperating jurisdictions.

cs.CR↗