A Messy State of the Union - Taming the Composite State Machines of TLS

Explore a comprehensive analysis of the Transport Layer Security (TLS) protocol's composite state machines in this IEEE conference talk. Delve into the challenges of designing robust state machines that correctly handle various protocol versions, extensions, authentication modes, and key exchange methods. Discover critical security vulnerabilities uncovered through systematic testing of popular open-source TLS implementations, including the FREAK flaw. Learn about the importance of formal verification for cryptographic protocol libraries and examine the first verified implementation of a composite TLS state machine in C. Gain insights into the complexities of TLS protocol design, the impact of state machine bugs, and the need for improved cryptographic protocol testing.

Intro
Agile Cryptographic Protocols
Transport Layer Security (1994)
TLS protocol overview
RSA Key Transport
(EC)DHE Key Exchange
Composing Key Exchanges
TLS State Machine
OpenSSL State Machine
Fuzzing TLS
Culprit: Underspecified State Machine
Composing with Optional Messages
SKIP: Server Impersonation with DHE
Export-Grade RSA in TLS
FREAK: Downgrade to RSA EXPORT
FREAK: Exploit and Impact
A Verified State Machine for OpenSSL
Conclusions Cryptographic protocol testing needs work