Attacking Formal Methods for Real-World Security Protocols Analyzing Crypto Protocols: using Legacy Crypto from attacks to proofs [part I] Karthikeyan Bhargavan + many, many others. (INRIA, Microsoft Research, LORIA, IMDEA, Univ of Pennsylvania, Univ of Michigan, JHU) Internet protocols (TLS, SSH, IPsec) seemingly implement textbook cryptographic protocols … yet, not exactly the same protocols • Modeling gaps between paper proofs and real protocol • Implementation gaps between protocol and deployment These gaps lead to many attacks, new questions Example: HTTPS for Web Security Secure connection to bank’s website Nobody other than the bank can read what I type (confidentiality) xxxxxxx My secret login Information Nobody other than me can access my account page (authentication) Goal: Prevent unauthorized access to data even if an unknown attacker controls Secure Channel? the network and some other bank clients. compose a standard AKE with a standard AEAD 3 • 3Shake Insecure resumption [Apr’14] • POODLE SSLv3 MAC-Encode-Encrypt [Dec’14] • SMACK State machine attacks [Jan’15] • FREAK Export-grade 512-bit RSA [Mar’15] • LOGJAM Export-grade 512-bit DH [May’15] • SLOTH RSA-MD5 signatures [Jan’16] • DROWN SSLv2 RSA-PKCS#1v1.5 [Mar’16] • 3Shake Insecure resumption [Apr’14] • SMACK State machine attacks [Jan’15] High-profile attacks, with Logos! • FREAK Export-grade 512-bit RSA [Mar’15] What’s going on? • LOGJAM Export-grade 512-bit DH [May’15] How do we prevent this in the future? • SLOTH RSA-MD5 signatures [Jan’16] Part I: Attacks on Authenticated Key Exchange in TLS Part 2: Finding Protocol Flaws with Symbolic Analysis Part 3: Mechanizing Cryptographic Protocol Proofs Part 4: Towards High-Assurance Crypto Software Part I: Attacks on Authenticated Key Exchange in TLS • TLS 1.2. IETF RFC 5246. • Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice. ACM CCS 2015. • Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH. ISOC NDSS 2016. 2018? TLS1.3 OpenSSL, SecureTransport, NSS, SChannel, GnuTLS, JSSE, PolarSSL, … many bugs, attacks, patches every year mostly for simplified models of TLS Client Server