@InCollection{BlanchetMOD11,
  author = 	 {Bruno Blanchet},
  title = 	 {Mechanizing Game-Based Proofs of Security Protocols},
  booktitle = 	 {Software Safety and Security - Tools for Analysis and Verification},
  pages = 	 {1--25},
  publisher = {IOS Press},
  year = 	 2012,
  editor = 	 {Tobias Nipkow and Olga Grumberg and Benedikt Hauptmann},
  volume = 	 33,
  series = 	 {NATO Science for Peace and Security Series -- D: Information and Communication Security},
  month = 	 may,
  IBSN = {978-1-61499-027-7},
  note = 	 {Proceedings of the summer school MOD 2011},
  abstract = {After a short introduction to the field of security
                  protocol verification, we present the automatic
                  protocol verifier CryptoVerif. In contrast to most
                  previous protocol verifiers, CryptoVerif does not
                  rely on the Dolev-Yao model, but on the
                  computational model. It produces proofs presented as
                  sequences of games, like those manually done by
                  cryptographers; these games are formalized in a
                  probabilistic process calculus. CryptoVerif provides
                  a generic method for specifying security properties
                  of the cryptographic primitives. It can prove
                  secrecy and correspondence properties (including
                  authentication). It produces proofs valid for any
                  number of sessions, in the presence of an active
                  adversary. It also provides an explicit formula for
                  the probability of success of an attack against the
                  protocol, as a function of the probability of
                  breaking each primitive and of the number of
                  sessions.},
  x-audience = {international},
  x-language = {EN},
  url = {http://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetMOD11.pdf},
  PDF = {http://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetMOD11.pdf}
}