Software:CryptoVerif

From HandWiki
CryptoVerif
Initial releaseScript error: No such module "Date time".
Stable release
1.21 / Script error: No such module "Date time".
Written inOCaml
Available inEnglish
LicenseMainly the GNU GPL / Windows binary BSD licenses
Websiteprosecco.gforge.inria.fr/personal/bblanche/cryptoverif/

CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet.[1]

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,
  • signatures,
  • hash functions.

Concrete security

CryptoVerif claims to 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

  1. Blanchet, Bruno (2008). "A Computationally Sound Mechanized Prover for Security Protocols". IEEE Transactions on Dependable and Secure Computing 5 (4): 193–207. doi:10.1109/TDSC.2007.1005.