Teaching Materials for the Tamarin Prover

This repository contains teaching materials related to the Tamarin Prover. These materials complement the official Tamarin manual.

General support

Understanding dependency graphs (handout)

The following PDF can be used as a reference handout for understanding dependency graphs.

• Handout: dependency graphs

(Update coming with more explanation of specific adversary nodes)

Tutorials

The core Tamarin team and other contributors have developed different tutorials over time. Below you can find four tutorials.

1. One-day tutorial

(Originally given at EuroSnP/Eurocrypt 2017)

• Morning slides PDF (Libreoffice source file)

• Afternoon slides PDF (Libreoffice source file)

• Tamarin model files (ZIP archive version)

• Handouts to print:

  • Exercises
  • Naxos protocol description
  • Dependency graphs

Authors: David Basin, Cas Cremers, Jannik Dreier, and Ralf Sasse.

2. Toy protocol exercise

• Tamarin toy protocol exercise.

Author: Benjamin Kiesl

3. Tamarin workshop

• Tamarin workshop (2-4 hours).

Author: Felix Linker

4. One-day Tamarin workshop

• Tamarin workshop given at Croatia Summer School on real-world crypto and privacy 2024.

Authors: Alexander Dax, Sofia Giampietro, Xenia Hofmeier, Niklas Medinger, and Aurora Naska

License

All the materials in the tamarin-prover/teaching repository are provided under a Creative Commons Attribution license (CC-BY).