A pretty proof of TLS 1.3 (well, almost :-))
- 講者Dr. Christoph Egger (main) & Prof. Chris Brzuska (insights on TLS and post-talk reflections) 教授 (法國基礎計算機科學研究所(IRIF) & 芬蘭阿爾託大學(Aalto University)副教授)
邀請人：鐘楷閔 - 時間2022-12-13 (Tue.) 14:00 ~ 15:00
- 地點資訊所新館106演講廳
摘要
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