Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate

Explore a comprehensive analysis of the TLS 1.3 Draft-18 protocol in this IEEE Symposium on Security & Privacy conference talk. Delve into the clean-slate design of TLS 1.3, examining its ability to prevent legacy problems and potential vulnerabilities. Learn about the methodology for developing verified symbolic and computational models of TLS 1.3 alongside a high-assurance reference implementation. Discover how ProVerif models are used to evaluate various TLS 1.3 versions against known and previously unpublished vulnerabilities. Examine the computational CryptoVerif model for TLS 1.3 Draft-18 and its security proofs. Investigate RefTLS, an interoperable implementation of TLS 1.0-13, and its automatic analysis through ProVerif model extraction from typed JavaScript code. Gain insights into recent attacks on legacy crypto in TLS, modeling weak crypto in ProVerif, and writing and verifying security goals for TLS 1.3.

Intro
Transport Layer Security (TLS) 1.3
Our Approach
Recent Attacks on Legacy Crypto in TLS
Modeling Weak Crypto in ProVerif
Modeling TLS 1.3 in ProVerif
Writing and Verifying Security Goals
Cryptographic Assumptions for TLS 1.3
More Unusual Proof Assumptions
Manual Proof of Composition for full TLS 1.3
RefTLS: A Reference TLS Implementation
RefTLS Architecture
Results and Limitations