CryptoVerif

CryptoVerif [1] is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet. Contrary to ProVerif by the same creator that uses a symbolic abstraction, it is sound in the computational model.

CryptoVerif
Developer(s)Bruno Blanchet
Initial release2005 (2005)
Stable release
1.21 / September 3, 2015 (2015-09-03)
Written inOCaml
Available inEnglish
LicenseMainly the GNU GPL / Windows binary BSD licenses
Websiteprosecco.gforge.inria.fr/personal/bblanche/cryptoverif/

It can prove secrecy and correspondences properties. The latter include in particular authentication.

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 can 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.

gollark: PotatOS's terms include the clause> This policy supersedes any applicable federal, national, state, and local laws, regulations and ordinances, international treaties, and legal agreements that would otherwise apply.so mine is.
gollark: It's not legally binding.
gollark: I can add that too? Neat.
gollark: The terms now say> By using potatOS, misusing potatOS, installing potatOS, reading code or documentation for potatOS, knowing about these terms, knowing anyone who is bound by these terms, reading these terms, or thinking of anything related to these terms, you agree to be bound by these terms.so that is not an excuse.
gollark: <@151391317740486657> Oh no. How terrible.

References
  1. Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.