  This document presents the security protocol verifier CryptoVerif.CryptoVerif
does not rely on the symbolic, Dolev-Yao model, but on the computational model.
It can verify secrecy, correspondence (which include authentication), and
indistinguishability properties. It produces proofs presented as sequences of
games, like those manually written by cryptographers; these games are
formalized in aprobabilistic process calculus. CryptoVerif provides a generic
method for specifying security properties of the cryptographic primitives.It
produces proofs valid for any number of sessions of the protocol, and provides
an upper bound on the probability of success of an attack against the protocol
as a function of the probability of breaking each primitive and of the number
of sessions. It can work automatically, or the user can guide it with manual
proof indications.
