ProVerif

From Wikipedia, the free encyclopedia

Template:Short description

Page Module:Infobox/styles.css has no content.

ProVerif
[[Programmer|DeveloperTemplate:Pluralize from text]]Bruno Blanchet
Initial releaseScript error: No such module "Date time".
Template:Infobox software/simple
Written inOCaml
Available inEnglish
LicenseMainly, GNU GPL; Windows binaries, BSD licenses
Websiteprosecco.gforge.inria.fr/personal/bblanche/proverif/

Script error: No such module "Check for conflicting parameters".

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[2] used correspondence assertions to verify the certified email protocol.[3]
  • Abadi, Blanchet & Fournet[4] analyse the Just Fast Keying[5] 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[6] studied the integrity of the Plutus file system[7] on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
  • Bhargavan et al.[8][9][10] 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[11] have evaluated authentication protocols found in the Trusted Platform Module (TPM), a widely deployed hardware chip, and discovered vulnerabilities.
  • Delaune, Kremer & Ryan[12][13] and Backes, Hritcu & Maffei[14] formalise and analyse privacy properties for electronic voting using observational equivalence.
  • Delaune, Ryan & Smyth[15] and Backes, Maffei & Unruh[16] analyse the anonymity properties of the trusted computing scheme Direct Anonymous Attestation (DAA) using observational equivalence.
  • Kusters & Truderung[17][18] examine protocols with Diffie-Hellman exponentiation and XOR.
  • Smyth, Ryan, Kremer & Kourjieh[19] formalise and analyse verifiability properties for electronic voting using reachability.
  • Google[20] verified its transport layer protocol ALTS.
  • Sardar et al.[21][22] verified the remote attestation protocols in Intel SGX.

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

References

Page Template:Reflist/styles.css has no content.

  1. ^ New release: ProVerif 2.04 - Community - OCaml
  2. ^ Page Module:Citation/CS1/styles.css has no content.Abadi, Martín; 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.
  3. ^ Page Module:Citation/CS1/styles.css has no content.Abadi, Martín; Glew, Neal (2002). "Certified email with a light on-line trusted third party". Proceedings of the 11th international conference on World Wide Web. WWW '02. New York, NY, USA: ACM. pp. 387–395. doi:10.1145/511446.511497. ISBN 978-1581134490. S2CID 9035150.
  4. ^ Page Module:Citation/CS1/styles.css has no content.Abadi, Martín; Blanchet, Bruno; Fournet, Cédric (July 2007). "Just Fast Keying in the Pi Calculus". ACM Transactions on Information and System Security. 10 (3): 9–es. CiteSeerX 10.1.1.3.3762. doi:10.1145/1266977.1266978. ISSN 1094-9224. S2CID 2371806.
  5. ^ Page Module:Citation/CS1/styles.css has no content.Aiello, William; Bellovin, Steven M.; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D.; Reingold, Omer (May 2004). "Just Fast Keying: Key Agreement in a Hostile Interne". ACM Transactions on Information and System Security. 7 (2): 242–273. doi:10.1145/996943.996946. ISSN 1094-9224. S2CID 14442788.
  6. ^ Page Module:Citation/CS1/styles.css has no content.Blanchet, B.; Chaudhuri, A. (May 2008). "Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage". 2008 IEEE Symposium on Security and Privacy (Sp 2008). pp. 417–431. CiteSeerX 10.1.1.362.4343. doi:10.1109/SP.2008.12. ISBN 978-0-7695-3168-7. S2CID 6736116.
  7. ^ Page Module:Citation/CS1/styles.css has no content.Kallahalla, Mahesh; Riedel, Erik; Swaminathan, Ram; Wang, Qian; Fu, Kevin (2003). "Plutus: Scalable Secure File Sharing on Untrusted Storage". Proceedings of the 2nd USENIX Conference on File and Storage Technologies. FAST '03: 29–42.
  8. ^ Page Module:Citation/CS1/styles.css has no content.Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (2006-09-08). "Verified Reference Implementations of WS-Security Protocols". Web Services and Formal Methods. Lecture Notes in Computer Science. Vol. 4184. Springer, Berlin, Heidelberg. pp. 88–106. CiteSeerX 10.1.1.61.3389. doi:10.1007/11841197_6. ISBN 9783540388623.
  9. ^ Page Module:Citation/CS1/styles.css has no content.Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). "Verified implementations of the information card federated identity-management protocol". Proceedings of the 2008 ACM symposium on Information, computer and communications security. ASIACCS '08. New York, NY, USA: ACM. pp. 123–135. doi:10.1145/1368310.1368330. ISBN 9781595939791. S2CID 6821014.
  10. ^ Page Module:Citation/CS1/styles.css has no content.Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen (December 2008). "Verified Interoperable Implementations of Security Protocols". ACM Transactions on Programming Languages and Systems. 31 (1): 5:1–5:61. CiteSeerX 10.1.1.187.9727. doi:10.1145/1452044.1452049. ISSN 0164-0925. S2CID 14018835.
  11. ^ Page Module:Citation/CS1/styles.css has no content.Chen, Liqun; Ryan, Mark (2009-11-05). "Attack, Solution and Verification for Shared Authorisation Data in TCG TPM". Formal Aspects in Security and Trust. Lecture Notes in Computer Science. Vol. 5983. Springer, Berlin, Heidelberg. pp. 201–216. CiteSeerX 10.1.1.158.2073. doi:10.1007/978-3-642-12459-4_15. ISBN 9783642124587.
  12. ^ Page Module:Citation/CS1/styles.css has no content.Delaune, Stéphanie; Kremer, Steve; Ryan, Mark (2009-01-01). "Verifying privacy-type properties of electronic voting protocols". Journal of Computer Security. 17 (4): 435–487. CiteSeerX 10.1.1.142.1731. doi:10.3233/jcs-2009-0340. ISSN 0926-227X.
  13. ^ Page Module:Citation/CS1/styles.css has no content.Kremer, Steve; Ryan, Mark (2005-04-04). "Analysis of an Electronic Voting Protocol in the Applied Pi Calculus". Programming Languages and Systems. Lecture Notes in Computer Science. Vol. 3444. Springer, Berlin, Heidelberg. pp. 186–200. doi:10.1007/978-3-540-31987-0_14. ISBN 9783540254355.
  14. ^ Page Module:Citation/CS1/styles.css has no content.Backes, M.; Hritcu, C.; Maffei, M. (June 2008). "Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus". 2008 21st IEEE Computer Security Foundations Symposium. pp. 195–209. CiteSeerX 10.1.1.612.2408. doi:10.1109/CSF.2008.26. ISBN 978-0-7695-3182-3. S2CID 15189878.
  15. ^ Page Module:Citation/CS1/styles.css has no content.Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (2008-06-18). "Automatic Verification of Privacy Properties in the Applied pi Calculus". Trust Management II. IFIP – The International Federation for Information Processing. Vol. 263. Springer, Boston, MA. pp. 263–278. doi:10.1007/978-0-387-09428-1_17. ISBN 9780387094274.
  16. ^ Page Module:Citation/CS1/styles.css has no content.Backes, M.; Maffei, M.; Unruh, D. (May 2008). "Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol". 2008 IEEE Symposium on Security and Privacy (Sp 2008). pp. 202–215. CiteSeerX 10.1.1.463.489. doi:10.1109/SP.2008.23. ISBN 978-0-7695-3168-7. S2CID 651680.
  17. ^ Page Module:Citation/CS1/styles.css has no content.Küsters, R.; Truderung, T. (July 2009). "Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation". 2009 22nd IEEE Computer Security Foundations Symposium. pp. 157–171. CiteSeerX 10.1.1.667.7130. doi:10.1109/CSF.2009.17. ISBN 978-0-7695-3712-2. S2CID 14185888.
  18. ^ Page Module:Citation/CS1/styles.css has no content.Küsters, Ralf; Truderung, Tomasz (2011-04-01). "Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach". Journal of Automated Reasoning. 46 (3–4): 325–352. arXiv:0808.0634. doi:10.1007/s10817-010-9188-8. ISSN 0168-7433. S2CID 7597742.
  19. ^ Page Module:Citation/CS1/styles.css has no content.Kremer, Steve; Ryan, Mark; Smyth, Ben (2010-09-20). "Election Verifiability in Electronic Voting Protocols". Computer Security – ESORICS 2010. Lecture Notes in Computer Science. Vol. 6345. Springer, Berlin, Heidelberg. pp. 389–404. CiteSeerX 10.1.1.388.2984. doi:10.1007/978-3-642-15497-3_24. ISBN 9783642154966.
  20. ^ Page Module:Citation/CS1/styles.css has no content."Application Layer Transport Security | Documentation". Google Cloud.
  21. ^ Page Module:Citation/CS1/styles.css has no content.Sardar, Muhammad Usama; Quoc, Do Le; Fetzer, Christof (August 2020). "Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX". 2020 23rd Euromicro Conference on Digital System Design (DSD). Kranj, Slovenia: IEEE. pp. 604–607. doi:10.1109/DSD51259.2020.00099. ISBN 978-1-7281-9535-3. S2CID 222297511.
  22. ^ Page Module:Citation/CS1/styles.css has no content.Sardar, Muhammad Usama; Faqeh, Rasha; Fetzer, Christof (2020). "Formal Foundations for Intel SGX Data Center Attestation Primitives". In Lin, Shang-Wei; Hou, Zhe; Mahony, Brendan (eds.). Formal Methods and Software Engineering. Lecture Notes in Computer Science. Vol. 12531. Cham: Springer International Publishing. pp. 268–283. doi:10.1007/978-3-030-63406-3_16. ISBN 978-3-030-63406-3. S2CID 229344923.
Retrieved from "https://cosmopedia.co/index.php?title=ProVerif&oldid=7920510"