CryptoVerif

From Wikipedia, the free encyclopedia
Jump to: navigation, search
CryptoVerif
Developer(s) Bruno Blanchet
Initial release 2005 (2005)
Stable release 1.12
Written in OCaml
Available in English
License Mainly the GNU GPL / Windows binary BSD licenses
Website www.cryptoverif.ens.fr/

CryptoVerif[1] is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet. Contrary to ProVerif by the same creator that uses a symbolic abstraction, it is sound in the computational model.

It can prove secrecy and correspondences properties. The latter include in particular authentication.

Supported cryptographic mechanisms[edit]

It provides a mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular

Concrete Security[edit]

CryptoVerif can evaluate the probability of a successful attack against a protocol relative to the probability of breaking each cryptographic primitive, i.e. it can establish concrete security).

References[edit]

  1. ^ Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.