Tamarin Prover

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, Cloudflare, 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.

Scientific and Societal Impact

Examples of Tamarin's impact on real-world security include:

• TLS 1.3 (RFC 8446): Tamarin-based analysis of early drafts identified a concrete man-in-the-middle attack in draft-10 of TLS 1.3. The IETF TLS Working Group updated the specification based on this report. Prof. Cremers is listed as a contributor in the final RFC 8446, now the web's dominant transport security protocol with ~97% global browser support.
• 5G-AKA: Tamarin analysis of the 3GPP 5G authentication standard revealed that critical security goals were not met except under unstated assumptions, leading to fixes adopted by 3GPP. A separate Tamarin-based analysis identified a security-critical race condition that providers could trigger by "correctly" implementing the standard.
• Apple iMessage PQ3: Apple's official security documentation for its post-quantum upgrade explicitly states that formal methods using Tamarin were employed to evaluate the design and obtain machine-checked proofs, a publicly documented case of industrial adoption at billion-user scale (iMessage serves over one billion Apple devices).
• EMV Contactless Payments (IEEE S&P 2021): Tamarin analysis of the global EMV chip-and-pin standard (present in virtually every bank card) uncovered a live PIN-bypass attack: a fraudulent Visa contactless transaction could succeed without PIN verification, regardless of the transaction amount. The attack was validated on real card terminals. Tamarin was then used to design and formally verify a corrective fix, making this a complete break-fix-verify cycle with direct relevance to billions of payment cards and contactless readers worldwide.
• SPDM 1.2 (CCS 2025): The most recent Tamarin analysis exposed cross-protocol attacks in the SPDM hardware-attestation standard (DMTF), with fixes already proposed and validated, extending Tamarin's reach to hardware-layer security infrastructure.
• Noise / WireGuard (USENIX Security 2020): A comprehensive Tamarin analysis formally verified the security of the entire Noise protocol framework, which underlies WireGuard, now built into the Linux kernel and deployed in millions of commercial and consumer VPN products.

Recognition

• 2026 Levchin Prize for Real-World Cryptography, awarded to the Tamarin Prover at Real World Crypto, for its innovations with demonstrated impact on the practice of cryptography in deployed systems
• ACM CCS Distinguished Paper Award (2025) and Distinguished Artifact Award (2024)
• USENIX Security Distinguished Paper Award (2023)
• Oxford MPLS Impact Award (TLS line of work)
• Over 3,000 Google Scholar citations across eight core Tamarin papers (CAV 2013: 1,105; CCS 2018 5G: 628; CCS 2017 TLS 1.3: 411; CSF 2012 theory: 402; further application and extension papers)
• 78 contributors across 10 versioned releases spanning 2012 to 2026; 515 GitHub stars; commits as recent as March 2026

FAIR Compliance and Sustainability

Tamarin is open source (GNU General Public License), version-controlled on GitHub with GitHub Actions CI/CD pipelines and an automated regression test suite. A CITATION.cff file with full author ORCIDs is present in the repository. Each of the 10 tagged releases has its own individual Zenodo DOI; a concept DOI (10.5281/zenodo.13971810) resolves to the latest version and supports stable long-term citation. The tool is installable via Homebrew and Docker, and is registered in the Helmholtz Research Software Directory. Extensive documentation, tutorials, and an active mailing list ensure broad accessibility and long-term maintainability. The latest commit is from March 2026, confirming active development over 12+ consecutive years.

Community metrics (GitHub, April 2026): 515 stars · 162 forks · 78 contributors · 10 versioned releases