CryptoVerif
{{Short description|Software tool for software verification}}
{{Multiple issues|
{{essay-like|date=November 2011}}
{{more citations needed|date=November 2011}}
{{Notability|Product|date=December 2021}}
}}
{{Infobox software
| name = CryptoVerif
| title = CryptoVerif
| logo =
| screenshot =
| caption =
| collapsible =
| author =
| developer =
| released = {{Start date|2005}}
| discontinued =
| latest release version = 1.21
| latest release date = {{start date|2015|9|3}}
| 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 = {{URL|prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/}}
}}
CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet.{{cite journal |first=Bruno |last=Blanchet |title=A Computationally Sound Mechanized Prover for Security Protocols |journal=IEEE Transactions on Dependable and Secure Computing |volume=5 |issue=4 |year=2008 |pages=193–207 |doi=10.1109/TDSC.2007.1005 }}
Supported cryptographic mechanisms
It provides a mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular
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
External links
- {{Official website|http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/}}