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.
@INPROCEEDINGS{BhargavanBlanchetKobeissiSP2017,
AUTHOR = {Karthikeyan Bhargavan and Bruno Blanchet and Nadim Kobeissi},
TITLE = {Verified Models and Reference Implementations for the {TLS} 1.3 Standard Candidate},
BOOKTITLE = {IEEE Symposium on Security and Privacy (S\&P'17)},
YEAR = 2017,
PAGES = {483--503},
MONTH = MAY,
ADDRESS = {San Jose, CA},
PUBLISHER = {IEEE},
NOTE = {{\bfseries Distinguished paper award}}
}