Mechanizing Game-Based Proofs of Security Protocols

Bruno Blanchet 1
1 CASCADE - Construction and Analysis of Systems for Confidentiality and Authenticity of Data and Entities
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
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.
Type de document :
Chapitre d'ouvrage
Tobias Nipkow; Orna Grumberg; Benedikt Hauptmann. Software Safety and Security, 33, IOS Press, pp.1-25, 2012, NATO Science for Peace and Security Series - D: Information and Communication Security, 978-1-61499-027-7. 〈10.3233/978-1-61499-028-4-1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01110430
Contributeur : Brigitte Briot <>
Soumis le : mercredi 28 janvier 2015 - 10:51:12
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Identifiants

Collections

Citation

Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. Tobias Nipkow; Orna Grumberg; Benedikt Hauptmann. Software Safety and Security, 33, IOS Press, pp.1-25, 2012, NATO Science for Peace and Security Series - D: Information and Communication Security, 978-1-61499-027-7. 〈10.3233/978-1-61499-028-4-1〉. 〈hal-01110430〉

Partager

Métriques

Consultations de la notice

101