@inproceedings{ abadi97calculus,
  author =	 "Abadi, Mart{\'\i}n and Gordon,  Andrew D.",
  title =	 "A Calculus for Cryptographic Protocols: The Spi Calculus",
  booktitle =	 "Proc. 4th ACM Conference on Computer and Communications
                  Security (CCS)",
  pages =	 "36--47",
  year =	 "1997"
}

@Manual{Blanchet:ProVerif,
  title = 	 {Cryptographic Protocol Verifier User Manual},
  OPTkey = 	 {},
  author =	 {Blanchet, Bruno},
  organization = {Ecole Normale Sup{\'e}rieure and Max-Planck-Institut f{\"u}r Informatik},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  month =	 feb,
  year =	 {2004},
  note =	 {\url{http://www.di.ens.fr/~blanchet/}},
  OPTannote = 	 {}
}

@InProceedings{NNS:H1,
  author = 	 {Nielson, Flemming and Nielson, Hanne Riis and Seidl, Helmut},
  title = 	 {Normalizable {H}orn Clauses, Strongly Recognizable Relations and {S}pi},
  booktitle = 	 {9th Static Analysis Symposium (SAS)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2002},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Springer Verlag LNCS 2477},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{JGL:eva:sem,
  author =       "Goubault-Larrecq, Jean",
  title =        "Les syntaxes et la s{\'e}mantique du langage de
                 sp{\'e}cification {EVA}",
  year =         "2001",
  month =        nov,
  howpublished = "Rapport num{\'e}ro 3 du projet RNTL EVA",
  note =         "32 pages",
  lsv-category = "cont",
  wwwpublic =    "non pour les contrats",
}

@InCollection{Blanchet:prolog,
  author = 	 {Blanchet, Bruno},
  title = 	 {An Efficient Cryptographic Protocol Verifier Based on {P}rolog Rules},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop (CSFW-14)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {82--96},
  publisher =	 {IEEE Computer Society Press},
  year =	 {2001},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress =	 {Cape Breton, Nouvelle-{\'E}cosse, Canada},
  OPTedition = 	 {},
  OPTmonth =	 jun,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@article{JGL-ipl2005,
      author =    {Goubault{-}Larrecq, Jean},
      journal =    {Information Processing Letters},
      month =    aug,
      number =    {3},
      pages =    {401-408},
      publisher =    {Elsevier Science Publishers},
      title =    {Deciding {\(\mathcal{\MakeUppercase{H}}_1\)} by Resolution},
      url =    {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
      volume =    {95},
      year =    {2005}
}

@InProceedings{CS:MACE,
  author = 	 {Claessen, Koen and S{\"o}rensson, Niklas},
  title = 	 {New Techniques that Improve {MACE}-Style Finite Model Building.},
  crossref = "W4:2003",
  note =	 {\url{http://www.uni-koblenz.de/~peter/models03/final/soerensson/main.ps}},
  OPTannote = 	 {}
}

@InProceedings{Tammet:MACE,
  author = 	 {Tammet, Tanel},
  title = 	 {Finite model building: improvements and comparisons},
  crossref = "W4:2003",
  note =	 {\url{http://www.uni-koblenz.de/~peter/models03/final/tammet/tammet.ps}},
  OPTannote = 	 {}
}

@Proceedings{W4:2003,
  title = 	 {CADE-19 Workshop W4},
  year = 	 {2003},
  OPTkey =		 {W4},
  editor =	 {Baumgartner, Peter},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress =	 {Miami, FL, USA},
  OPTmonth =	 jul,
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {\url{http://www.uni-koblenz.de/~peter/models03/final/}},
  OPTannote = 	 {}
}

@InProceedings{JGL:JFLA04,
  author =       "Goubault-Larrecq, Jean",
  title =        "Une fois qu'on n'a pas trouv{\'e} de preuve, comment le
                 faire comprendre {\`a} un assistant de preuve~?",
  pages = "1--40",
  booktitle =    "Actes 15{\`e}mes journ{\'e}es francophones sur les langages
                 applicatifs (JFLA 2004), Sainte-Marie-de-R{\'e}, France,
                 Jan.\ 2004",
  year =         "2004",
  publisher =    "INRIA, collection didactique",
  lsv-category = "auti",
  URL =          "http://www.lsv.ens-cachan.fr/Publis/PAPERS/JGL-JFLA2004.ps",
  wwwpublic =    "public ccsb",
}