Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Chinese Journal of Computers

Computationally Sound and Effective Symbolic Analysis of Group Key Exchange Protocols

Zhang Zi

Published Jan 1, 2012• 1 citation
OpenAlex

Abstract

The computational soundness of symbolic analysis is always argued,because the cryptographic primitives are viewed as black boxes,and the specific security properties of those cryptographic primitives have not been considered yet.Moreover,this kind of approaches is ineffective,when it is used to analyze group key exchange protocols with a large number of participants.This paper considers those problems above,and proposes computationally sound and effective symbolic analysis of group key exchange protocols.More specifically,we design a pattern function for symbolic expression,so as to define the concrete security properties that modular exponentiation operation needs satisfy.Based on that,we prove the symbolic analysis of Burmester-Desmedt protocol is computationally sound in universally composable security framework.Furthermore,we use mathematical inductive method to prove the security of Burmester-Desmedt protocol is unrelated to the number of participants.The number of the participants does not affect symbolic analysis.As a result,the efficiency of symbolic analysis is improved.

Related papers

Computationally Sound Symbolic Security Reduction Analysis of Group Key Exchange Protocol using Bilinear Pairings.

Zijian Zhang, Liehuang Zhu, Lejian Liao

Canetti and Herzog have proposed a universally composable symbolic analysis (UCSA) of mutual authentication and key exchange protocols within universally composable security framework. It is fully automated and computationally sound symbolic analysis. Furthermore, Canetti and Gajek have analyzed Diffie-Hellman based key exchange protocols as an extension of their work. It deals with forward secrecy in case of fully adaptive party corruptions. However, their work only addresses two-party protocols that use public key encryptions, digital signatures and Diffie-Hellman exchange. We make the following contributions. First, we extend UCSA approach to analyze group key exchange protocols that use bilinear pairings exchange and digital signatures to resist insider attack under fully adaptive party corruptions with respect to forward secrecy. Specifically, we propose an formal algebra, and property of bilinear pairings in the execution of group key exchange protocol among arbitrary number of participants. This provides computationally sound and fully automated analysis. Second, we reduce the security of multiple group key exchange sessions among arbitrary number of participants to the security of a single group key exchange session among three participants. This improves the efficiency of security analysis.

•Jan 1, 2011•0 citations

Key Exchange Protocols: Security Definition, Proof Method and Applications.

Anupam Datta, Ante Đerek, John C. Mitchell +1 more

We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that, unlike conventional key indistinguishability, is closed under general composition with steps that use the key.

•Jan 1, 2006•8 citations

A Modular Approach to the Design and Analysis of Authentication and Key Exchange Protocols.

Mihir Bellare Y, Ran Canetti, Hugo Krawczyk

We present a general framework for constructing and analyzing authentication protocols in realistic models of communication networks. This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols. The key element in our approach is a modular treatment of the authentication problem in cryptographic protocols; this applies to the definition of security, to the design of the protocols, and to their analysis. In particular, following this modular approach, we show how to systematically transform solutions that work in a model of idealized authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary. Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols. In particular, we provide a security analysis of some well-known key exchange protocols (e.g. authenticated Diffie-Hellman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being

•Jan 1, 1998•380 citations

A new hierarchical and scalable group key exchange protocol with XOR operation

Hongyuan Wang, Liehuang Zhu, Zhenghe Yang +1 more

With the rapid development of the technology of group broadcast, distributed computation and wireless network, how to construct a secure Group Key Exchange (GKE) protocol for a number of participants on channels is drawing more and more attention. Meanwhile, security analysis of cryptographic protocol has been a hotspot. Symbolic analysis is a major approach to analyse the security of protocols. In this paper, we propose a GKE protocol originated from a two-participant key exchange protocol and prove that the protocol is secure. We represent the protocol as processes in the spi calculus, and state their security properties as queries in ProVerif, an automatic analyser based on spi calculus.

International Journal of Wireless and Mobile Computing•Jan 1, 2013•0 citations

Scalable Protocols for Authenticated Group Key Exchange.

Jonathan I. Katz, Moti M. Yung

We consider the problem of authenticated group key exchange among n parties communicating over an insecure public network. A number of solutions to this problem have been proposed; however, all prior provably-secure solutions do not scale well and, in particular, require O (n) rounds. Our main contribution is the first scalable protocol for this problem along with a rigorous proof of security in the standard model under the DDH assumption; our protocol uses a constant number of rounds and requires only O (1) \full modular exponentiations per user. Toward this goal (and adapting work of Bellare, Canetti, and Krawczyk), we first present an efficient compiler that transforms any ngroup key-exchange protocol secure against a passive eavesdropper to an authenticated protocol which is secure against an active adversary who controls all communication in the network. This compiler adds only one round and O (1) communication (per user) to the original scheme. We then prove secure | against a passive adversary | a variant of the two-round group key-exchange protocol of Burmester and Desmedt. Applying our compiler to this protocol results in a provably-secure three-round protocol for authenticated group key exchange which also achieves forward secrecy.

•Jan 1, 2003•7 citations

A modular approach to the design and analysis of authentication and key exchange protocols (extended abstract)

Mihir Bellare Y, Ran Canetti, Hugo Krawczyk

We prcscnt a general framework for constructing and analyzing authentication protocols in realistic models of communication networks.This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols.The key element in our appronch io a modular treatment of the authentication problem in cryptographic protocols; thii applies to the definition of accurity, to the design of the protocols, and to their analysis.In particulnr, following this modular approach, we show how to systematically transform solutions that work in a model of idaalizcd authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary.Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols.In particular, we provide a security analysis of aomo well-known key exchange protocols (e.g.authenticated Dlfllc-Hcllman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being deployed on a large scale for the Intornot Protocol and other applications.

ACM Symposium on Theory of Computing (STOC)•Jan 1, 1998•357 citations
The computational soundness of symbolic analysis is always argued,because the cryptographic primitives are viewed as black boxes,and the specific security properties of those cryptographic primitives have not been considered yet.Moreover,this kind of approaches is ineffective,when it is used to analyze group key exchange protocols with a large number of participants.This paper considers those problems above,and proposes computationally sound and effective symbolic analysis of group key exchange protocols.More specifically,we design a pattern function for symbolic expression,so as to define the concrete security properties that modular exponentiation operation needs satisfy.Based on that,we prove the symbolic analysis of Burmester-Desmedt protocol is computationally sound in universally composable security framework.Furthermore,we use mathematical inductive method to prove the security of Burmester-Desmedt protocol is unrelated to the number of participants.The number of the participants does not affect symbolic analysis.As a result,the efficiency of symbolic analysis is improved.
Canetti and Herzog have proposed a universally composable symbolic analysis (UCSA) of mutual authentication and key exchange protocols within universally composable security framework. It is fully automated and computationally sound symbolic analysis. Furthermore, Canetti and Gajek have analyzed Diffie-Hellman based key exchange protocols as an extension of their work. It deals with forward secrecy in case of fully adaptive party corruptions. However, their work only addresses two-party protocols that use public key encryptions, digital signatures and Diffie-Hellman exchange. We make the following contributions. First, we extend UCSA approach to analyze group key exchange protocols that use bilinear pairings exchange and digital signatures to resist insider attack under fully adaptive party corruptions with respect to forward secrecy. Specifically, we propose an formal algebra, and property of bilinear pairings in the execution of group key exchange protocol among arbitrary number of participants. This provides computationally sound and fully automated analysis. Second, we reduce the security of multiple group key exchange sessions among arbitrary number of participants to the security of a single group key exchange session among three participants. This improves the efficiency of security analysis.
We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that, unlike conventional key indistinguishability, is closed under general composition with steps that use the key.
We present a general framework for constructing and analyzing authentication protocols in realistic models of communication networks. This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols. The key element in our approach is a modular treatment of the authentication problem in cryptographic protocols; this applies to the definition of security, to the design of the protocols, and to their analysis. In particular, following this modular approach, we show how to systematically transform solutions that work in a model of idealized authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary. Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols. In particular, we provide a security analysis of some well-known key exchange protocols (e.g. authenticated Diffie-Hellman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being
With the rapid development of the technology of group broadcast, distributed computation and wireless network, how to construct a secure Group Key Exchange (GKE) protocol for a number of participants on channels is drawing more and more attention. Meanwhile, security analysis of cryptographic protocol has been a hotspot. Symbolic analysis is a major approach to analyse the security of protocols. In this paper, we propose a GKE protocol originated from a two-participant key exchange protocol and prove that the protocol is secure. We represent the protocol as processes in the spi calculus, and state their security properties as queries in ProVerif, an automatic analyser based on spi calculus.
We consider the problem of authenticated group key exchange among n parties communicating over an insecure public network. A number of solutions to this problem have been proposed; however, all prior provably-secure solutions do not scale well and, in particular, require O (n) rounds. Our main contribution is the first scalable protocol for this problem along with a rigorous proof of security in the standard model under the DDH assumption; our protocol uses a constant number of rounds and requires only O (1) \full modular exponentiations per user. Toward this goal (and adapting work of Bellare, Canetti, and Krawczyk), we first present an efficient compiler that transforms any ngroup key-exchange protocol secure against a passive eavesdropper to an authenticated protocol which is secure against an active adversary who controls all communication in the network. This compiler adds only one round and O (1) communication (per user) to the original scheme. We then prove secure | against a passive adversary | a variant of the two-round group key-exchange protocol of Burmester and Desmedt. Applying our compiler to this protocol results in a provably-secure three-round protocol for authenticated group key exchange which also achieves forward secrecy.
We prcscnt a general framework for constructing and analyzing authentication protocols in realistic models of communication networks.This framework provides a sound formalization for the authentication problem and suggests simple and attractive design principles for general authentication and key exchange protocols.The key element in our appronch io a modular treatment of the authentication problem in cryptographic protocols; thii applies to the definition of accurity, to the design of the protocols, and to their analysis.In particulnr, following this modular approach, we show how to systematically transform solutions that work in a model of idaalizcd authenticated communications into solutions that are secure in the realistic setting of communication channels controlled by an active adversary.Using these principles we construct and prove the security of simple and practical authentication and key-exchange protocols.In particular, we provide a security analysis of aomo well-known key exchange protocols (e.g.authenticated Dlfllc-Hcllman key exchange), and of some of the techniques underlying the design of several authentication protocols that are currently being deployed on a large scale for the Intornot Protocol and other applications.