package cryptoverif
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=55f6f52976b57ad779a736a6b617da03
sha512=f05b70ff9ab72daf6d58fd598b89fcbf8415cf1adfd0c93be8f98c18364d7da1c968be0a42cba7e0b17081f0bf73dd0b1c291ebc6df4306e93008a4a57e5ac61
Description
CryptoVerif is an automatic protocol prover sound in the computational model. It can prove
- secrecy;
- correspondences, which include in particular authentication;
- indistinguishability between two games.
It provides a generic 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.
The generated proofs are proofs by sequences of games, as used by cryptographers. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. CryptoVerif can also evaluate the probability of success of an attack against the protocol as a function of the probability of breaking each cryptographic primitive and of the number of sessions (exact security).
This software is under development; please use it at your own risk. Comments and bug reports welcome.