State-Separating Proofs and Their Applications

Abstract

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.