Steve Kremer: Symbolic bisimulation for the applied pi calculus

Symbolic bisimulation for the applied pi calculus

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Symbolic bisimulation for the applied pi calculus. Journal of Computer Security, 18(2):317–377, IOS Press, March 2010.
doi:10.3233/JCS-2010-0363

Download

[PDF] [HTML]

Abstract

We propose a symbolic semantics for the finite applied pi calculus. The applied pi calculus is a variant of the pi calculus with extensions for modelling cryptographic protocols. By treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms. We define a symbolic labelled bisimulation relation, which is shown to be sound but not complete with respect to standard bisimulation. We explore the lack of completeness and demonstrate that the symbolic bisimulation relation is sufficient for many practical examples. This work is an important step towards automation of observational equivalence for the finite applied pi calculus, e.g. for verification of anonymity or strong secrecy properties.

BibTeX

@article{DKR-jcs09,
  abstract =      {We propose a symbolic semantics for the finite
                   applied pi~calculus. The~applied pi calculus is a
                   variant of the pi~calculus with extensions for
                   modelling cryptographic protocols. By~treating inputs
                   symbolically, our semantics avoids potentially
                   infinite branching of execution trees due to inputs
                   from the environment. Correctness is maintained by
                   associating with each process a set of constraints on
                   terms. We~define a symbolic labelled bisimulation
                   relation, which is shown to be sound but not complete
                   with respect to standard bisimulation. We explore the
                   lack of completeness and demonstrate that the
                   symbolic bisimulation relation is sufficient for many
                   practical examples. This~work is an important step
                   towards automation of observational equivalence for
                   the finite applied pi calculus, \textit{e.g.}~for
                   verification of anonymity or strong secrecy
                   properties.},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Ryan, Mark D.},
  DOI =           {10.3233/JCS-2010-0363},
  journal =       {Journal of Computer Security},
  month =         mar,
  number =        {2},
  pages =         {317-377},
  publisher =     {{IOS} Press},
  title =         {Symbolic bisimulation for the applied pi~calculus},
  volume =        {18},
  year =          {2010},
  nmonth =        {3},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs09.pdf},
}