23rd Estonian Winter School in Computer Science (EWSCS)
XXIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 4 - 9, 2018

Jannik Dreier

Université de Lorraine

Symbolic verification of cryptographic protocols using Tamarin


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. Moreover, Tamarin also supports unbounded verification of equivalence properties.

During this introductory course, we will see how to model protocols in Tamarin, how to specify security properties, and how to interpret the results. We will also take a glimpse under the hood to see how one can improve models to help the tool.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 10, 2020 22:34 Europe/Helsinki (GMT +03:00) by local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: //cs.ioc.ee/ewscs/2018/