@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@article{TCS2013-Vincent,
author = {Cheval, Vincent and Cortier, V{\'e}ronique and Delaune, St\'ephanie},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
title = {Deciding equivalence-based properties using constraint solving},
year = {2013},
doi = {10.1016/j.tcs.2013.04.016},
volume = {492},
OPTnumber = {},
pages = {1-39},
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
\emph{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: \emph{observational equivalence}, \emph{may-testing equivalence}, and \emph{trace equivalence}.
First, we study the
relationship between these three notions.
We show that for \emph{determinate} processes, observational equivalence actually
coincides with trace equivalence, a notion simpler to reason with.
We exhibit a large class of determinate processes, called \emph{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 \emph{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.
},
}