Surf Wiki
Save to docs
general/cryptographic-software

From Surf Wiki (app.surf) — the open knowledge base

ProVerif

Software for automated reasoning about cryptography

Software for automated reasoning about cryptography

FieldValue
nameProVerif
titleProVerif
logo
screenshot
developerBruno Blanchet
released
latest release version2.04
latest release date
latest preview date
programming languageOCaml
languageEnglish
licenseMainly, GNU GPL; Windows binaries, BSD licenses
website

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

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 used correspondence assertions to verify the certified email protocol.
  • Abadi, Blanchet & Fournet analyse the Just Fast Keying 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 studied the integrity of the Plutus file system on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
  • Bhargavan et al. use ProVerif to analyse cryptographic protocol implementations written in F#; in particular the Transport Layer Security (TLS) protocol has been studied in this manner.
  • Chen & Ryan have evaluated authentication protocols found in the Trusted Platform Module (TPM), a widely deployed hardware chip, and discovered vulnerabilities.
  • Delaune, Kremer & Ryan and Backes, Hritcu & Maffei formalise and analyse privacy properties for electronic voting using observational equivalence.
  • Delaune, Ryan & Smyth and Backes, Maffei & Unruh analyse the anonymity properties of the trusted computing scheme Direct Anonymous Attestation (DAA) using observational equivalence.
  • Kusters & Truderung examine protocols with Diffie-Hellman exponentiation and XOR.
  • Smyth, Ryan, Kremer & Kourjieh formalise and analyse verifiability properties for electronic voting using reachability.
  • Google verified its transport layer protocol ALTS.
  • Sardar et al. verified the remote attestation protocols in Intel SGX.

Further examples can be found online: https://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif-users.html.

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. The Tamarin Prover is a modern alternative to ProVerif, with excellent support for Diffie-Hellman equational reasoning, and verification of observational equivalence properties.

References

References

  1. [https://discuss.ocaml.org/t/new-release-proverif-2-04/8924 New release: ProVerif 2.04 - Community - OCaml]
  2. (2005). "Computer-assisted verification of a protocol for certified email". Science of Computer Programming.
  3. (2002). "Proceedings of the 11th international conference on World Wide Web". ACM.
  4. (July 2007). "Just Fast Keying in the Pi Calculus". ACM Transactions on Information and System Security.
  5. (May 2004). "Just Fast Keying: Key Agreement in a Hostile Interne". ACM Transactions on Information and System Security.
  6. (May 2008). "2008 IEEE Symposium on Security and Privacy (Sp 2008)".
  7. (2003). "Plutus: Scalable Secure File Sharing on Untrusted Storage". Proceedings of the 2nd USENIX Conference on File and Storage Technologies.
  8. (2006-09-08). "Web Services and Formal Methods". Springer, Berlin, Heidelberg.
  9. (2008). "Proceedings of the 2008 ACM symposium on Information, computer and communications security". ACM.
  10. (December 2008). "Verified Interoperable Implementations of Security Protocols". ACM Transactions on Programming Languages and Systems.
  11. (2009-11-05). "Formal Aspects in Security and Trust". Springer, Berlin, Heidelberg.
  12. (2009-01-01). "Verifying privacy-type properties of electronic voting protocols". Journal of Computer Security.
  13. (2005-04-04). "Programming Languages and Systems". Springer, Berlin, Heidelberg.
  14. (June 2008). "2008 21st IEEE Computer Security Foundations Symposium".
  15. (2008-06-18). "Trust Management II". Springer, Boston, MA.
  16. (May 2008). "2008 IEEE Symposium on Security and Privacy (Sp 2008)".
  17. (July 2009). "2009 22nd IEEE Computer Security Foundations Symposium".
  18. (2011-04-01). "Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach". Journal of Automated Reasoning.
  19. (2010-09-20). "Computer Security – ESORICS 2010". Springer, Berlin, Heidelberg.
  20. "Application Layer Transport Security {{!}} Documentation".
  21. (August 2020). "2020 23rd Euromicro Conference on Digital System Design (DSD)". IEEE.
  22. (2020). "Formal Methods and Software Engineering". Springer International Publishing.
Info: Wikipedia Source

This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page.

cryptographic-software free-software-programmed-in-ocaml automated-reasoning software-using-the-gnu-general-public-license software-using-the-bsd-license
Want to explore this topic further?

Ask Mako anything about ProVerif — get instant answers, deeper analysis, and related topics.

Research with Mako

Free with your Surf account

Content sourced from Wikipedia, available under CC BY-SA 4.0.

This content may have been generated or modified by AI. CloudSurf Software LLC is not responsible for the accuracy, completeness, or reliability of AI-generated content. Always verify important information from primary sources.

Report