In response to standardization requests regarding password-authenticated key exchange (PAKE) protocols, the IRTF working group CFRG has setup a PAKE selection process in 2019, which led to the selection of the CPace protocol in the balanced setting, in which parties share a common password. In subsequent standardization efforts, the CPace protocol further developed, yielding a protocol family whose actual security guarantees in practical settings are not well understood. In this paper, we provide a comprehensive security analysis of CPace in the universal composability framework. Our analysis is realistic in the sense that it captures adaptive corruptions and refrains from modeling CPace’s \(\textsf {Map2Pt}\) function that maps field elements to curve points as an idealized function. In order to extend our proofs to different CPace variants optimized for specific elliptic-curve ecosystems, we employ a new approach which represents the assumptions required by the proof as libraries accessed by a simulator. By allowing for the modular replacement of assumptions used in the proof, this new approach avoids a repeated analysis of unchanged protocol parts and lets us efficiently analyze the security guarantees of all the different CPace variants. As a result of our analysis, all of the investigated practical CPace variants enjoy adaptive UC security.
In response to standardization requests regarding password-authenticated key exchange (PAKE) protocols, the IRTF working group CFRG has setup a PAKE selection process in 2019, which led to the selection of the CPace protocol in the balanced setting, in which parties share a common password. In subsequent standardization efforts, the CPace protocol further developed, yielding a protocol family whose actual security guarantees in practical settings are not well understood. In this paper, we provide a comprehensive security analysis of CPace in the universal composability framework. Our analysis is realistic in the sense that it captures adaptive corruptions and refrains from modeling CPace’s (\textsf {Map2Pt}) function that maps field elements to curve points as an idealized function. In order to extend our proofs to different CPace variants optimized for specific elliptic-curve ecosystems, we employ a new approach which represents the assumptions required by the proof as libraries accessed by a simulator. By allowing for the modular replacement of assumptions used in the proof, this new approach avoids a repeated analysis of unchanged protocol parts and lets us efficiently analyze the security guarantees of all the different CPace variants. As a result of our analysis, all of the investigated practical CPace variants enjoy adaptive UC security.
A Password-Authenticated Key Exchange (PAKE) protocol allows two parties to agree upon a cryptographic key, when the only information shared in advance is a low-entropy password. The standard security notion for PAKE (Canetti et al., Eurocrypt 2005) is in the Universally Composable (UC) framework. We show that unlike most UC security notions, UC PAKE does not imply correctness. While Canetti et al. has briefly noticed this issue, we present the first comprehensive study of correctness in UC PAKE: We show that TrivialPAKE, a no-message protocol that does not satisfy correctness, is a UC PAKE; We propose nine approaches to guaranteeing correctness in the UC security notion of PAKE, and show that seven of them are equivalent, whereas the other two are unachievable; We prove that a direct solution, namely changing the UC PAKE functionality to incorporate correctness, is impossible; Finally, we show how to naturally incorporate correctness by changing the model—we view PAKE as a three-party protocol, with the man-in-the-middle adversary as the third party. In this way, we hope to shed some light on the very nature of UC-security in the man-in-the-middle setting.
Message authentication and key exchange are two of the most basic tasks of cryptography. Solutions based on public-key infrastructure (PKI) are prevalent. Still, the state of the art in composable security analysis of PKI-based authentication and key exchange is somewhat unsatisfactory. Specifically, existing treatments either (a) make the unrealistic assumption that the PKI is accessible only within the confines of the protocol itself, thus failing to capture real-world PKI-based authentication, or (b) impose oftenunnecessary requirements—such as strong on-line non-transferability—on candidate protocols, thus ruling out natural candidates. We give a modular and universally composable analytical framework for PKI-based message authentication and key exchange protocols. This framework guarantees security even when the PKI is pre-existing and globally available, without being unnecessarily restrictive. Specifically, we model PKI as a global set-up functionality within the Global UC security model [Canetti et al., TCC 2007] and relax the ideal authentication and key exchange functionalities accordingly. We then demonstrate the security of basic signature-based authentication and key exchange protocols. Our modeling makes minimal security assumptions on the PKI in use; in particular, “knowledge of the secret key” is not needed.
Through constructing and utilizing non-malleable,extractable,and weak simulation-sound trapdoor commitment schemes and corresponding smooth projective hash function familes,this paper proposes an efficient two-party password authenticated key exchange(PAKE) protocol within the universal composable(UC) framework,which is the optimal two-round PAKE protocol in this setting.Rigorous security proofs based on standard assumptions in the presence of static corruption adversary are then given out.Comparisons with previously proposed protocols show that,this protocol avoids the use of zero-knowledge protocols,and achieves a higher performance in terms of communication efficiency while attaining a comparable computational complexity.
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.
Message authentication is one of the most basic tasks of cryptography, and authentication based on public-key infrastructure (PKI) is one of the most prevalent methods for message and entity authentication. Still, the state of the art in composable security analysis of PKI-based authentication is somewhat unsatisfactory. Specifically, existing treatments either (a) make the unrealistic assumption that the PKI is accessible only within the confines of the authentication protocol itself, thus failing to capture real-world PKI-based authentication, or (b) impose often-unnecessary requirements—such as strong on-line non-transferability—on candidate protocols, thus ruling out natural candidates. We give a modular and composable analytical framework for PKI-based message authentication protocols. This framework guarantees security even when the PKI is pre-existing and globally available, without being unnecessarily restrictive. Specifically, we model PKI as a global set-up functionality within the Global UC security model [Canetti et al., TCC 2007] and relax the ideal authentication functionality accordingly. We then demonstrate the security of a simple signature-based authentication protocol. Our modeling makes minimal security assumptions on the PKI in use; in particular, “knowledge of the secret
Security protocols, such as TLS, SSH, IEEE~802.11, and DNSSEC, have become crucial tools in modern society to protect people, data, and infrastructure. They are used throughout virtually all electronic devices to achieve a wide range of different security goals, such as confidentiality, authentication, and integrity. As the long history of attacks on security protocols illustrates, it is indispensable to perform a formal security analysis of such protocols. A central tool in cryptography for taming the complexity of the design and the analysis of modern protocols is modularity, provided by security models for universal composability. Such models allow for designing and analyzing small parts of a protocol in isolation and then reusing these security results in the context of the overall protocol. This is not just easier than analyzing the whole protocol as a monolithic block but also reduces the overall effort required in building and analyzing multiple different protocols based on the same underlying components, such as cryptographic primitives. Ideally, a model for universal composability should support a protocol designer in easily creating full, precise, and detailed specifications as well as sound security proofs of various protocols for various types of adversarial models, instead of being an additional obstacle one has to overcome during a security analysis. In particular, such a model should be sound, flexible/expressive, and easy to use. Unfortunately, despite the wide spread use of models for universal composability, existing models and frameworks are still unsatisfying in these respects as none combines all of these requirements simultaneously. In this thesis we therefore develop a model for universal composability, called the iUC framework, which combines soundness, usability, and flexibility in a so far unmatched way, and hence constitutes a solid framework for designing and analyzing essentially any protocol and application in a modular, universally composable, and sound manner. We use our model in a case study to analyze multiple different key exchange protocols precisely as they are deployed in practice. This illustrates the combination of both flexibility and usability of our model. This case study is also an important independent contribution as this is the first faithful security analysis of these unmodified protocols in a universal composability setting.