Computationally sound and effective symbolic analysis of group key exchange protocols

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.