Automatic Security Analysis For Group Key Exchange Protocol: A Case Study In Burmester-Desmedt Protocol

Canetti and Herzog have already proposed universally composable symbolic analysis (UCSA) for mutual authentication and key exchange protocols automatically without sacrificing the soundness of the cryptography. We want to extend their work to analyze group key exchange protocols. This paper takes the case of BD protocol with arbitrary participants against passive adversary (BD-Passive), and proves that BD-Passive is a secure group key exchange protocol. More specially, we (1) define the ideal functionality of BD-Passive; (2) prove the security property of BD-Passive in UC security framework by UCSA. Obviously, our work plays a new approach to prove group key exchange protocols automatically without sacrificing the soundness of the cryptography.