The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol’s desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol’s roles are run in parallel with the adversary.
In addition to trace properties, Tamarin can express observational equivalence properties. Such properties express that an adversary cannot distinguish two systems and are especially useful for modeling privacy.
In this talk, we present an introduction to the Tamarin tool and explain how a protocol specified in traditional Alice&Bob notation can be translated to the Tamarin protocol model. Furthermore, we explain on the example of a simplified e-voting protocol how properties such as privacy and receipt-freeness can be modeled with Tamarin’s built in observational equivalence theory.
Lara Schmid is a PhD student with Prof. David Basin at the Institute of Information Security at ETH Zurich. She received a Master’s degree in Computer Science from ETH Zurich in 2015. In her Master’s thesis she proposed a model for formalizing and reasoning about erroneous human agents in security protocols. She is interested in formal methods for analyzing security protocols. At the moment, her focus is on formally modeling e-voting protocols.
The SRM seminars are the joint seminars of the Security and Trust of Software Systems and Applied Security and Information Assurance research groups, supported by the Laboratory of Algorithmics, Cryptology and Security and the Interdisciplinary Centre for Security, Reliability and Trust.