Spi Calculus Translated to pi-Calculus Preserving May-Testing

Michael Baldamus, Joachim Parrow, and Björn Victor

December 2003

Abstract:

We present a concise and natural encoding of the spi-calculus into the more basic pi-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 pi. The translation also entails a more detailed operational 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.

Available as PDF (424 kB), compressed Postscript (339 kB), and Postscript (951 kB)

Download BibTeX entry.