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.
Type de document :
Article dans une revue
IEEE Security & Privacy, IEEE, 2016, 14 (6), pp.18-25. 〈10.1109/MSP.2016.123〉
Liste complète des métadonnées
Contributeur : Bhargavan Karthikeyan <>
Soumis le : mercredi 4 janvier 2017 - 09:31:18
Dernière modification le : jeudi 26 avril 2018 - 10:28:22




Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss. miTLS: Verifying Protocol Implementations against Real-World Attacks. IEEE Security & Privacy, IEEE, 2016, 14 (6), pp.18-25. 〈10.1109/MSP.2016.123〉. 〈hal-01425964〉



Consultations de la notice