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