Stéphanie Delaune and Lucca Hirschi. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. Journal of Logical and Algebraic Methods in Programming, 87:127–144, 2017.
Cryptographic protocols aim at securing communications over insecurenetworks such as the Internet, where dishonest users may listen tocommunications and interfere with them. A secure communication has adifferent meaning depending on the underlying application. It rangesfrom the confidentiality of a data to e.g. verifiability in electronic voting systems. Another example ofa security notion is privacy.Formal symbolic models have proved their usefulness for analysing the securityof protocols. Until quite recently, most results focused on trace properties like confidentiality orauthentication. There are however several security properties, whichcannot be defined (or cannot be naturally defined) as trace propertiesand require a notion of behavioural equivalence. Typical examples are anonymity, and privacy related properties. Duringthe last decade, several results and verification tools have beendeveloped to analyse equivalence-based security properties.We propose here a synthesis of decidability and undecidability resultsfor equivalence-based security properties.Moreover, we give an overview of existing verification tools that maybe used to verify equivalence-based security properties.
@article{DH-survey16,
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.},
author = {Delaune, St{\'e}phanie and Hirschi, Lucca},
title = {A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {87},
pages = {127--144},
year = {2017},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}