A pretty proof of TLS 1.3 (well, almost :-))
- LecturerProf. Dr. Christoph Egger (main) & Prof. Chris Brzuska (insights on TLS and post-talk reflections) (IRIF& Aalto University)
Host: Kai-Min Chung - Time2022-12-13 (Tue.) 14:00 ~ 15:00
- LocationAuditorium 106 at IIS new Building
Abstract
We present an analysis of the TLS 1.3 handshake (key exchange) protocol and explain (1) our conceptual insights in the protocol design and (2) modular proof techniques for managing the complexity of TLS 1.3.
A core idea in the analysis is that of a *key schedule*. It captures the key derivations in TLS and is a fairly complex primitive in itself. Analyzing the key schedule separately makes it easier to prove the security of the key exchange protocol of TLS 1.3. Additionally, the key schedule is a (symmetric-key) primitive which is nicer to analyze than an interactive protocol.
Towards modular proofs, we represent our security game as graphs with both visual appeal and formal meaning. Namely, we write our security game for the key schedule in stateful pieces of code which call one another such that code + call-graph defines the security game. We will see that reductions simply boil down to drawing cuts in graphs which is a nice and convenient feature.
The talk is based on:
Key Schedule Security for the TLS 1.3 Handshake https://static.siccegge.de/pdfs/BDEFKK22.pdf
State-separation for game-playing proofs:
https://eprint.iacr.org/2018/306
A core idea in the analysis is that of a *key schedule*. It captures the key derivations in TLS and is a fairly complex primitive in itself. Analyzing the key schedule separately makes it easier to prove the security of the key exchange protocol of TLS 1.3. Additionally, the key schedule is a (symmetric-key) primitive which is nicer to analyze than an interactive protocol.
Towards modular proofs, we represent our security game as graphs with both visual appeal and formal meaning. Namely, we write our security game for the key schedule in stateful pieces of code which call one another such that code + call-graph defines the security game. We will see that reductions simply boil down to drawing cuts in graphs which is a nice and convenient feature.
The talk is based on:
Key Schedule Security for the TLS 1.3 Handshake https://static.siccegge.de/pdfs/BDEFKK22.pdf
State-separation for game-playing proofs:
https://eprint.iacr.org/2018/306