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.