Skip to Main content Skip to Navigation
Book sections

Mechanizing Game-Based Proofs of Security Protocols

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.
Document type :
Book sections
Complete list of metadata

Cited literature [56 references]  Display  Hide  Download

https://hal.inria.fr/hal-00863389
Contributor : Ben Smyth <>
Submitted on : Wednesday, September 18, 2013 - 5:37:53 PM
Last modification on : Saturday, July 11, 2020 - 3:45:27 AM
Long-term archiving on: : Friday, December 20, 2013 - 3:03:46 PM

File

BlanchetMOD11.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00863389, version 1

Collections

Citation

Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. Tobias Nipkow and Olga Grumberg and Benedikt Hauptmann. Software Safety and Security - Tools for Analysis and Verification, 33, IOS Press, pp.1--25, 2012, NATO Science for Peace and Security Series ― D: Information and Communication Security. ⟨hal-00863389⟩

Share

Metrics

Record views

317

Files downloads

253