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

Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Implementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes, and key exchange methods. Confusingly, each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that correctly multiplexes between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years, and have now finally been patched due to our disclosures. Several of these vulnerabilities, including the recently publicized FREAK flaw, enable a network attacker to break into TLS connections between authenticated clients and servers. We argue that state machine bugs stem from incorrect compositions of individually correct state machines. We present the first verified implementation of a composite TLS state machine in C that can be embedded into OpenSSL and accounts for all its supported cipher suites. Our attacks expose the need for the formal verification of core components in cryptographic protocol libraries, our implementation demonstrates that such mechanized proofs are within reach, even for mainstream TLS implementations.
Original languageEnglish
Title of host publication2015 IEEE Symposium on Security and Privacy
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages18
ISBN (Electronic)978-1-4673-6949-7
Publication statusPublished - 20 Jul 2015
Event2015 IEEE Symposium on Security and Privacy - The Fairmont, San Jose, CA, United States
Duration: 18 May 201520 May 2015

Publication series

ISSN (Print)1081-6011
ISSN (Electronic)2375-1207


Conference2015 IEEE Symposium on Security and Privacy
Country/TerritoryUnited States
CitySan Jose, CA
Internet address


  • cryptographic protocols
  • formal verification
  • TLS protocol
  • authentication modes
  • composite TLS state machine
  • key exchange methods
  • message sequence
  • open-source TLS
  • security vulnerabilities
  • transport layer security protocol
  • Authentication
  • Computer bugs
  • Cryptography
  • Libraries
  • Protocols
  • Servers
  • Transport Layer Security
  • formal methods
  • man-in-the-middle attacks
  • software verification


Dive into the research topics of 'A Messy State of the Union: Taming the Composite State Machines of TLS'. Together they form a unique fingerprint.

Cite this