A method for proving observational equivalence

A method for proving observational equivalence. Véronique Cortier and Stéphanie Delaune. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09), pp. 266–276, IEEE Computer Society Press, Port Jefferson, NY, USA, July 2009.

Download

[PDF] [HTML]

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 observational equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.
In this paper, we consider the applied pi calculus and 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. 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.

BibTeX

@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},
}