CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet. Contrary to ProVerif

ProVerif

ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet....

 by the same creator that uses a symbolic abstraction, it is sound in the computational model.

It can prove
secrecy

Secrecy

Secrecy is the practice of hiding information from certain individuals or groups, perhaps while sharing it with other individuals...

 and correspondences properties. The latter include in particular authentication

Authentication

Authentication is the act of confirming the truth of an attribute of a datum or entity...

.

Supported cryptographic mechanisms

It provides a mechanism for specifying the security assumptions on cryptographic primitive

Cryptographic primitive

Cryptographic primitives are well-established, low-level cryptographic algorithms that are frequently used to build computer security systems. These routines include, but are not limited to, one-way hash functions and encryption functions.- Rationale :...

s, which can handle in particular

• symmetric encryption,
• message authentication codes,
• public-key encryption,
• signatures,
• hash functions.

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

Concrete security

In cryptography, concrete security or exact security is a practice-oriented approach that aims to give more precise estimates of the computational complexities of adversarial tasks than polynomial equivalence would allow....

).