\begin{thebibliography}{10}

\bibitem{abadi99ic}
Martin Abadi and Andrew~D. Gordon.
\newblock A calculus for cryptographic protocols: {The} spi calculus.
\newblock {\em Information and Computation}, 148(1):1--70, 99.

\bibitem{boreale}
Michele Boreale.
\newblock Symbolic trace analysis of cryptographic protocols.
\newblock In {\em Proceedings of ICALP 2001}, volume 2076 of {\em LNCS}, pages
  667 -- 681. Springer-Verlag, 2001.

\bibitem{boreale-siam}
Michele Boreale, Rocco~De Nicola, and Rosario Pugliese.
\newblock Proof techniques for cryptographic processes.
\newblock {\em SIAM J. Comput.}, 31(3):947--986, 2001.

\bibitem{borgstrom04concur}
Johannes Borgstr{\"o}m, S{\'e}bastien Briais, and Uwe Nestmann.
\newblock Symbolic bisimulation in the spi calculus.
\newblock In Philippa Gardner and Nobuko Yoshida, editors, {\em CONCUR}, volume
  3170 of {\em LNCS}, pages 161--176. Springer, 2004.

\bibitem{borgstrom05}
Johannes Borgstr{\"o}m and Uwe Nestmann.
\newblock On bisimulations for the spi calculus.
\newblock {\em Mathematical Structures in Computer Science}, 15(3):487--552,
  2005.

\bibitem{dawson-gore-gls-ca}
J.~E. Dawson and R.~Gor{\'e}.
\newblock Formalising cut-admissibility for provability logic.
\newblock Submitted, 2009.

\bibitem{dolevyao}
D.~Dolev and A.~Yao.
\newblock On the security of public-key protocols.
\newblock {\em IEEE Transactions on Information Theory}, 2(29), 1983.

\bibitem{kahsai08}
Temesghen Kahsai and Marino Miculan.
\newblock Implementing spi calculus using nominal techniques.
\newblock In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt L{\"o}we,
  editors, {\em CiE}, volume 5028 of {\em LNCS}, pages 294--305. Springer,
  2008.

\bibitem{milner92icII}
Robin Milner, Joachim Parrow, and David Walker.
\newblock A calculus of mobile processes, {Part II}.
\newblock {\em Information and Computation}, pages 41--77, 1992.

\bibitem{sangiorgi96acta}
Davide Sangiorgi.
\newblock A theory of bisimulation for the pi-calculus.
\newblock {\em Acta Inf.}, 33(1):69--97, 1996.

\bibitem{tiu-trace-based-bisim-abs}
Alwen Tiu.
\newblock A trace based bisimulation for the spi calculus: An extended
  abstract.
\newblock In Zhong Shao, editor, {\em APLAS}, volume 4807 of {\em LNCS}, pages
  367--382. Springer, 2007.

\bibitem{tiu-trace-based-bisim-full}
Alwen Tiu.
\newblock A trace based bisimulation for the spi calculus.
\newblock Preprint, available from \url{http://arxiv.org/pdf/0901.2166v1},
  2009.

\bibitem{ucb-mech-LF}
Christian Urban, James Cheney, and Stefan Berghofer.
\newblock Mechanizing the metatheory of lf.
\newblock In {\em LICS}, pages 45--56. IEEE Computer Society, 2008.

\end{thebibliography}
