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.
| Developer(s) | Bruno Blanchet |
|---|---|
| Initial release | 2005 |
| Stable release | 1.21
/ September 3, 2015 |
| Written in | OCaml |
| Available in | English |
| License | Mainly the GNU GPL / Windows binary BSD licenses |
| Website | prosecco |
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: I mean, except that we would have no way to defeat the aliens who were somehow *only* vulnerable to JavaScript code, in 2047.
gollark: If I were to retroactively make Brendon Eich embed Scheme instead we would all be better off.
gollark: That layout was/is perfect and without flaw APART FROM where it does that æ.
gollark: FLEXBOOOOOOOOOOX WHYYYY
gollark: CSS is so mildly irritating because there's basically always a way to do what I want which makes it all work really well, but it's impossible to work out what that way is.
References
- Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.
External links
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.