CryptoVerif

(... to be written)

Source

CryptoVerif's project page is [CryptoVerif]. A detailed explanation is in [B17]. Newer developments are described in slides [B17a]. A nice short practical introduction to CryptoVerif is [S10].

CryptoVerif has been used to verify various drafts of the upcoming TLS 1.3 standard in the Computational Model [BBK17, RefTLS].

Khartikeyan Bhargavan explained and live-demoed CryptoVerif in his talk "Mechanized Computational Protocol Proofs", starting at 21:53, at the 8th BIU Winter School on Cryptography, Secure Key Exchange, February 11-15 2018 (all videos). No slides found for this talk, but similar slides from Bruno Blanchet [B09, B11, B14, B17b] can be used.

The remainder of the CryptoVerif presentation and demo is in the first 21:00 minutes of the followup talk "Verified Cryptographic Libraries":

CryptoVerif is actively used in research, and is accessible enough even for a Master's Thesis[L18] student.

Literature

  • [CryptoVerif] CryptoVerif: Cryptographic Protocol Verifier in the Computational Model
  • [B07] Bruno Blanchet: A Computationally Sound Mechanized Prover for Security Protocols. May 25, 2007. In: IEEE Transactions on Dependable and Secure Computing, 5(4):193-207, October-December 2008. Special issue IEEE Symposium on Security and Privacy 2006. (ieee paywalled, full pdf)
  • [B09] Bruno Blanchet: CryptoVerif, A Computationally Sound Mechanized Prover for Cryptographic Protocols. September 2009. (slides pdf)
  • [B11] Bruno Blanchet: Mechanizing Game-Based Proofs of Security Protocols. August 2011. (paper pdf, slides pdf, slides pdf backup, slides pdf backup)
  • [B14] Bruno Blanchet: CryptoVerif. November 2014. (slides pdf)
  • [B15] Bruno Blanchet: The automatic protocol verifier CryptoVerif. Aprit 2015. (slides pdf)
  • [CB13] David Cadé, Bruno Blanchet: From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. In: Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), 4(1):4-31, March 2013. Special issue ARES'12. (full pdf, backup pdf)
  • [CB15] David Cadé, Bruno Blanchet: Proved Generation of Implementations from Computationally Secure Protocol Specifications. January 5, 2015. (full pdf)
  • [B17] Bruno Blanchet: CryptoVerif, A Computationally-Sound Security Protocol Verifier. November 20, 2017 (full pdf)
  • [B17a] Bruno Blanchet: CryptoVerif, state of the art, perspectives, and relations to other tools. April 2017 (slides pdf)
  • [B17b] Bruno Blanchet: Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. June 2017. (slides pdf, other source)
  • [BBK17] Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi: Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. (full pdf)
  • [L18] Benjamin Lipp: A Mechanized Computational Analysis of the WireGuard Virtual Private Network Protocol. Master's Thesis at KIT and INRIA. 2018. (full pdf)
  • [S10] Ivo Seeba: CryptoVerif, the tool of crypto analysis. (full pdf)
  • [BBK17] Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi: Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In: 2017 IEEE Symposium on Security and Privacy. (full pdf)
  • [RefTLS] Symbolic Verification with ProVerif. Project Website.