Jannik Dreier his team Awarded the 2026 Levchin Prize for Tamarin Prover

 

Warmest congratulations to Jannik Dreier, maître de conférences à l’Université de Lorraine, teacher at Telecom Nancy and researcher at Loria (UMR CNRS – Université de Lorraine) , along with his colleagues: David Basin (ETH Zurich), Cas Cremers (CISPA), and Ralf Sasse (ETH Zurich), recipients of the 2026 Levchin Prize!

The Levchin Prize (“for Real-World Cryptography”) recognizes groundbreaking innovations in cryptography and its application in real-world systems. The award was presented on March 9 at the Real-World Crypto Symposium in Taipei, a leading international conference in applied cryptography that brings together approximately 600 academic and industry professionals annually.

This prestigious award honors the four researchers for their work on the development of Tamarin Prover, a tool for verifying cryptographic protocols, and its application to industrial and real-world cryptographic protocols.

“We are deeply honored to receive this award. At the Real-World Crypto Symposium, many researchers and industry professionals seek and propose solutions to apply cryptography in practice. The Levchin Prize is a recognition that crowns over a decade of development and improvement of the tool, and it highlights the concrete and tangible impact of Tamarin in real life, far beyond fundamental research.”

Scientific Advances for the Security of Cryptographic Protocols

Over the past decade, research on Tamarin Prover has significantly advanced the state of the art in cryptographic protocol verification. It has enabled industrial-scale progress and achieved unprecedented precision in computer-assisted analysis of these protocols.

“The work on Tamarin began with Cas Cremers, David Basin, and two PhD students, Simon Meier and Benedikt Schmidt, later joined by Ralf Sasse and myself. Today, the project has grown significantly, with many contributors, including PhD students and interns from Loria, CISPA, and ETH,” comments Jannik Dreier, a researcher at Loria in the Pesto team (Loria/Inria).

Tamarin offers both automated verification and user-guided proof search, similar to interactive proof assistants. It can be used to discover new attacks, assist in designing improvements, and provide correctness proofs.

“Last year, we also published a book on Tamarin, designed as a practical guide for users. Writing this book took us five years, but we hope it will contribute to the democratization of verification techniques.”

Tamarin has been used to analyze a wide range of protocols, including TLS 1.3, 5G-AKA, EMV, iMessage PQ3, and other industrial standards. The Tamarin tool is open-source, freely accessible, and has a global user base in both academic and industrial sectors. Many companies now use Tamarin directly for the protocols they develop or standardize, such as Apple, Amazon, Cloudflare, Google, Mozilla, Ericsson, Huawei, Dfinity, and SRI.

“Tamarin is not limited to research or industry; it is also used in education to teach students the techniques for verifying and securing protocols. I use Tamarin in my course on cryptographic protocol security at Telecom Nancy. I complement this course with a ‘Protocol Championship,’ an event where students practice developing protocols, analyzing them, and detecting flaws in competing protocols, both manually and using Tamarin.”

Congratulations to the entire team for receiving this award, which celebrates over a decade of research.

For Further Information: