Developer(s) Bruno Blanchet Available in English | ||
Initial release June 1, 2002 (2002-06-01) Stable release 1.90 / May 7, 2015 (2015-05-07) License Mainly the GNU GPL / Windows binary BSD licenses |
ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet.
Contents
Support is provided for cryptographic primitives including: symmetric & asymmetric cryptography; digital signatures; hash functions; bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and observational equivalence. These reasoning capabilities are particularly useful to the computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an unbounded message space. The tool is capable of attack reconstruction: when a property cannot be proved, an execution trace which falsifies the desired property is constructed.
Applicability of ProVerif
ProVerif has been used in the following case studies, which include the security analysis of actual network protocols:
Further examples can be found online: [1].
Alternatives
Alternative analysis tools include: AVISPA (for reachability and correspondence assertions), KISS (for static equivalence), YAPA (for static equivalence). CryptoVerif for verification of security against polynomial time adversaries in the computational model.