A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols

TL;DR

This survey reviews symbolic methods for verifying equivalence-based security properties in cryptographic protocols, highlighting decidability results and existing tools for analyzing complex security notions like anonymity and privacy.

Contribution

It provides a comprehensive synthesis of decidability results and an overview of verification tools for equivalence-based security properties in cryptography.

Findings

Decidability results vary depending on protocol models and properties.

Several tools exist for verifying equivalence-based security properties.

Equivalence notions are crucial for analyzing privacy and anonymity.

Abstract

Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. A secure communication has a different meaning depending on the underlying application. It ranges from the confidentiality of a data to e.g. verifiability in electronic voting systems. Another example of a security notion is privacy. Formal symbolic models have proved their usefulness for analysing the security of protocols. Until quite recently, most results focused on trace properties like confidentiality or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, and privacy related properties. During the last decade, several results and verification tools have been developed to analyse equivalence-based security properties. We propose here a synthesis of decidability and undecidability results for equivalence-based security properties. Moreover, we give an overview of existing verification tools that may be used to verify equivalence-based security properties.