Security Extension for Bresson-Chevassut-Pointcheval's model

Chunjie Cao, Jianfeng Ma, SangJae Moon

Published Jan 1, 2006• 0 citations

Abstract

The Bresson-Chevassut-Pointcheval (BCP) model is a formalism for the analysis of authenticated group key exchange protocols. Also there are some desired security goals for a practical group key exchange protocol, which are necessary in achieving resistance to active attacks mounted by an increasingly powerful adversary. However, whether a proved secure protocol in the BCP model can meet these security goals remains unknown. Firstly, the relationship between the BCP model and the desired security goals is analyzed in this paper. And it is shown that a protocol proved authenticated key exchange (AKE) security in the BCP model can surely achieve some security goals such as key independence, resistance to all types of passive attacks, Perfect Forward Secrecy (PFS) and implicit key authentication, but can not provide key integrity and known-key security. It is the lack of group key consistency in the definition of AKE security that causes the security flaws. Then, we present new definition of group key (GK) security, and show that a proved GK secure protocol can guarantee all the desired security goals. Key words: Provable security, Distributed computing, Formal model,

Related papers

On Security Models and Compilers for Group Key Exchange Protocols.

Emmanuel Bresson, Mark Manulis, Jörg Schwenk

Abstract. Group key exchange (GKE) protocols can be used to guarantee confidentiality and group authentication formalization (security model) that considers the environment of the protocol and identifies its security goals. The first security model for GKE protocols was proposed by Bresson, Chevassut, Pointcheval, and Quisquater in 2001, and has been subsequently applied in many security proofs. Their definitions of AKE- and MA-security became meanwhile standard. In this paper we analyze the BCPQ model and some of its later appeared modifications and identify several security risks resulting from the technical construction of this model – the notion of partnering. Consequently, we propose a revised model with extended definitions for AKE- and MA-security capturing, in addition, attacks of malicious protocol participants. Further, we analyze some well-known generic solutions (compilers) for AKE- and MA-security of GKE protocols proposed based on the definitions of the BCPQ model and its variants and identify several limitations resulting from the underlying assumptions. In order to remove these limitations and at the same time to show that our revised security model is in fact practical enough for the construction of reductionist security proofs we describe a modified compiler which provides AKE- and MA-security for any GKE protocol, under standard cryptographic assumptions. Key words: Group key exchange, extended security model, malicious participants, compiler for AKE- and

Open Research (University of Surrey)Jan 1, 20060 citations

Modeling insider attacks on group key-exchange protocols

Jonathan I. Katz, Ji Sun Shin

Protocols for authenticated key exchange (AKE) allow parties within an insecure network to establish a common session key which can then be used to secure their future communication. It is fair to say that group AKE is currently less well understood than the case of two-party AKE; in particular, attacks by malicious insiders --- a concern specific to the group setting --- have so far been considered only in a relatively "ad-hoc" fashion. The main contribution of this work is to address this deficiency by providing a formal, comprehensive model and definition of security for group AKE which automatically encompasses insider attacks. We do so by defining an appropriate ideal functionality for group AKE within the universal composability (UC) framework. As a side benefit, any protocol secure with respect to our definition is secure even when run concurrently with other protocols, and the key generated by any such protocol may be used securely in any subsequent application.In addition to proposing this definition, we show that the resulting notion of security is strictly stronger than the one proposed by Bresson, et al. (termed "AKE-security"), and that our definition implies all previously-suggested notions of security against insider attacks. We also show a simple technique for converting any AKE-secure protocol into one secure with respect to our definition.

ACM SIGSAC Conference on Computer and Communications Security (CCS)Nov 7, 2005184 citations

Stronger Security of Authenticated Key Exchange

Brian A. LaMacchia, Kristin Lauter, Anton Mityagin

Recent work by Krawczyk [10] and Menezes [14] has highlighted the importance of under-standing well the guarantees and limitations of formal security models when using them to prove the security of protocols. In this paper we focus on security models for authenticated key exchange (AKE) protocols. We observe that there are several classes of attacks on AKE protocols that lie outside the scope of the Canetti-Krawczyk model. Some of these additional attacks have already been considered by Krawczyk [10]. In an attempt to bring these attacks within the scope of the security model we extend the Canetti-Krawczyk model for AKE security by providing significantly greater powers to the adversary. Our contribution is a more compact, integrated, and comprehensive formulation of the security model. We then introduce a new AKE protocol called NAXOS and prove that it is secure against these stronger adversaries. 1

Jan 1, 20065 citations

Provably authenticated group Diffie-Hellman key exchange

Emmanuel Bresson, Olivier Chevassut, David Pointcheval +1 more

Group Diffie-Hellman protocols for Authenticated Key Exchange (AKE) are designed to provide a pool of players with a shared secret key which may later be used, for example, to achieve multicast message integrity. Over the years, several schemes have been offered. However, no formal treatment for this cryptographic problem has ever been suggested. In this paper, we present a security model for this problem and use it to precisely define AKE (with "implicit" authentication) as the fundamental goal, and the entity-authentication goal as well. We then define in this model the execution of an authenticated group Diffie-Hellman scheme and prove its security.

ACM SIGSAC Conference on Computer and Communications Security (CCS)Jan 1, 200148 citations

Provably authenticated group Diffie-Hellman key exchange

Emmanuel Bresson, Olivier Chevassut, David Pointcheval +1 more

ACM SIGSAC Conference on Computer and Communications Security (CCS)Nov 5, 2001372 citations

A Formal Treatment of the Limits of Authenticated Key Exchange Security

Michèle Feltz, Cas J. F. Cremers

Authenticated Key Exchange (AKE) protocols are a core building block of all modern communications, connecting the distribution benefits of public-key cryptography to the performance benefits of symmetric-key cryptography. Modern AKE protocols are proven secure in game-based security models that offer considerably more security guarantees than the seminal Bellare-Rogaway model from 1993, in order to capture real-world security properties such as various notions of forward secrecy and resistance against predictable or bad pseudorandom number generators. For most of these security models, it is claimed that they offer “the best possible security”, based on informal arguments that at best hold under unstated assumptions. This has led to a fragmented landscape of AKE security models with seemingly contradictory results.We provide the first systematization of the limits of game-based security models for two-party AKE protocols. Our treatment covers classical stateless protocols as well as a restricted class of modern stateful protocols. Our analysis uncovers how the details of the considered protocol class have crucial implications for (im)possibility results, and reveals how different security goals can be achieved in different relevant classes of AKE protocols. From our formal impossibility results, we derive strong security models for these classes and give protocols that satisfy them.

Jan 1, 20260 citations