Developer(s) Bruno Blanchet | Initial release 2005 (2005) Available in English | |
Stable release 1.21 / September 3, 2015 (2015-09-03) 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.
Contents
It can prove secrecy and correspondences properties. The latter include in particular authentication.
Supported cryptographic mechanisms
It provides a mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular
Concrete Security
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
CryptoVerif Wikipedia(Text) CC BY-SA