CryptoVerif
From Wikipedia, the free encyclopedia
Page Module:Message box/ambox.css has no content.Page Template:Multiple issues/styles.css has no content.
This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages)
Page Module:Message box/ambox.css has no content.
|
Page Module:Infobox/styles.css has no content.
| CryptoVerif | |
|---|---|
| Initial release | Script error: No such module "Date time". |
| Written in | OCaml |
| Available in | English |
| License | Mainly the GNU GPL / Windows binary BSD licenses |
| Website | prosecco |
Script error: No such module "Check for conflicting parameters".
CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet.[1]
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
- ^ Page Module:Citation/CS1/styles.css has no content.Blanchet, Bruno (2008). "A Computationally Sound Mechanized Prover for Security Protocols". IEEE Transactions on Dependable and Secure Computing. 5 (4): 193–207. doi:10.1109/TDSC.2007.1005.
