Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols

David Basin (1) , Cas Cremers (2) , Jannik Dreier (3) , Ralf Sasse (1)

1 Institute of Information Security [ETH Zürich]
2 CISPA - Helmholtz Center for Information Security [Saarbrücken]
3 PESTO - Proof techniques for security protocols

Tamarin is a mature, state-of-the-art tool for cryptographic protocol verification. We introduce Tamarin and survey some of the larger, tour-de-force results achieved with it. We also show how Tamarin can formalize a wide range of protocols, adversary models, and properties, and scale to substantial, real-world, verification problems.

Domaines: Cryptographie et sécurité [cs.CR]

David Basin, Cas Cremers, Jannik Dreier, Ralf Sasse. Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols. IEEE Security and Privacy Magazine, In press, ⟨10.1109/msec.2022.3154689⟩. ⟨hal-03586826⟩