Automated Verification of Group Key Agreement Protocols

Abstract—We advance the state-of-the-art in automated sym-bolic cryptographic protocol analysis by providing the first algorithm that can handle Diffie-Hellman exponentiation, bilin-ear pairing, and AC-operators. Our support for AC-operators enables protocol specifications to use multisets, natural numbers, and finite maps. We implement the algorithm in the TAMARIN prover and provide the first symbolic correctness proofs for group key agreement protocols that use Diffie-Hellman or bilinear pairing, loops, and recursion, while at the same time supporting advanced security properties, such as perfect forward secrecy and eCK-security. We automatically verify a set of protocols, including the STR, group Joux, and GDH protocols, thereby demonstrating the effectiveness of our approach. I