Paper: Spi Calculus Translated to π--Calculus Preserving May-Tests (at LICS 2004)

Authors: Michael Baldamus Joachim Parrow Björn Victor

Abstract

We present a concise and natural encoding of the spi-calculus into the more basic π-calculus and establish its correctness with respect to a formal notion of testing. This is particularly relevant for security protocols modelled in spi since the tests can be viewed as adversaries. The translation has been implemented in a prototype tool. As a consequence, protocols can be described in the spi calculus and analysed with the emerging flora of tools already available for π. The translation also entails a more detailed ooperational understanding of spi since high level constructs like encryption are encoded in a well known lower level. The formal correctness proof is nontrivial and interesting in its own; so called context bisimulations and new techniques for compositionality make the proof simpler and more concise.

BibTeX

  @InProceedings{BaldamusParrowVicto-SpiCalculusTranslat,
    author = 	 {Michael Baldamus and Joachim Parrow and Björn Victor},
    title = 	 {Spi Calculus Translated to π--Calculus Preserving May-Tests},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004)},
    year =	 {2004},
    month =	 {July}, 
    pages =      {22--31},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }