fbpx
Wikipedia

ProVerif

January 01, 1970

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.

ProVerif
Developer(s)Bruno Blanchet
Initial releaseJune 1, 2002 (2002-06-01)
Stable release
2.04 / December 1, 2021 (2021-12-01)[1]
Written inOCaml
Available inEnglish
LicenseMainly, GNU GPL; Windows binaries, BSD licenses
Websiteprosecco.gforge.inria.fr/personal/bblanche/proverif/

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 edit

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 edit

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 edit

  1. ^ New release: ProVerif 2.04 - Community - OCaml
  2. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ 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. ^ "Application Layer Transport Security | Documentation". Google Cloud.
  21. ^ 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. ^ 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.

External links edit

  • Official website

January 01, 1970
proverif, software, tool, automated, reasoning, about, security, properties, cryptographic, protocols, tool, been, developed, bruno, blanchet, others, developer, bruno, blanchetinitial, releasejune, 2002, 2002, stable, release2, december, 2021, 2021, written, . 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 ProVerifDeveloper s Bruno BlanchetInitial releaseJune 1 2002 2002 06 01 Stable release2 04 December 1 2021 2021 12 01 1 Written inOCamlAvailable inEnglishLicenseMainly GNU GPL Windows binaries BSD licensesWebsiteprosecco wbr gforge wbr inria wbr fr wbr personal wbr bblanche wbr proverif wbr Support is provided for cryptographic primitives including symmetric amp 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 Contents 1 Applicability of ProVerif 2 Alternatives 3 References 4 External linksApplicability of ProVerif editProVerif has been used in the following case studies which include the security analysis of actual network protocols Abadi amp Blanchet 2 used correspondence assertions to verify the certified email protocol 3 Abadi Blanchet amp 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 amp 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 amp Ryan 11 have evaluated authentication protocols found in the Trusted Platform Module TPM a widely deployed hardware chip and discovered vulnerabilities Delaune Kremer amp Ryan 12 13 and Backes Hritcu amp Maffei 14 formalise and analyse privacy properties for electronic voting using observational equivalence Delaune Ryan amp Smyth 15 and Backes Maffei amp Unruh 16 analyse the anonymity properties of the trusted computing scheme Direct Anonymous Attestation DAA using observational equivalence Kusters amp Truderung 17 18 examine protocols with Diffie Hellman exponentiation and XOR Smyth Ryan Kremer amp 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 editAlternative 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 edit New release ProVerif 2 04 Community OCaml 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 Abadi Martin 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 Abadi Martin Blanchet Bruno Fournet Cedric 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 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 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 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 Bhargavan Karthikeyan Fournet Cedric 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 Bhargavan Karthikeyan Fournet Cedric 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 Bhargavan Karthikeyan Fournet Cedric 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 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 Delaune Stephanie 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 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 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 Delaune Stephanie 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 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 Kusters 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 Kusters 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 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 Application Layer Transport Security Documentation Google Cloud 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 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 External links editOfficial website Retrieved from https en wikipedia org w index php title ProVerif amp oldid 1206933627, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.