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

Information Sciences

Computationally sound symbolic security reduction analysis of the group key exchange protocols using bilinear pairings

Zijian Zhang, Liehuang Zhu, Lejian Liao, Mingzhong Wang

Published May 6, 2012• 11 citations
Publisher
DOI
10.1016/j.ins.2012.04.029

Related papers

Computationally Sound Symbolic Criteria for UC-secure Multi-Party Mutual Authentication and Key Exchange Protocols

Muratani Hirofumi, Yoshikazu Hanatani

IEICE Technical Report; IEICE Tech. Rep.•Mar 9, 2007•1 citation

Design and analysis of one-round certificateless authenticated group key agreement protocol with bilinear pairings.

SK Hafizul Islam, Abhishek Singh

•Jan 1, 2014•0 citations

A new efficient authenticated multiple-key exchange protocol from bilinear pairings

Mohammad Sabzinejad Farash, Mahmoud Ahmadian‐Attari, Reza Ebrahimi Atani +1 more

Computers & Electrical Engineering•Oct 10, 2012•29 citations

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

Computationally Sound and Effective Symbolic Analysis of Group Key Exchange Protocols

Zhang Zi

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.

Chinese Journal of Computers•Jan 1, 2012•1 citation

Cryptanalysis of ID-Based Authenticated Key Agreement Protocols from Bilinear Pairings (Short Paper)

Kyung‐Ah Shim, Seung-Hyun Seo

Lecture notes in computer science•Jan 1, 2006•3 citations
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.
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.