We advance the state-of-the-art in automated symbolic
cryptographic protocol analysis by providing the first algorithm
that can handle Diffie-Hellman exponentiation, bilinear 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.