CryptoVerif: Automatic game sequences in the computational model
================================================================

CryptoVerif automates game-hopping proofs in the computational model, producing concrete security bounds for protocols. It has been applied to TLS 1.3, Signal and WireGuard and is the computational counterpart to ProVerif.

Maintainer: Bruno Blanchet, Inria (Prosecco)
Website: https://bblanche.gitlabpages.inria.fr/CryptoVerif/
Category: Proof systems and computational proofs
Targets: Protocols: TLS 1.3, Signal, WireGuard, Key exchange, Authenticated encryption compositions
Approach: Automatic and guided sequences of games with concrete security bounds
Access: Open source
Status: Active, mature
Strengths: Automation reduces proof effort. | Concrete bounds, not just yes/no. | Long record on major protocols.
Limits: Less flexible than EasyCrypt for novel primitives. | Modelling effort still significant. | Small user community.
Firms using it: none listed
Sources: https://bblanche.gitlabpages.inria.fr/CryptoVerif/

Source page: https://sorryfree.com/frameworks/cryptoverif/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13