CryptoVerif
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.
It can prove
secrecy and correspondences properties. The latter include in particular authentication.It provides a mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular
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.
