State-Separating Proofs and Their Applications

Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | Doctoral thesis (article-based) | Defence date: 2023-08-10
Degree programme
62 + app. 126
Aalto University publication series DOCTORAL THESES, 112/2023
Cryptographic protocols are commonly used to provide security for network traffic and digital interactions in general. Security means different things in different contexts. The most common security properties include confidentiality and authenticity of transmitted information, but cryptographicprotocols can also provide more sophisticated security properties such as unlinkability or deniability. Cryptographers typically use reduction proofs to show that a given protocol indeed provides a certain type of security. A prerequisite for such a proof is the formal description of the desired security notion. One way to achieve this formalization is the code-based game-playing framework introduced by Bellare and Rogaway [10], where security is encoded as a game played by a computationally boundedadversary. The game provides the adversary access to a set of oracles, which are defined through (pseudo-)code and which the adversary can query (or call) similar to functions in a computer program. Intuitively, the adversary wins the game if it can defeat the security of the protocol in question. A protocol is thus secure if the probability of an adversary winning the security game is sufficiently close to random chance. For example, we can define the security of a protocol aiming to allow two parties to agree on a secret key as follows: A protocol of this kind is secure if any adversary observing the protocol flow between two honest parties has a sufficiently low probability of distinguishing the resulting key from a randomly sampled string (thus expressing that the adversary has learned nothing about the real key). Despite the structure and formalism introduced by Bellare and Rogaway’s code-based gameplaying framework, security definitions for larger protocols are still often complex and their proofs error-prone and hard to verify. A variety of frameworks exist to allow for composed definitions and modularization of proofs. With the State Separating Proofs framework, this thesis includes (in Publication I) one such framework. The SSP framework builds on that introduced by Bellare and Rogaway by leveraging the separation of state within a model to facilitate compositional proofs. This thesis also includes several security proofs of real world protocols (or components thereof) to showcase the strengths and weaknesses of the SSP framework. In particular, the thesis includes a security proof of the key derivations of draft 11 of the Messaging Layer Security protocol (Publication III) the key schedule of the Transport Layer Security protocol (Version 1.3, Publication II), as well as a security protocol of a novel scheme for rotating signature keys (RSIG, Publication IV). This thesis also includes a computer-aided security proof of the cryptobox protocol (part of the NaCl library [11]) using the EasyCrypt [7] tool chain, where the SSP framework was used to guide both security modelling and proof (Publication V). Finally, we discuss the SSP framework in the context of related work such as other compositional frameworks and computer-aided cryptography.
Supervising professor
Brzuska, Chris, Prof., Aalto University, Department of Mathematics and Systems Analysis, Finland
Thesis advisor
Brzuska, Chris, Prof., Aalto University, Department of Mathematics and Systems Analysis, Finland
Delignat-Lavaud, Antoine, Microsoft Research Cambridge, UK
Kohlweiss, Markulf, Prof., University of Edinburgh, UK
compositional frameworks, protocol analysis, key exchange
Other note
  • [Publication 1]: Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Konrad Kohbrok, Markulf Kohlweiss. State Separation for Code-Based Game-Playing Proofs. In Advances in Cryptology – ASIACRYPT 2018, Pages 222-249, October 2018.
    DOI: 10.1007/978-3-030-03332-3_9 View at publisher
  • [Publication 2]: Chris Brzuska, Antoine Delignat-Lavaud, Christoph Egger, Cédric Fournet, Konrad Kohbrok, Markulf Kohlweiss. Key Schedule Security for the TLS 1.3 Standard. In Advances in Cryptology – ASIACRYPT 2022, Pages 621-650, December 2022.
    DOI: 10.1007/978-3-031-22963-3_21 View at publisher
  • [Publication 3]: Chris Brzuska, Eric Cornelissen, Konrad Kohbrok. Security Analysis of the MLS Key Derivation. In Proceedings of the IEEE Symposium on Security & Privacy 2022, Pages 2535-2553, May 2022.
    DOI: 10.1109/SP46214.2022.9833678 View at publisher
  • [Publication 4]: Cas Cremers, Britta Hale and Konrad Kohbrok. The Complexities of Healing in Secure Group Messaging: Why Cross-Group Effects Matter. In Proceedings of the 30th USENIX Security Symposium, Pages 1847-1864, August 11-13 2021.
    Full text in Acris/Aaltodoc:
  • [Publication 5]: François Dupressoir, Konrad Kohbrok, Sabine Oechsner. Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox. In 2022 IEEE 35th Computer Security Foundations Symposium (CSF), Pages 211-226, August 2022.
    DOI: 10.1109/CSF54842.2022.9919671 View at publisher