Tamarin is an automated verification tool that has been used to analyze group key protocols, public-key infrastructure proposals, and proposed standards, such as TLS. For example, using Tamarin, attacks were found in TLS 1.3 and 5G. Tamarin works in the symbolic model of cryptographic protocols, and enables automatic analysis as well as a powerful interactive mode:

Tamarin supports both falsification and unbounded verification of security protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined convergent rewriting theory.

Tutorial co-located with Eurocrypt 2019

We are holding a tutorial workshop co-located with EuroCrypt in Darmstadt, Germany on Sunday May 19. In this tutorial, we will combine presentation and hands-on exercises to show attendees the basics of security protocol modeling with multiset rewriting, property specification, and analysis. Participants will model classic protocols, find attacks and perform verification, and leave with an understanding how to start modeling their own protocols of interest.

Room

The tutorial will be held in room (t.b.d.).

Registration

Please do not forget to register!

Schedule

The tentative tutorial schedule is:

Prerequisites

We request that you bring a laptop for the hands-on part with Tamarin and its dependencies installed. To do so, follow the instructions in the manual available here: Installation instructions.

We hope to see you all there!

David Basin & Cas Cremers & Jannik Dreier & Ralf Sasse