CryptoVerif
CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet. 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

External links
 

Cryptographic software