Tamarin: Symbolic protocol verification with multiset rewriting
===============================================================

Tamarin is the most widely used symbolic protocol verifier for stateful, multi-role protocols. It has analysed TLS 1.3, 5G authentication, WPA2, the Noise framework and EMV, and supports interactive guidance when automation stalls.

Maintainer: ETH Zürich, CISPA, University of Oxford
Website: https://tamarin-prover.com
Category: Symbolic protocol analysis
Targets: TLS 1.3, 5G AKA, WPA2, Noise, EMV, Messaging protocols
Approach: Symbolic (Dolev-Yao) analysis over unbounded sessions with user-guided lemmas
Access: Open source
Status: Active, mature
Strengths: Most expressive of the automatic symbolic tools. | Interactive mode for hard proofs. | Largest record of real protocol findings.
Limits: Modelling skill required; non-termination is possible. | Symbolic abstraction misses cryptographic weaknesses. | No code connection.
Firms using it: Symbolic Software
Sources: https://tamarin-prover.com

Source page: https://sorryfree.com/frameworks/tamarin/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13