From Seo Wiki - Search Engine Optimization and Programming Languages
|This article is an orphan, as few or no other articles link to it. Please introduce links to this page from related articles; suggestions are available. (January 2010)|
|This article may not meet the general notability guideline. Please help to establish notability by adding reliable, secondary sources about the topic. If notability cannot be established, the article is likely to be merged, redirected, or deleted. (November 2009)|
ProVerif is the leading software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet and is based upon over a decade of theoretical research.
Support is provided for, but not limited to, 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 particular useful to the computer security domain since they permit the analysis of secrecy and authentication properties. Moreover, 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. Moreover, the tool is capable of attack reconstruction: when a property cannot be proved, an execution trace which falsifies the desired property is constructed.