@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@article{CCD-tcs13,
abstract = {Formal methods have proved their usefulness for
analyzing the security of protocols. Most existing
results focus on trace properties like secrecy 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, privacy related properties or
statements closer to security properties used in
cryptography.\par In this paper, we consider three
notions of equivalence defined in the applied pi
calculus: observational equivalence, may-testing
equivalence, and trace equivalence. First, we study
the relationship between these three notions. We show
that for determinate processes, observational
equivalence actually coincides with trace
equivalence, a notion simpler to reason with. We
exhibit a large class of determinate processes,
called simple processes, that capture most existing
protocols and cryptographic primitives. While trace
equivalence and may-testing equivalence seem very
similar, we show that may-testing equivalence is
actually strictly stronger than trace equivalence. We
prove that the two notions coincide for image-finite
processes, such as processes without replication.\par
Second, we reduce the decidability of trace
equivalence (for finite processes) to deciding
symbolic equivalence between sets of constraint
systems. For simple processes without replication and
with trivial else branches, it turns out that it is
actually sufficient to decide symbolic equivalence
between pairs of positive constraint systems. Thanks
to this reduction and relying on a result first
proved by M. Baudet, this yields the first
decidability result of observational equivalence for
a general class of equational theories (for processes
without else branch nor replication). Moreover, based
on another decidability result for deciding
equivalence between sets of constraint systems, we
get decidability of trace equivalence for processes
with else branch for standard primitives.},
author = {Cheval, Vincent and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
OPTDOI = {10.1016/j.tcs.2013.04.016},
journal = {Theoretical Computer Science},
month = jun,
pages = {1-39},
publisher = {Elsevier Science Publishers},
title = {Deciding equivalence-based properties using
constraint solving},
volume = {492},
year = {2013},
nmonth = {6},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}