Analyzing cryptographic protocols with Tamarin

Abstract

The Tamarin prover is an automated tool for symbolic verification of security protocols. This talk, based on a lecture series by David Basin at Marktoberdorf 2025, gives an overview of Tamarin, covering its usage and theoretical foundations. As an application, we’ll cover how Tamarin was used to find (and fix) vulnerabilities in EMV, the international standard protocol for smart-card payments.