Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice

Vincent Cheval, Steve Kremer, Itsaka Rakotonirina

TL;DR

DeepSec provides a rigorous framework for deciding privacy-style security properties of cryptographic protocols under a bounded number of sessions. It combines a symbolic semantics, constraint-based unification, and a partition-tree data structure to obtain exact decision procedures for trace equivalence and related relations over a broad class of primitives modeled by destructor subterm-convergent rewrite systems. The authors establish tight complexity bounds, proving coNEXP-completeness for trace equivalence and labelled bisimilarity, and they implement these procedures in the DeepSec prover, achieving strong performance on a wide range of protocols versus existing tools. This work advances both theory and practice by delivering decidability and complexity results alongside scalable tools that can analyze real-world privacy properties like anonymity and unlinkability. The approach lays groundwork for extending to richer security properties and more general cryptographic theories, with practical implications for automated security verification.

Abstract

Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.

DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice

TL;DR

DeepSec provides a rigorous framework for deciding privacy-style security properties of cryptographic protocols under a bounded number of sessions. It combines a symbolic semantics, constraint-based unification, and a partition-tree data structure to obtain exact decision procedures for trace equivalence and related relations over a broad class of primitives modeled by destructor subterm-convergent rewrite systems. The authors establish tight complexity bounds, proving coNEXP-completeness for trace equivalence and labelled bisimilarity, and they implement these procedures in the DeepSec prover, achieving strong performance on a wide range of protocols versus existing tools. This work advances both theory and practice by delivering decidability and complexity results alongside scalable tools that can analyze real-world privacy properties like anonymity and unlinkability. The approach lays groundwork for extending to richer security properties and more general cryptographic theories, with practical implications for automated security verification.

Abstract

Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
Paper Structure (144 sections, 61 theorems, 142 equations, 13 figures, 2 tables, 1 algorithm)

This paper contains 144 sections, 61 theorems, 142 equations, 13 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Complexity
  3. Decision procedure
  4. Tool implementation
  5. Model
  6. Messages and cryptography
  7. Protocol messages
  8. Specifying cryptographic assumptions
  9. Protocols
  10. Processes
  11. Attacker's knowledge
  12. Operational semantics
  13. Security properties
  14. Against a passive attacker
  15. Against an active attacker
  16. ...and 129 more sections

Key Result

proposition 3.9

For all sets of second-order equations $\mathcal{E}$, the computation of $\mathit{mgu}(\mathcal{E})$ terminates. Besides we have that $\mathit{mgu}(\mathcal{E}) = \bot$iff there exist no unifiers of $\mathcal{E}$. When $\mathit{mgu}(\mathcal{E}) \neq \bot$, we have that:

Figures (13)

  • Figure 4: Semantics of the calculus
  • Figure 5: A symbolic semantics for the applied pi-calculus
  • Figure 6: Tree of all constraint systems reachable by executing $B$ symbolically
  • Figure 7: A simplified partition tree of $P$ and $Q$
  • Figure 8: Partition tree with the rewriting system extended with $\mathsf{test\_aenc}(\mathsf{aenc}(x,y,\mathsf{pk}(z))) \to \mathsf{ok}$
  • ...and 8 more figures

Theorems & Definitions (122)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • definition 2.4
  • definition 2.5: trace
  • Example 2.6
  • definition 2.7
  • Example 2.8
  • definition 2.9: Trace equivalence
  • definition 2.10: Simulation, (Bi)similarity
  • ...and 112 more