||This article is written like a personal reflection or opinion essay that states the Wikipedia editor's personal feelings about a topic, rather than the opinions of experts. (November 2011) (Learn how and when to remove this template message)|
|This article needs additional citations for verification. (November 2011) (Learn how and when to remove this template message)|
1.21 / September 3, 2015
|License||Mainly the GNU GPL / Windows binary BSD licenses|
CryptoVerif  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.
Supported cryptographic mechanisms
It provides a mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular
- symmetric encryption,
- message authentication codes,
- public-key encryption,
- hash functions.
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).
- Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.