CryptoVerif

CryptoVerif est un outil logiciel de raisonnement automatique sur les protocoles de sécurité écrit par Bruno Blanchet.

Il fournit un mécanisme permettant de spécifier les hypothèses de sécurité sur les primitives cryptographiques , qui peuvent gérer en particulier

• cryptage symétrique ,
• codes d'authentification des messages ,
• cryptage à clé publique ,
• signatures ,
• fonctions de hachage .

CryptoVerif prétend évaluer la probabilité d'une attaque réussie contre un protocole par rapport à la probabilité de casser chaque primitive cryptographique, c'est-à-dire qu'il peut établir une sécurité concrète .