@TechReport{ it:2003-063,
author = {Michael Baldamus and Joachim Parrow and Bj{\"o}rn Victor},
title = {Spi Calculus Translated to $\pi$-Calculus Preserving
May-Testing},
institution = {Department of Information Technology, Uppsala University},
department = {Division of Computer Systems},
year = {2003},
number = {2003-063},
month = dec,
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.}
}