Formal Verification with the Tamarin Prover

Introduction

The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification in the symbolic model. Security protocols are specified as multiset rewriting systems and analysed with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined subterm-convergent rewriting theory.

Objectives

Tamarin was initially developed at the Information Security group at ETH Zurich and evolved into a collaborative effort. Our group's current research focus is twofold:

• we develop foundations for new verifications techniques that benefit Tamarin by extending its scope: e.g., verification of observational equivalence, dealing with more equational theories, etc.
• using Tamarin, we formally model real-life security protocols (5G, ISO/IEC 9798, EMV, etc.) and formally prove high-assurance guarantees of correctness, or expose attacks.

Publications

A full list of publications is available external pageherecall_made.