On the Concrete Security of TLS 1.3 PSK Mode
Hannah Davis, Denis Diemert, Felix Günther, Tibor Jager
Abstract
The pre-shared key (PSK) handshake modes of TLS 1.3 allow for the performant, low-latency resumption of previous connections and are widely used on the Web and by resource-constrained devices, e.g., in the Internet of Things. Taking advantage of these performance benefits with optimal and theoretically-sound parameters requires tight security proofs. We give the first tight security proofs for the TLS 1.3 PSK handshake modes.
Our main technical contribution is to address a gap in prior tight security proofs of TLS 1.3 which modeled either the entire key schedule or components thereof as independent random oracles to enable tight proof techniques. These approaches ignore existing interdependencies in TLS 1.3's key schedule, arising from the fact that the same cryptographic hash function is used in several components of the key schedule and the handshake more generally. We overcome this gap by proposing a new abstraction for the key schedule and carefully arguing its soundness via the indifferentiability framework. Interestingly, we observe that for one specific configuration, PSK-only mode with hash function SHA-384, it seems difficult to argue indifferentiability due to a lack of domain separation between the various hash function usages. We view this as an interesting insight for the design of protocols, such as future TLS versions.
For all other configurations however, our proofs significantly tighten the security of the TLS 1.3 PSK modes, confirming standardized parameters (for which prior bounds provided subpar or even void guarantees) and enabling a theoretically-sound deployment.
Ask about this paper
Ask your agent about it.
Lune has read the top-tier papers around this one, so every answer names the papers it rests on.
Your agent calls
Lunesearch_papers
Free to start. No credit card required.
Terminal
Install the CLIlune papers get f4199591-dab3-45c3-9fc8-3ab15cd3b98cCited by top-tier papers2
- On the Tight Security of the Double RatchetDaniel Collins, Doreen Riepel, Si An Oliver TranCCS 2024 · 3 citations
- Formal Analysis of SPDM: Security Protocol and Data Model version 1.2Cas Cremers, Alexander Dax, Aurora NaskaUSENIX Security 2023
Related papers
- Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed AuthenticationCas Cremers, Marko Horvat, Sam Scott, Thyla van der MerweS&P 2016 · 128 citations
- Multiple Handshakes Security of TLS 1.3 CandidatesXinyu Li, Jing Xu, Zhenfeng Zhang, Dengguo Feng et al.S&P 2016 · 32 citations
- Downgrade Resilience in Key-Exchange ProtocolsKarthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green et al.S&P 2016 · 54 citations
- Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3Marc Fischlin, Felix Günther, Benedikt Schmidt, Bogdan WarinschiS&P 2016 · 1 citation
- A Comprehensive Symbolic Analysis of TLS 1.3Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott et al.CCS 2017 · 247 citations
