Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson

TL;DR

CryptoVampire tackles automated verification for the Computationally Complete Symbolic Attacker ($\mathrm{CCSA}$) within the $BC$ Logic by encoding the BC framework into first-order logic ($FO$) and coupling it with saturation-based proving via the Vampire prover. It introduces the Evaluated Logic to bridge cryptographic semantics with classical $FO$, enabling sound automated proofs of trace properties for stateful, computationally grounded protocols and ensuring that FO proofs imply BC-security guarantees. The work delivers a practical automated verifier that handles subterm reasoning, offers preprocessing and native subterm techniques, and achieves competitive performance against CryptoVerif while enabling automation support for Squirrel proofs. These advances pave the way for scalable, fully automated cryptographic protocol verification with potential extensions to composition, post-quantum security, and relational indistinguishability proofs, significantly impacting protocol design and verification workflows.

Abstract

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.

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

TL;DR

CryptoVampire tackles automated verification for the Computationally Complete Symbolic Attacker () within the Logic by encoding the BC framework into first-order logic () and coupling it with saturation-based proving via the Vampire prover. It introduces the Evaluated Logic to bridge cryptographic semantics with classical , enabling sound automated proofs of trace properties for stateful, computationally grounded protocols and ensuring that FO proofs imply BC-security guarantees. The work delivers a practical automated verifier that handles subterm reasoning, offers preprocessing and native subterm techniques, and achieves competitive performance against CryptoVerif while enabling automation support for Squirrel proofs. These advances pave the way for scalable, fully automated cryptographic protocol verification with potential extensions to composition, post-quantum security, and relational indistinguishability proofs, significantly impacting protocol design and verification workflows.

Abstract

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.
Paper Structure (58 sections, 15 theorems, 75 equations, 13 figures)

This paper contains 58 sections, 15 theorems, 75 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Our contributions
  4. Overview
  5. First-Order Formalization of the Protocol
  6. Honest functions
  7. Honest randomness
  8. Cryptographic properties
  9. Protocol steps
  10. Protocol query
  11. Automated Verification of Protocol Queries
  12. Subterm reasoning
  13. Soundness challenges
  14. Further optimizations
  15. Preliminaries
  16. ...and 43 more sections

Key Result

Theorem 2

For all Squirrel protocol $\mathcal{P}_{\mathrm{sq}}$, we can find a CryptoVampire protocol $\mathcal{P}$, such that for all Squirrel trace $\mathbb{T}_{\mathrm{sq}}$ over $\mathcal{P}_{\mathrm{sq}}$, we can find a CryptoVampire trace over $\mathcal{P}$, such that for all computational models $\math where $\left[ \_ \right]^{\mathbb{T}_{\mathrm{sq}}}_{\mathrm{sq}}$ is the Squirrel unfolding from s

Figures (13)

  • Figure 1: Grammar of $\hbox{$\text{\mlogicname S}$} \xspace\mleft( \mathcal{N}\xspace, \mathcal{F}\xspace, \mathcal{I}\xspace, \mathcal{C}\xspace, \mathcal{S}\xspace \mright)$
  • Figure 2: The Evaluated Logic $\hbox{$\text{\mlogicname E}$} \xspace\mleft( \mathcal{N}\xspace, \mathcal{F}\xspace, \mathcal{I}\xspace, \mathcal{C}\xspace, \mathcal{S}\xspace \mright)$
  • Figure 3: Cryptographic Model
  • Figure 4: Axiomatization of the subterm relation
  • Figure 5: CryptoVampire experiments
  • ...and 8 more figures

Theorems & Definitions (61)

  • Example 2: Basic Hash
  • Example 3: Functions
  • Example 4: Nonces
  • Example 5: Cryptographic Properties
  • Example 6: Steps
  • Example 7: Mutual Execution
  • Example 8: Query
  • Example 9
  • Example 10: Preprocessing
  • Remark 2: Eliminating subterm reasoning
  • ...and 51 more