Recently, Canetti and Krawczyk (Eurocrypt'2001) formu- lated a notion of security for key-exchange (ke) protocols, called SK- security, and showed that this notion suffices for constructing secure channels. However, their model and proofs do not suffice for proving more general composability properties of SK-secure ke protocols. We show that while the notion of SK-security is strictly weaker than a fully-idealized notion of key exchange security, it is sufficiently robust for providing secure composition with arbitrary protocols. In particular, SK-security guarantees the security of the key for any application that desires to set-up secret keys between pairs of parties. We also provide new definitions of secure-channels protocols with similarly strong com- posability properties, and show that SK-security suffices for obtaining these definitions. To obtain these results we use the recently proposed framework of uni- versally composable (UC) security. We also use a new tool, called non- information oracles, which will probably find applications beyond the present case. These tools allow us to bridge between seemingly limited indistinguishability-based definitions such as SK-security and more pow- erful, simulation-based definitions, such as UC security, where general composition theorems can be proven. Furthermore, based on such compo- sition theorems we reduce the analysis of a full-fledged multi-session key- exchange protocol to the (simpler) analysis of individual, stand-alone, key-exchange sessions.
Recently, Canetti and Krawczyk (Eurocrypt'2001) formu- lated a notion of security for key-exchange (ke) protocols, called SK- security, and showed that this notion suffices for constructing secure channels. However, their model and proofs do not suffice for proving more general composability properties of SK-secure ke protocols. We show that while the notion of SK-security is strictly weaker than a fully-idealized notion of key exchange security, it is sufficiently robust for providing secure composition with arbitrary protocols. In particular, SK-security guarantees the security of the key for any application that desires to set-up secret keys between pairs of parties. We also provide new definitions of secure-channels protocols with similarly strong com- posability properties, and show that SK-security suffices for obtaining these definitions. To obtain these results we use the recently proposed framework of uni- versally composable (UC) security. We also use a new tool, called non- information oracles, which will probably find applications beyond the present case. These tools allow us to bridge between seemingly limited indistinguishability-based definitions such as SK-security and more pow- erful, simulation-based definitions, such as UC security, where general composition theorems can be proven. Furthermore, based on such compo- sition theorems we reduce the analysis of a full-fledged multi-session key- exchange protocol to the (simpler) analysis of individual, stand-alone, key-exchange sessions.
The Universal Composability (UC) framework provides provable security guaranties for harsh application environment, where we want to construct protocols which keep security guarantees even when they are concurrently composed with arbitrary number of arbitrary (even hostile) protocols.This is a very strong guarantee.The UC-framework inherently supports the modular design, which allows secure composition of arbitrary number of UC-secure components with an arbitrary protocol.In contrast, traditional analysis and design is a stand alone analysis where security of a single instance is considered, i.e. an instance which is not in potential interaction with any concurrent instances.Furthermore, a typical traditional analysis is informal, i.e. without a formal proof.In spite of these facts, beyond the task of key-exchange this technology have not really took the attention of the community of applied cryptography.From practitioner's point of view the UC-world may seem more or less an academic interest of theoretical cryptographers.Accordingly we take a pragmatic approach, where we concentrate on meaningful compromises between the assumed adversarial strength, ideality wishes and realization complexity while keeping provable security guarantees within the UC-framework.We believe that even modest but provable goals (especially, if tunable to application scenarios) are interesting if a wider penetration of the UC-technology is desired into the daily-practice of protocol applications.
Key exchange protocols allow two parties to agree on a shared secret over an untrusted channel. A huge number of scientific works on key exchange have been published since the discovery of the first key exchange protocol, designed in 1976 by Diffie and Hellman [DH76]. The most prominent of these works is the game-based security model by Bellare and Rogaway [BR93], published in 1993 and, today, known as the "golden standard" for the security of key exchange protocols. The main purpose of key exchange protocols is to establish keys for a symmetric-key protocol such as a secure channel. Ideally, if both, the key exchange protocol and the channel protocol, are secure, then we would hope that they can be securely composed. While this is true for simulation-based security models [Can01, KT11, BPW03], game-based models usually lack composition theorems altogether. That is unfortunate, as they are often more suitable for real-life protocols such as TLS. Our first two composition theorems address the composition of BR-secure key exchange protocols with arbitrary symmetric-key protocols. We formally establish that an additional condition is necessary, namely, the key exchange requires a public session matching algorithm. Maybe surprisingly, many important key agreement protocols are not BR-secure due to the popular technique of explicit key confirmation. We devise a more flexible yet sufficiently strong model for this class of protocols and prove that it is closed under reductions. Overall, we devellop a tool for the modular analysis of real-life protocols and exemplify the use of our framwork on a profile of the TLS protocol. As in the case of most practical cryptography, information-theoretic security for key exchange protocols is out of reach, i.e., impossible in a formal sense. Therefore, protocols such as TLS rely on computational assumptions, e.g., the Diffie-Hellmann assumption or the hardness of factoring numbers. As the security of protocols is tightly related to the underlying complexity assumptions, researchers have been striving for simpler and weaker assumptions. The holy grail in this area is to base key agreement, one-way functions or simply any type of cryptography on the mere assumptions that NP does not equal P [FF93, BT03, AGGM06]. While positive results in this area remain elusive, there has been some recent progress on negative results [HMX10, PTV11], showing that cryptographic primitives such as hash functions cannot be based on NP-hardness unless coAM is contained in NP. In this thesis, we provide two oracle results that show that, via relativizing techniques, these negative results do not carry over to key agreement and regular one-way functions. In particular, we give an oracle relative to which the intersection of NP and coNP is easy while infinitely many often secure key agreement exists; and we give an oracle relative to which languages in the intersection of AM and coAM is easy while regular function families exists that are infinitely many often one-way.
In this paper, we present a simpler and more restricted variant of the universally composable security (UC) framework that is suitable for “standard ” two-party and multiparty computation tasks. Many of the complications of the UC framework exist in order to enable more general tasks than classic secure computation. This generality may be a barrier to entry for those who are used to the stand-alone model of secure computation and wish to work with universally composable security but are overwhelmed by the differences. The variant presented here (called simplified universally composable security, or just SUC) is closer to the definition of security for multiparty computation in the stand-alone setting. The main difference is that a protocol in the SUC framework runs with a fixed set of parties who know each other’s identities ahead of time, and machines cannot be added dynamically to the execution. As a result, the definitions of polynomial time and protocol composition are much simpler. In addition, the SUC framework has authenticated channels built in, as is standard in previous definitions of security, and all communication is done via the adversary in order to enable arbitrary scheduling of messages. Due to these differences, not all cryptographic tasks can be expressed in the SUC framework.
Assessing the security of key exchange protocols is a crucial task and turned out to be highly non-trivial.Many protocols proposed in the past have subsequently been broken.In order to provide a formal framework for security proofs, various security models have been defined.In this thesis, we analyse several such security models for key exchange protocols using the paradigm of constructive cryptography.We examine the exact constructive security guarantees and semantics that these notions provide.In particular, we compare constructive security definitions with a model proposed by Bellare and Rogaway, SK-security by Canetti and Krawczyk and a formal model for secure key exchange proposed by Shoup.i
Modeling security for protocols running in the complex network environment of the Internet can be a daunting task. Ideally, a security model for the Internet should provide the following guarantee: a protocol that implements a particular task specification will retain all the same security properties as the specification itself, even when an arbitrary set of protocols runs concurrently on the same network. This guarantee must hold even when other protocols are maliciously designed to interact badly with the analyzed protocol, and even when the analyzed protocol is composed with other protocols. The popular Universal Composability (UC) security framework aims to provide this guarantee.
Unfortunately, such strong security guarantees come with a price: they are impossible to achieve without the use of some trusted setup. Typically, this trusted setup is global in nature, and takes the form of a Public Key Infrastructure (PKI) and/or a Common Reference String (CRS). However, the current approach to modeling security in the presence of such setups falls short of providing expected security guarantees. A quintessential example of this phenomenon is the deniability concern: there exist natural protocols that meet the strongest known security notions (including UC) while failing to provide the same deniability guarantees that their task specifications imply they should provide.
We introduce the Generalized Universal Composability (GUC) framework to extend the UC security notion and enable the re-establishment of its original intuitive security guarantees even for protocols that use global trusted setups. In particular, GUC enables us to guarantee that secure protocols will provide the same level of deniability as the task specification they implement. To demonstrate the usefulness of the GUC framework, we first apply it to the analysis and construction of deniable authentication protocols. Building upon such deniable authentication protocols, we then prove a general feasibility result showing how to construct protocols satisfying our security notion for a large class of two-party and multi-party tasks (assuming the availability of some reasonable trusted setup). Finally, we highlight the practical applicability of GUC by constructing efficient protocols that securely instantiate two common cryptographic tasks: commitments and zero-knowledge proofs.
Introduced by Canetti in 2001, Universal Composability (UC) is a widely adopted security model that enables the specification and proof of security for a broad range of protocols, offering strong security guarantees. At its core lies the universal composition theorem (UC theorem), which ensures that protocols proven secure within the framework remain secure even when deployed in real-world environments with multiple instances of them. In this work, we present two key contributions. First, we identify several problems with the UC framework, in particular the UC Theorem. They include counterexamples, limitations that make it unusable for important classes of protocols, and weaknesses in its proof. These problems reveal flaws in nearly all the fundamental concepts of UC. Second, we propose a revised formulation of the main concepts of UC to address these issues. Although the resulting modifications are nontrivial, our updated definitions are designed to remain as faithful as possible to the structure and intent of the original model.