Simon Jeanteur | Searcharxiv

arXiv2026

LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean

Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-dependent behavior, inductively defined data structures, unbounded executions, and conditional secrecy requires a level of expressiveness that is difficult to reconcile with effective automation. As a result, protocol verification has largely followed two disjoint paths: fully automated methods with limited expressiveness, or interactive proofs in general-purpose theorem provers that offer flexibility but only limited, non-specialized automation. We present an orthogonal approach that bridges this gap by combining compositional type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols. Guided by the language-and-automation co-design (LAC) principle, our approach delivers protocol-specific automation while retaining high expressiveness. We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*, and combining protocol-specific automation with interactive proofs. Our framework supports, in a unified setting, a broad class of functional and security requirements, including secrecy and authentication for stateful protocols, as well as recursive conditional secrecy for protocols using XOR. We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.

cs.CR↗

arXiv2024

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel.

cs.CR↗