Symbolic Bisimulation for the Applied Pi-Calculus

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Symbolic Bisimulation for the Applied Pi-Calculus. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp. 133–145, Lecture Notes in Computer Science 4855, Springer, New Delhi, India, December 2007.

Download

[PDF] 

Abstract

We propose a symbolic semantics for the finite applied pi calculus, which is a variant of the pi calculus with extensions for modelling cryptgraphic 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 symbolic terms. Based on the semantics, we define a sound symbolic labelled bisimulation relation. This 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 of protocols with a bounded number of sessions.

BibTeX

@inproceedings{DKR-fsttcs07,
  abstract =      {We propose a symbolic semantics for the finite
                   applied pi calculus, which is a variant of the pi
                   calculus with extensions for modelling cryptgraphic
                   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 symbolic terms. Based
                   on the semantics, we~define a sound symbolic labelled
                   bisimulation relation. This~is an important step
                   towards automation of observational equivalence for
                   the finite applied pi calculus, \emph{e.g.}, for
                   verification of anonymity or strong secrecy
                   properties of protocols with a bounded number of
                   sessions.},
  address =       {New~Delhi, India},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and
                   Ryan, Mark D.},
  booktitle =     {{P}roceedings of the 27th {C}onference on
                   {F}oundations of {S}oftware {T}echnology and
                   {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
  OPTDOI =           {10.1007/978-3-540-77050-3_11},
  editor =        {Arvind, V. and Prasad, Sanjiva},
  month =         dec,
  pages =         {133-145},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Symbolic Bisimulation for the Applied Pi-Calculus},
  volume =        {4855},
  year =          {2007},
  acceptrate =    {40/135},
  acronym =       {{FSTTCS}'07},
  nmonth =        {12},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}