Logic in Computer Science, Symposium on (2004)

Turku, Finland

July 13, 2004 to July 17, 2004

ISSN: 1043-6871

ISBN: 0-7695-2192-4

pp: 22-31

Michael Baldamus , Uppsala University, Sweden

Joachim Parrow , Uppsala University, Sweden

Bj? Victor , Uppsala University, Sweden

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.

INDEX TERMS

null

CITATION

Michael Baldamus,
Joachim Parrow,
Bj? Victor,
"Spi Calculus Translated to π--Calculus Preserving May-Tests",

*Logic in Computer Science, Symposium on*, vol. 00, no. , pp. 22-31, 2004, doi:10.1109/LICS.2004.1319597CITATIONS