A Unilateral-to-Mutual Authentication Compiler for Key Exchange (with Applications to Client Authentication in TLS 1.3)
Hugo Krawczyk
Abstract
We study the question of how to build "compilers" that transform a unilaterally authenticated (UA) key-exchange protocol into a mutually-authenticated (MA) one. We present a simple and efficient compiler and characterize the UA protocols that the compiler upgrades to the MA model, showing this to include a large and important class of UA protocols. The question, while natural, has not been studied widely. Our work is motivated in part by the ongoing work on the design of TLS 1.3, specifically the design of the client authentication mechanisms including the challenging case of post-handshake authentication. Our approach supports the analysis of these mechanisms in a general and modular way, in particular aided by the notion of "functional security" that we introduce as a generalization of key exchange models and which may be of independent interest.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers3
- Verified Models and Reference Implementations for the TLS 1.3 Standard CandidateKarthikeyan Bhargavan, Bruno Blanchet, Nadim KobeissiS&P 2017 · 233 citations
- Implementing and Proving the TLS 1.3 Record LayerAntoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko et al.S&P 2017 · 20 citations
- Formal Analysis of SPDM: Security Protocol and Data Model version 1.2Cas Cremers, Alexander Dax, Aurora NaskaUSENIX Security 2023
Builds on1
Related papers
- 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
- Password-Authenticated TLS via OPAQUE and Post-Handshake AuthenticationJulia Hesse, Stanislaw Jarecki, Hugo Krawczyk, Christopher A. WoodEUROCRYPT 2023 · 9 citations
- A Comprehensive Symbolic Analysis of TLS 1.3Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott et al.CCS 2017 · 247 citations
- Quantifying the Security Cost of Migrating Protocols to PracticeChristopher Patton, Thomas ShrimptonCRYPTO 2020 · 2 citations
- 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
