@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@inproceedings{CD-csf09,
  address =       {Port Jefferson, NY, USA},
  author =        {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 22nd {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'09)},
  month =         jul,
  pages =         {266-276},
  publisher =     {{IEEE} Computer Society Press},
  title =         {A~method for proving observational equivalence},
  year =          {2009},
  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
                   the notion of \emph{observational equivalence}.
                   Typical examples are anonymity, privacy related
                   properties or statements closer to security
                   properties used in cryptography.\par In this paper,
                   we consider the applied pi calculus and 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.
                   Then, for simple processes without replication,
                   we~reduce the decidability of trace equivalence to
                   deciding an equivalence relation introduced by
                   M.~Baudet. Altogether, this yields the first
                   decidability result of observational equivalence for
                   a general class of equational theories.},
  doi =           {10.1109/CSF.2009.9},
}