Universally composable symbolic analysis of group key exchange protocol

Canetti and Herzog have already proposed universally composable symbolic analysis (UCSA) to analyze mutual authentication and key exchange protocols. However, they do not analyze group key exchange protocol. Therefore, this paper explores an approach to analyze group key exchange protocols, which realize automation and guarantee the soundness of cryptography. Considered that there exist many kinds of group key exchange protocols and the participants' number of each protocol is arbitrary. So this paper takes the case of Burmester-Desmedt (BD) protocol with three participants against passive adversary (3-BD-Passive). In a nutshell, our works lay the root for analyzing group key exchange protocols automatically without sacrificing soundness of cryptography.