ProVerif

ProVerif

Developer(s)	Bruno Blanchet
Initial release	June 1, 2002
Stable release	1.90 / May 7, 2015
Written in	OCaml
Available in	English
License	Mainly the GNU GPL / Windows binary BSD licenses
Website	prosecco.gforge.inria.fr/personal/bblanche/proverif/

ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet.

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:

• Abadi & Blanchet^[1] used correspondence assertions to verify the certified email protocol.^[2]
• Abadi, Blanchet & Fournet ^[3] analyse the Just Fast Keying ^[4] protocol, which was one of the candidates to replace Internet Key Exchange (IKE) as the key exchange protocol in IPsec, by combining manual proofs with ProVerif proofs of correspondence and equivalence.
• Blanchet & Chaudhuri ^[5] studied the integrity of the Plutus file system ^[6] on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
• Bhargavan et al. ^[7][8][9] use ProVerif to analyse cryptographic protocol implementations written in the F Sharp (programming language); in particular the Transport Layer Security (TLS) protocol has been studied in this manner.
• Chen & Ryan ^[10] have evaluated authentication protocols found in the Trusted Platform Module (TPM), a widely deployed hardware chip, and discovered vulnerabilities.
• Delaune, Kremer & Ryan ^[11][12] and Backes, Hritcu & Maffei ^[13] formalise and analyse privacy properties for electronic voting using observational equivalence.
• Delaune, Ryan & Smyth^[14] and Backes, Maffei & Unruh^[15] analyse the anonymity properties of the trusted computing scheme Direct Anonymous Attestation (DAA) using observational equivalence.
• Kusters & Truderung^[16][17] examine protocols with Diffie-Hellman exponentiation and XOR.
• Smyth, Ryan, Kremer & Kourjieh ^[18] formalise and analyse verifiability properties for electronic voting using reachability.

Further examples can be found online: .

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.

References

1. Abadi, Martin; Blanchet, Bruno (2005), "Computer-assisted verification of a protocol for certified email", Science of Computer Programming, 58 (1-2): 3–27, doi:10.1016/j.scico.2005.02.002
2. Abadi, Martin; Neal Glew; Bill Horne; Benny Pinkas (2002). "Certified email with a light on-line trusted third party: Design and implementation". 11th International World Wide Web Conference. pp. 387–395.
3. Abadi, Martin; Bruno Blanchet, and Cedric Fournet (2007), "Just Fast Keying in the pi calculus", ACM Transactions on Information and System Security, 10 (3): 1–59 Cite uses deprecated parameter |coauthors= (help)
4. Aiello, William; Steven M. Bellovin, Matt Blaze, Ran Canetti, John Ioannidis, Angelos Keromytis, and Omer Reingold (2004), "Just Fast Keying: Key agreement in a hostile Internet", ACM Transactions on Information and System Security, 7 (2): 242–273, doi:10.1145/996943.996946 Cite uses deprecated parameter |coauthors= (help)
5. Bruno Blanchet and Avik Chaudhuri. Automated formal analysis of a protocol for secure file sharing on untrusted storage. In IEEE Symposium on Security and Privacy, pages 417–431, Oakland, CA, May 2008. IEEE.
6. Mahesh Kallahalla, Erik Riedel, Ram Swaminathan, Qian Wang, and Kvin Fu. Plutus: Scalable secure file sharing on untrusted storage. In 2nd Conference on File and Storage Technologies (FAST’03), pages 29–42, San Francisco, CA, April 2003. Usenix.
7. Karthikeyan Bhargavan, C´edric Fournet, and Andrew Gordon. Verified reference implementations of WS-Security protocols. In Mario Bravetti, Manuel Nunez, and Gianluigi Zavattaro, editors, 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006), volume 4184 of Lecture Notes on Computer Science, pages 88–106, Vienna, Austria, September 2006. Springer.
8. Karthikeyan Bhargavan, Cedric Fournet, Andrew Gordon, and Nikhil Swamy. Verified implementations of the information card federated identity-management protocol. In ACM Symposium on Information, Computer and Communications Security (ASIACCS’08), pages 123–135, Tokyo, Japan, March 2008. ACM.
9. Karthikeyan Bhargavan, Cedric Fournet, Andrew Gordon, and Stephen Tse. Verified interoperable implementations of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW’06), pages 139–152, Venice, Italy, July 2006. IEEE Computer Society.
10. Liqun Chen and Mark Ryan. Attack, solution and verification for shared authorisation data in TCG TPM. In Proc. Sixth Formal Aspects in Security and Trust (FAST’09), Lecture Notes on Computer Science. Springer, 2009.
11. Delaune, Stephanie; Steve Kremer, and Mark D. Ryan (2009), "Verifying privacy-type properties of electronic voting protocols", Journal of Computer Security Cite uses deprecated parameter |coauthors= (help)
12. Steve Kremer and Mark D. Ryan. Analysis of an electronic voting protocol in the applied pi calculus. In Mooly Sagiv, editor, Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, volume 3444 of Lecture Notes on Computer Science, pages 186–200, Edinbourgh, UK, April 2005. Springer.
13. Michael Backes, Catalin Hritcu, and Matteo Maffei. Automated verification of electronic voting protocols in the applied pi-calculus. In 21st IEEE Computer Security Foundations Symposium (CSF’08), pages 195–209, Pittsburgh, PA, June 2008. IEEE Computer Society.
14. Stephanie Delaune, Mark D. Ryan, and Ben Smyth. Automatic verification of privacy properties in the applied pi-calculus. In Yuecel Karabulut, John Mitchell, Peter Herrmann, and Christian Damsgaard Jensen, editors, Proceedings of the 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM’08), volume 263 of IFIP Conference Proceedings, pages 263–278. Springer, June 2008.
15. Michael Backes, Matteo Maffei, and Dominique Unruh. Zero-knowledge in the applied picalculus and automated verification of the direct anonymous attestation protocol. In 29th IEEE Symposium on Security and Privacy, pages 202–215, Oakland, CA, May 2008. IEEE.
16. Ralf Kusters and Tomasz Truderung. Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In 22nd IEEE Computer Security Foundations Symposium, pages 157–171, Port Jefferson, New York, USA, July 2009. IEEE.
17. Ralf Kusters and Tomasz Truderung. Reducing protocol analysis with XOR to the XORfree case in the Horn theory based approach. In Proceedings of the 15th ACM conference on Computer and communications security (CCS’08), pages 129–138, Alexandria, Virginia, USA, October 2008. ACM.
18. Ben Smyth, Mark Ryan, Steve Kremer, and Mounira Kourjieh. Election verifiability in electronic voting protocols. In ARSPA-WITS’10: Proceedings of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, 2010.

External links

• Official website