Paper 2011/460

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

Zijian Zhang, Liehuang Zhu, and 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.

Note: Submitted to Elsevier.

Available format(s)
Publication info
Published elsewhere. Unknown where it was published
Universally Composable Symbolic AnalysisComputational SoundnessBilinear PairingsGroup Key Exchange ProtocolForward Secrecy.
Contact author(s)
zhangzijian @ bit edu cn
2011-10-10: last of 7 revisions
2011-08-29: received
See all versions
Short URL
Creative Commons Attribution


      author = {Zijian Zhang and Liehuang Zhu and Lejian Liao},
      title = {Computationally Sound Symbolic Security Reduction Analysis of Group Key Exchange Protocol using Bilinear Pairings},
      howpublished = {Cryptology ePrint Archive, Paper 2011/460},
      year = {2011},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.