package cryptoverif

All checked builds pass
  1. Overview
  2. Docs
CryptoVerif: Cryptographic protocol verifier in the computational model

Install 

dune-project
 Dependency

cryptoverif.inria.fr Edit opam file Versions (13)

Authors

  1. B
    Bruno Blanchet <Bruno.Blanchet@inria.fr>, Pierre Boutry <boutry.pierre@gmail.com>, David Cadé <David.Cade@normalesup.org>, Christian Doczkal <christian.doczkal@mpi-sp.org>, Aymeric Fromherz <Aymeric.Fromherz@inria.fr>, Charlie Jacomme <Charlie.Jacomme@inria.fr>, Benjamin Lipp <Benjamin.Lipp@mpi-sp.org>, and Pierre-Yves Strub <pierre-yves@strub.nu>

Maintainers

  1. B
    Bruno Blanchet <Bruno.Blanchet@inria.fr>

Sources

cryptoverif2.13.tar.gz
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.

Added to opam-repository:

Dependencies (4)

  1. conf-m4 post
  2. cryptokit >= "1.21" & post
  3. ocamlfind post
  4. ocaml >= "4.08"

Dev Dependencies

None

Optional Dependencies

None

Used by

None

Conflicts

None

Build status

Results of building cryptoverif with each compiler on check.ci.ocaml.org, run of against opam-repository 7cdc698. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
2.13 (this version) n/a good good good good
2.12 good good good good good
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure