aalto1 untyped-item.component.html
Towards formally verifying the TLS 1.3 Key Schedule Security in SSBee
Loading...
URL
Journal Title
Journal ISSN
Volume Title
School of Science |
Master's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
Department
Major/Subject
Mcode
Degree programme
Language
en
Pages
195
Series
Abstract
TLS is one of the most important cryptographic protocols protecting communications on the Internet. The standardization process of TLS 1.3 prioritized addressing security issues over implementation concerns. Early drafts of TLS 1.3 standard welcomed inspiration from the cryptography community and specifically the OPTLS handshake by Krawczyk and Wee. TLS 1.3 key schedule is at the core of the TLS 1.3 handshake responsible for all cryptographic operations deriving keys for the handshake and record layer, such as handshake and application
traffic secrets, among others.
The main security requirement for the key schedule is to generate pseudorandom and unique keys given honest Diffie-Hellman shares or Pre-shared Key (PSK), or both (depending on the key exchange mode). Brzuska, Delignat-Lavaud, Egger, Fournet, Kohbrok, Kohlweiss (BDEFKK) (Asiacrypt, 2022) model these security goals and reduce the security of the TLS 1.3 standard key schedule (as appeared in the standard) to the security assumptions of the underlying primitives. BDEFKK capture the security properties of the key schedule in the State-separating Proofs (SSP) framework. SSP is one of the compositional frameworks in cryptography developed by the community for modular security analysis. SSP enables BDEFKK to break the complexity of the key schedule security games into several small components each with only one responsibility. However, their modular analysis is still long and over 100 pages which makes human verification difficult.
This thesis brings to light that formal verification of large scale proofs of real world protocols' cryptographic analysis is indeed approachable, provided the analysis itself utilizes modular analysis and verification-friendly proof framework that makes the gap with verification tools smaller. Specifically, we lay the foundations, formalize the security games, and take steps towards verification of one subtle lemma from the analysis of BDEFKK, pen-and-paper proof of which takes 10 pages of the paper, in SSBee. SSBee is a novel software toolchain (and at the time of writing this thesis, being actively developed by Chris Brzuska, Christoph Egger, and Jan Winkelmann) tailored particularly for formalizing reduction proofs written in the SSP framework. We successfully verify major statements in the lemma and find and add missing or minor details in the proof. Additionally, we highlight verification techniques discovered during different stages of the project. We conclude our verification story with our vision for future of SSBee with promising integrations with other tools for program verification.
Lastly, BDEFKK reduce the security of the key schedule to a new Salted Oracle Diffie-Hellman (SODH) assumption among others. Inspired by mmPRF-ODH assumption instantiation of Brendel, Fischlin, Günther, and Janson, we analyze the assumption in the random oracle model and partially reduce to the well-known Strong Diffie-Hellman (SDH) assumption introduced by Abdalla, Bellare, and Rogaway and formally verify one non trivial step of the reduction with SSBee. Although BDEFKK were more optimistically claiming that SODH assumption can be reduced to Computational Diffie-Hellman (CDH) assumption, this thesis explains why it seems too optimistic.
Description
Supervisor
Brzuska, ChrisThesis advisor
Mödersheim, SebastianBrzuska, Chris