Computationally sound symbolic security reduction analysis of the group key exchange protocols using bilinear pairings

The security of the group key exchange protocols has been widely studied in the cryptographic community in recent years. Current work usually applies either the computational approach or the symbolic approach for security analysis. The symbolic approach is more efficient than the computational approach, because it can be easily automated. However, compared with the computational approach, it has to overcome three challenges: (1) The computational soundness is unclear; (2) the number of participants must be fixed; and (3) the advantage of efficiency disappears, if the number of participants is large. This paper proposes a computationally sound symbolic security reduction approach to resolve these three issues. On one hand, combined with the properties of the bilinear pairings, the universally composable symbolic analysis (UCSA) approach is extended from the two-party protocols to the group key exchange protocols. Meanwhile, the computational soundness of the symbolic approach is guaranteed. On the other hand, for the group key exchange protocols which satisfy the syntax of the simple protocols proposed in this paper, the security is proved to be unrelated with the number of participants. As a result, the symbolic approach just needs to deal with the protocols among three participants. This makes the symbolic approach has the ability to handle arbitrary number of participants. Therefore, the advantage of efficiency is still guaranteed. The proposed approach can also be applied to other types of cryptographic primitives besides bilinear pairing for computationally sound and efficient symbolic analysis of group key exchange protocols.