Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Trace Equivalence Decision: Negative Tests and Non-determinism. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11), pp. 321–330, ACM Press, Chicago, Illinois, USA, October 2011.
We consider security properties of cryptographic protocols that can be modeled using the notion of trace equivalence. The notion of equivalence is crucial when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability.
In this paper, we give a calculus that is close to the applied pi calculus and that allows one to capture most existing protocols that rely on classical cryptographic primitives. First, we propose a symbolic semantics for our calculus relying on constraint systems to represent infinite sets of possible traces, and we reduce the decidability of trace equivalence to deciding a notion of symbolic equivalence between sets of constraint systems. Second, we develop an algorithm allowing us to decide whether two sets of constraint systems are in symbolic equivalence or not. Altogether, this yields the first decidability result of trace equivalence for a general class of processes that may involve else branches and\slash or private channels (for a bounded number of sessions).
@inproceedings{CCD-ccs11,
abstract = {We consider security properties of cryptographic
protocols that can be modeled using the notion of
trace equivalence. The notion of equivalence is
crucial when specifying privacy-type properties, like
anonymity, vote-privacy, and unlinkability.\par In
this paper, we give a calculus that is close to the
applied pi calculus and that allows one to capture
most existing protocols that rely on classical
cryptographic primitives. First, we propose a
symbolic semantics for our calculus relying on
constraint systems to represent infinite sets of
possible traces, and we reduce the decidability of
trace equivalence to deciding a notion of symbolic
equivalence between sets of constraint systems.
Second, we develop an algorithm allowing us to decide
whether two sets of constraint systems are in
symbolic equivalence or not. Altogether, this yields
the first decidability result of trace equivalence
for a general class of processes that may involve
else branches and\slash or private channels (for a
bounded number of sessions).},
address = {Chicago, Illinois, USA},
author = {Cheval, Vincent and Comon{-}Lundh, Hubert and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 18th {ACM} {C}onference on
{C}omputer and {C}ommunications {S}ecurity
({CCS}'11)},
OPTDOI = {10.1145/2046707.2046744},
editor = {Chen, Yan and Danezis, George and Shmatikov, Vitaly},
month = oct,
pages = {321-330},
publisher = {ACM Press},
title = {Trace Equivalence Decision: Negative Tests and
Non-determinism},
year = {2011},
acronym = {{CCS}'11},
nmonth = {10},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}