@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.}
}