Cryptology ePrint Archive: Report 2011/460
Computationally Sound Symbolic Security Reduction Analysis of Group Key Exchange Protocol using Bilinear Pairings
Zijian Zhang and Liehuang Zhu and Lejian Liao
Abstract: 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.
Category / Keywords: Universally Composable Symbolic Analysis, Computational Soundness, Bilinear Pairings, Group Key Exchange Protocol, Forward Secrecy.
Date: received 22 Aug 2011, last revised 10 Oct 2011
Contact author: zhangzijian at bit edu cn
Available formats: PDF | BibTeX Citation
Note: Submitted to Elsevier.
Version: 20111010:165941 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]