Uppsala University
Department of Information Technology

### Technical Report 2003-063

# 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.