CryptoVerif

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==