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. Using Tamarin, recently attacks were found in TLS 1.3. 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 subterm-convergent rewriting theory.

Tutorial co-located with IEEE EuroSnP and Eurocrypt 2017

We are holding a tutorial between EuroSnP and EuroCrypt in Paris on Saturday, April 29th. 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.

The tentative tutorial schedule is:

Note: lunch is not included, but we will have a list of recommendations nearby.

We hope to see you all there!

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.

David Basin & Cas Cremers & Jannik Dreier & Ralf Sasse