Public defence in Computer Science, M.Sc. Konrad Kohbrok

Title of the thesis: State-Separating Proofs and Their Applications

Doctoral student: Konrad Kohbrok
Opponent: Prof. Tibor Jager, Bergische University Wuppertal, Germany
Custos: Prof. Chris Brzuska, Aalto University School of Science, Department of Computer Science

Thesis available for public display 10 days prior to the defence at: https://aaltodoc.aalto.fi/doc_public/eonly/riiputus/

A Modular Approach to Taming the Complexity of Cryptographic Protocols 

Cryptographic protocols such as the Transport Layer Security (TLS) protocol that underpins HTTPS ensure confidentiality and integrity of our online communication. Because of the complexity of protocols like TLS, the cryptographic community has developed tools to ease their analysis, e.g., frameworks that allow for a modular approach, or computer-aided techniques that automate parts of the analysis. 

In this thesis, we introduce the State-Separating Proofs (SSP) framework, which iterates on the commonly used code-based game-playing style of defining cryptographic security. In contrast to existing frameworks which are mostly definitional in nature, the SSP framework provides a graph-based modularization technique based on the separation of component state that eases both writing and verification of proofs. In particular, the framework allows for the re-use of components which, among other things, greatly simplifies proofs of simulation correctness, a recurring part of most cryptographic security proofs. We also show the efficacy of the SSP framework by successfully applying it to prove the security of core components of the TLS protocol, as well as the Messaging Layer Security (MLS) protocol, an emerging protocol developed by the Internet Engineering Task Force as the new standard for secure messaging. Finally, we show how the SSP framework can be used to guide computer-aided proofs by proving the security of the cryptobox protocol using the EasyCrypt proof assistant.

Doctoral theses in the School of Science: https://aaltodoc.aalto.fi/handle/123456789/52