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

TL;DR

DeepSec advances the automated verification of cryptographic protocols by providing new theoretical complexity results, a decision procedure for key equivalences, and an efficient implementation that broadens practical analysis capabilities.

Contribution

It introduces a decision procedure for trace equivalence and labelled bisimilarity for protocols with certain cryptographic primitives, along with an efficient tool implementation.

Findings

New complexity results for static, trace, and bisimilarity

Decidable equivalences for a wide range of cryptographic primitives

DeepSec outperforms existing tools in efficiency and scope

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.