On Generalizations of Composable Security
Daniel Jost
Cryptography is a cornerstone for the protection of the digital society, and security definitions lie at the heart of cryptographic research. Their importance stems from the fact that for a cryptographic scheme, in contract to its correctness, security cannot simply be demonstrated. Rather, the widely accepted paradigm is to build confidence by mathematically proving their security. This foremost requires to have a sound and meaningful mathematical security model, such that the implied guarantees actually correspond to the intended properties.
The paradigm of provable security can be traced back to Shannon's seminal work on the one-time pad encryption. His custom-made and purely information-theoretic definition, however, does not handily generalize to other types of schemes and flavors of security. Nowadays, most security definitions are game-based, meaning that a protocol is secure if an attacker is unable to perform a certain set of attacks in a prescribed and simplified interaction with the scheme. This, however, has severe drawbacks. First, the match between the formal security definition and the intended use-case of the corresponding application is not performed rigorously, but typically only argued informally. Second, such security definitions do not compose. For instance, a provably secure symmetric encryption scheme might turned out insecure when combined with a provably secure key-agreement scheme, due to the lack of composability of the respective definitions.
A in many respects superior approach are composable (sometimes called simulation-based) security frameworks. In such a framework, the goal of a cryptographic primitive can be seen as providing a construction of a so-called ideal resource from an assume resource, for a well-defined construction notion. The ideal resource thereby formalizes what must be achieved---in any possible context---in a clean and abstract manner. For instance, the goal of an encryption scheme can be seen as construction of a secure channel that does not leak the messages, but at most their length, to an eavesdropper, hence making the achieved guarantees explicit rather than listing excluded attacks. The assumed resource, on the other hand, makes explicit what is required to be available to the involved parties, e.g., a shared secret key and an authentication channel.Moreover, by design, those frameworks ensure that the security of an overall scheme is directly implied by the security of its components, making them well suited for modular protocol designs and analyses.
However, up to now, the adoption of composable security statements has been hindered by a number of obstacles. In particular, the imposed abstraction boundaries lack flexibility, impeding modularity as it prevents certain resources from being decomposed. Moreover, the traditional types of composable security statements are frequently overly specific, e.g., encoding a very particular assumed or constructed resource, hindering their reuse.Some popular abstraction boundaries, such as the random oracle, are even known to be outright impossible to construct from resources readily available in the real world.In addition, composable frameworks are also met with some skepticism because of many impossibility results; goals such as commitments and zero-knowledge that are achievable in a stand-alone sense were shown to be unachievable composably (without a setup). In particular, in the context of adaptive security, the so-called "simulator commitment problem" arises: once a party gets corrupted, an efficient simulator is unable to be consistent with its pre-corruption outputs.
Generalizing Constructive Cryptography. In this thesis, we generalize and extend the Constructive Cryptography framework in three ways to overcome those limitations.
First, we propose the extension of the Constructive Cryptography framework by so-called global event histories, to enable more flexible abstraction boundaries. That is, in addition to the traditional input-output behavior, each resource can trigger events from a predefined set. Other resources can then depend on the global event history, i.e., on which events having occurred so far and in which order. For example, a key resource (one module) can now export the event of having been leaked, upon which a channel (another, apparently independent module) can degrade its security guarantees.
Second, we propose the notion of context-restricted constructions. Context-restricted constructions allow us to model that certain resources can only be used in an explicitly specified set of contexts.Such a notion with explicitly limited composition guarantees is particularly useful when dealing with abstractions such as a random oracle, where no weaker and feasible to instantiate, yet useful abstraction boundary are known. As an application, we then show that the notion of universal computational extractors (UCE), introduced by Bellare et al. as an alternative to the random oracle model, can be understood as a special case of context-restricted constructions.
Third, we revisit the so-called simulator commitment problem, that mainly occurs in the context of adaptive security. We introduce a novel composable security notion that is able to express thecomposable guarantees of schemes that previously only admitted standalone security definitions, while providing clean semantics of how the guarantees should be interpreted, holding in any environment, and being equipped with a composition theorem.In a nutshell, we introduce interval-wise guarantees formalizing properties that hold in between two events, not forcing the simulation to be consistent between the intervals (the root of the commitment issues). On a technical level, we leverage the specification-based approach of the CC framework, where proving a protocol $\pi$ to be secure corresponds to modeling the assumed real-world specification $\mathcal{R}$, and showing that $\pi \mathcal{R}$ is contained in an ideal specification $\mathcal{S}$. We formalize interval-wise guarantees as a novel type of specifications and develop the required theory.
A case study. Finally, we consider two-party secure messaging, proposing the first systematic and composable security model thereof. Taking advantage of our notion of global events, we develop a unified and easily reusable type security statement for each of the involved sub-protocol. This is in stark contrast to existing game-based security treatments, where the security games of sub-protocols are tailored to the overall protocol analysis, impeding their reuse in other protocols and contexts. Furthermore, we utilize our novel types of specifications to deal with the commitment problem, naturally occurring in secure messaging where one considers adaptive exposure of parties' secret state.
BibTeX Citation
@phdthesis{Jost20,
author = {Daniel Jost},
title = {On Generalizations of Composable Security},
year = {2020},
month = {3},
school = {ETH Zurich},
}