BlanchetMOD11

Bruno Blanchet Back to publications

Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. In Olga Grumberg, Tobias Nipkow, and Javier Esparza, editors, Tools for Analysis and Verification of Software Safety and Security. IOS Press, 2012. Proceedings of the 2011 MOD summer school. To appear.

Get the paper

.pdf, 204 Kb

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.

Bibtex


@INCOLLECTION{BlanchetMOD11,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Mechanizing Game-Based Proofs of Security Protocols},
  BOOKTITLE = {Tools for Analysis and Verification of Software Safety and Security},
  OPTPAGES = {},
  PUBLISHER = {IOS Press},
  YEAR = {2012},
  EDITOR = {Olga Grumberg and Tobias Nipkow and Javier Esparza},
  OPTVOLUME = {},
  OPTNUMBER = {},
  OPTSERIES = {NATO Science for Peace and Security Series -- D: Information and Communication Security},
  OPTTYPE = {},
  OPTCHAPTER = {},
  OPTADDRESS = {},
  OPTEDITION = {},
  OPTMONTH = {},
  NOTE = {Proceedings of the 2011 MOD summer school. To appear}
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-ens.fr (remove trap-)