\begin{thebibliography}{}

\bibitem[Abadi and Gordon, 1997]{abadi97calculus}
Abadi, M. and Gordon, A.~D. (1997).
\newblock A calculus for cryptographic protocols: The spi calculus.
\newblock In {\em Proc. 4th ACM Conference on Computer and Communications
  Security (CCS)}, pages 36--47.

\bibitem[Blanchet, 2001]{Blanchet:prolog}
Blanchet, B. (2001).
\newblock An efficient cryptographic protocol verifier based on {P}rolog rules.
\newblock In {\em 14th IEEE Computer Security Foundations Workshop (CSFW-14)},
  pages 82--96. IEEE Computer Society Press.

\bibitem[Blanchet, 2004]{Blanchet:ProVerif}
Blanchet, B. (2004).
\newblock {\em Cryptographic Protocol Verifier User Manual}.
\newblock Ecole Normale Sup{\'e}rieure and Max-Planck-Institut f{\"u}r
  Informatik.
\newblock \url{http://www.di.ens.fr/~blanchet/}.

\bibitem[Claessen and S{\"o}rensson, 2003]{CS:MACE}
Claessen, K. and S{\"o}rensson, N. (2003).
\newblock New techniques that improve {MACE}-style finite model building.
\newblock
  \url{http://www.uni-koblenz.de/~peter/models03/final/soerensson/main.ps}.

\bibitem[Goubault-Larrecq, 2001]{JGL:eva:sem}
Goubault-Larrecq, J. (2001).
\newblock Les syntaxes et la s{\'e}mantique du langage de sp{\'e}cification
  {EVA}.
\newblock Rapport num{\'e}ro 3 du projet RNTL EVA.
\newblock 32 pages.

\bibitem[Goubault-Larrecq, 2004]{JGL:JFLA04}
Goubault-Larrecq, J. (2004).
\newblock Une fois qu'on n'a pas trouv{\'e} de preuve, comment le faire
  comprendre {\`a} un assistant de preuve~?
\newblock In {\em Actes 15{\`e}mes journ{\'e}es francophones sur les langages
  applicatifs (JFLA 2004), Sainte-Marie-de-R{\'e}, France, Jan.\ 2004}, pages
  1--40. INRIA, collection didactique.

\bibitem[Goubault{-}Larrecq, 2005]{JGL-ipl2005}
Goubault{-}Larrecq, J. (2005).
\newblock Deciding {\(\mathcal{\MakeUppercase{h}}_1\)} by resolution.
\newblock {\em Information Processing Letters}, 95(3):401--408.

\bibitem[Nielson et~al., 2002]{NNS:H1}
Nielson, F., Nielson, H.~R., and Seidl, H. (2002).
\newblock Normalizable {H}orn clauses, strongly recognizable relations and
  {S}pi.
\newblock In {\em 9th Static Analysis Symposium (SAS)}. Springer Verlag LNCS
  2477.

\end{thebibliography}