SoftwareApplication
identifier: 10.3233/JCS-210053
name: Tamarin Prover
description: The Tamarin Prover is a state-of-the-art tool for the analysis of security protocols, which underpin the security of modern distributed computing.
description: The **Tamarin Prover** is a state-of-the-art scientific security protocol analysis tool that addresses critical challenges in cryptographic verification. Security protocols allow citizens across the globe to work, purchase, and communicate securely every day. Examples include web browsing using TLS, WiFi security, or electronic payments by ATMs and stores, and their security is therefore critical for society. The Tamarin Prover can automatically construct proofs that a protocol is secure, or find counterexamples (attacks) against a wide range of threat models, and has an extensive graphical user interface for complex protocols. Tamarin's target group is global: it includes the academic security research community as well as security researchers in government and industry. Research on Tamarin has substantially advanced the state-of-the-art and enabled new levels of scale and precision in computer-aided protocol analysis. Tamarin is considered the state-of-the-art scientific tool in its domain, and is currently the most-used tool in protocol security research papers at the top (A\*) security conferences. Tamarin's scientific value has led to a wide spectrum of applications to large-scale, real-world protocols, such as TLS 1.3, 5G, Apple iMessage, and EMV, and has attracted a global user base. Its world-wide user community includes researchers and industry practitioners that use it to analyze their protocols or build on its results. In industry, many companies are directly using Tamarin for protocols they are developing or standardizing, e.g., at Apple, Amazon, Cisco, Cloudﬂare, Intel, Mozilla, and Ericsson. In 2026, the Tamarin team was awarded the IACR Levchin Prize for Real-World Cryptography (https://rwc.iacr.org/LevchinPrize/winners.html#Tamarin) at the 2026 Real-World Crypto conference in Taipei. ![Visual representation of an attack found on the current protocol model.](https://hifis.net/assets/img/spotlights/tamarin/attack.png)Visual representation of an attack …
code repository: https://github.com/tamarin-prover/tamarin-prover
author: https://orcid.org/0000-0003-0322-2293
keywords: Cryptographic Protocols
keywords: Information
keywords: Formal Verification
programming language: Haskell
programming language: Python
programming language: JavaScript
programming language: TypeScript
programming language: Makefile
programming language: CSS
programming language: HTML
programming language: Vim Script
programming language: TeX
programming language: Shell
programming language: Dockerfile
programming language: C
programming language: Emacs Lisp
programming language: Tree-sitter Query
license:
  creative work: creativeWork
    name: GPL-3.0-only
reference publication: 978-3-031-90936-8

https://orcid.org/0000-0003-0322-2293
type: Person
given name: Cas
family name: Cremers
name: Cas Cremers
role name: Core developer / Project leader
affiliation: Organization
  name: CISPA Helmholtz Center for Information Security

978-3-031-90936-8
type: ScholarlyArticle
name: Modeling and Analyzing Security Protocols with Tamarin
url: https://doi.org/10.1007%2F978-3-031-90936-8