Skip to Main content Skip to Navigation
Journal articles

miTLS: Verifying Protocol Implementations against Real-World Attacks

Abstract : 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.
Complete list of metadata

https://hal.inria.fr/hal-01425964
Contributor : Bhargavan Karthikeyan <>
Submitted on : Wednesday, January 4, 2017 - 9:31:18 AM
Last modification on : Tuesday, April 21, 2020 - 10:18:04 AM

Links full text

Identifiers

Collections

Citation

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss. miTLS: Verifying Protocol Implementations against Real-World Attacks. IEEE Security and Privacy Magazine, Institute of Electrical and Electronics Engineers, 2016, 14 (6), pp.18-25. ⟨10.1109/MSP.2016.123⟩. ⟨hal-01425964⟩

Share

Metrics