miTLS: Verifying Protocol Implementations against Real-World Attacks

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss

Research output: Contribution to journalArticlepeer-review


The TLS Internet Standard, previously known as SSL, is the default protocol for encrypting communications between clients and servers on the Web. Hence, TLS routinely protects our sensitive emails, health records, and payment information against network-based eavesdropping and tampering. For the past 20 years, TLS security has been analyzed in various cryptographic and programming models to establish strong formal guarantees for various protocol configurations. However, TLS deployments are still often vulnerable to attacks and rely on security experts to fix the protocol implementations. The miTLS project intends to solve this apparent contradiction between published proofs and real-world attacks, which reveals a gap between TLS theory and practice. To this end, the authors developed a verified reference implementation and a cryptographic security proof that account for the protocol's low-level details. The resulting formal development sheds light on recent attacks, yields security guarantees for typical TLS usages, and informs the design of the protocol's next version.
Original languageEnglish
Pages (from-to)18-25
Number of pages8
JournalIEEE Security and Privacy
Issue number6
Publication statusPublished - 16 Dec 2016

Fingerprint Dive into the research topics of 'miTLS: Verifying Protocol Implementations against Real-World Attacks'. Together they form a unique fingerprint.

Cite this