CryptoVerif
Software tool for software verification
title: "CryptoVerif" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["cryptographic-software"] description: "Software tool for software verification" topic_path: "general/cryptographic-software" source: "https://en.wikipedia.org/wiki/CryptoVerif" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0
::summary Software tool for software verification ::
::data[format=table title="Infobox software"]
| Field | Value |
|---|---|
| name | CryptoVerif |
| title | CryptoVerif |
| logo | |
| screenshot | |
| released | |
| latest release version | 1.21 |
| latest release date | |
| latest preview date | |
| programming language | OCaml |
| language | English |
| license | Mainly the GNU GPL / Windows binary BSD licenses |
| website | |
| :: |
| name = CryptoVerif | title = CryptoVerif | logo = | screenshot = | caption = | collapsible = | author = | developer = | released = | discontinued = | latest release version = 1.21 | latest release date = | latest preview version = | latest preview date = | programming language = OCaml | operating system = | platform = | size = | language = English | status = | genre = | license = Mainly the GNU GPL / Windows binary BSD licenses | website =
CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet.
Supported cryptographic mechanisms
It provides a 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.
Concrete security
CryptoVerif claims to evaluate the probability of a successful attack against a protocol relative to the probability of breaking each cryptographic primitive, i.e. it can establish concrete security.
References
References
- Blanchet, Bruno. (2008). "A Computationally Sound Mechanized Prover for Security Protocols". IEEE Transactions on Dependable and Secure Computing.
::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::