Why Verified Crypto?

(... to be written)

Sources

The real-world attacks presented here (Alert, 3SHAKE, VHC, SMACK, Logjam, SLOTH, SKIP, FREAK...) are listed and explained in [SMACK]. This site links to the original papers and slides[B15] etc. Highly recommended.

The main inspiration for this crypto bite is Karthikeyan Bhargavan's talk "Man-in-the-Middle Attacks on Authenticated Key Exchange" (slides) at the 8th BIU Winter School on Cryptography, Secure Key Exchange, February 11-15 2018 (all videos):

and Karthik's follow-up session "Downgrade Attacks on Agile Real-World Protocols" (same slides starting at page 50):

Karthik also gave an invited talk Protecting TLS from legacy crypto at EUROCRYPT 2016 (slides):

Another interesting presentation is Nadia Henninger's talk "How Diffie-Hellman Fails in Practice" (slides), at Simons Institute's workshop The Mathematics of Modern Cryptography, July 6-10, 2015. (all talks). This is covered in [WeakDH].

Literature

  • [WeakDH] David Adrian, Karthikeyan Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella-Béguelin, and Paul Zimmermann: Imperfect Forward Secrecy, How Diffie-Hellman Fails in Practice. In: 22nd ACM Conference on Computer and Communications Security (CCS ’15), Denver, CO, October 2015. (full pdf, slides pdf)
  • [GIJABS12] Martin Georgiev, Subodh Iyengar, Suman Jana, Rishita Anubhai, Dan Boneh, Vitaly Shmatikov: The Most Dangerous Code in the World, Validating SSL Certificates in Non-Browser Software. In: CCS'12 Proceedings of the 2012 ACM conference on Computer and communications security, pages 38-49. (acm.org paywalled, full pdf)
  • [SMACK] State Machine AttaCKs. (formerly smacktls.com)
  • [B15] Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cedric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue: A Messy State of the Union, Taming the Composite State Machines of TLS. In: 2015 IEEE Symposium on Security and Privacy. (full pdf, slides pdf)

(... to be extended)