Formal Verification with the Tamarin Prover
Current Members
Past Members
- external page Prof. Cas Cremers
- external page Dr. Jannik Dreier
- external page Dr. Luca Hirschi
- Dr. Dennis Jackson
- Prof. Sasa Radomirovic
- external page Dr. Jorge Toro
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 page here.