Formal Verification of Authenticated Encryption with Associated Data with Tamarin Prover

Tamarin Prover and ProVerif are automated tools for formally verifying the security of cryptographic protocols. Tamarin Prover is a type of theorem prover, whereas ProVerif is a type of symbolic model checker. In this paper, we formalized the structure of authenticated encryption with associated data (AEAD). To do so, we formalized AEAD as two types of generic compositions, using the Encrypt-then-Message Authentication Code (MAC) and MAC-then-Encrypt constructions presented by Rogaway et al. Using Tamarin Prover, we verified the confidentiality and integrity independent of considering the attacker's capabilities. We demonstrated that the attacker's abilities can be modeled in ProVerif, and we compared our findings with results obtained via ProVerif. We found that ProVerif is superior to Tamarin Prover in the studied scenarios, although future work is needed to consider attacker's abilities.