Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate

Abstract : TLS 1.3 is the next version of the Transport Layer Security (TLS) protocol. Its clean-slate design is a reaction both to the increasing demand for low-latency HTTPS connections and to a series of recent high-profile attacks on TLS. The hope is that a fresh protocol with modern cryptography will prevent legacy problems; the danger is that it will expose new kinds of attacks, or reintroduce old flaws that were fixed in previous versions of TLS. After 18 drafts, the protocol is nearing completion, and the working group has appealed to researchers to analyze the protocol before publication. This paper responds by presenting a comprehensive analysis of the TLS 1.3 Draft-18 protocol. We seek to answer three questions that have not been fully addressed in previous work on TLS 1.3: (1) Does TLS 1.3 prevent well-known attacks on TLS 1.2, such as Logjam or the Triple Handshake, even if it is run in parallel with TLS 1.2? (2) Can we mechanically verify the computational security of TLS 1.3 under standard (strong) assumptions on its cryptographic primitives? (3) How can we extend the guarantees of the TLS 1.3 protocol to the details of its implementations? To answer these questions, we propose a methodology for developing verified symbolic and computational models of TLS 1.3 hand-in-hand with a high-assurance reference implementation of the protocol. We present symbolic ProVerif models for various intermediate versions of TLS 1.3 and evaluate them against a rich class of attacks to reconstruct both known and previously unpublished vulnerabilities that influenced the current design of the protocol. We present a computational CryptoVerif model for TLS 1.3 Draft-18 and prove its security. We present RefTLS, an interoperable implementation of TLS 1.0-1.3 and automatically analyze its protocol core by extracting a ProVerif model from its typed JavaScript code.
Type de document :
Communication dans un congrès
38th IEEE Symposium on Security and Privacy , May 2017, San Jose, United States. pp.483 - 502, 2017, 〈10.1109/SP.2017.26〉
Liste complète des métadonnées

Littérature citée [71 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01575920
Contributeur : Bruno Blanchet <>
Soumis le : lundi 21 août 2017 - 19:43:17
Dernière modification le : mercredi 23 août 2017 - 01:10:16

Fichier

BhargavanBlanchetKobeissiSP201...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Relations

  • est une partie de hal-01528752 - Companion technical report

Citation

Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. 38th IEEE Symposium on Security and Privacy , May 2017, San Jose, United States. pp.483 - 502, 2017, 〈10.1109/SP.2017.26〉. 〈hal-01575920〉

Partager

Métriques

Consultations de
la notice

41

Téléchargements du document

14