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.
- J. Dreier. Symbolic verification of cryptographic protocols using Tamarin.
- Exercises [pdf], Tamarin files for the exercises [spthy files]
- Videos from the lectures (large, unedited files) [mp4, password-protected]
- Tamarin manual, incl. precise installation instructions
April 10, 2020 22:34 Europe/Helsinki (GMT +03:00)
local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: //cs.ioc.ee/ewscs/2018/