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.
Complete list of metadatas

Cited literature [85 references]  Display  Hide  Download

https://hal.inria.fr/hal-01528752
Contributor : Bruno Blanchet <>
Submitted on : Thursday, December 20, 2018 - 4:13:41 PM
Last modification on : Thursday, February 7, 2019 - 5:09:35 PM
Long-term archiving on : Friday, March 22, 2019 - 1:04:01 PM

File

RR-9040.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01528752, version 3

Collections

Citation

Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. [Research Report] RR-9040, Inria Paris. 2017, pp.51. ⟨hal-01528752v3⟩

Share

Metrics

Record views

632

Files downloads

312