Logo Tamarin
Our digital lives are governed by a wide range of IT protocols used to protect the exchange of data, such as the EMV (Europay Mastercard Visa) standard for debit & credit card transactions or the TLS (Transport Layer Security) protocol, which protects internet connections. Jannik Dreier, an associate professor at Telecom Nancy and the University of Lorraine, and a member of PESTO, a joint Inria-LORIA project team, has sought to identify vulnerabilities with these protocols. His ally in navigating these cryptographic labyrinths is a software program called Tamarin.
Moving faster and making fewer errors
In 2021, researchers from ETH Zurich (Eidgenössische Technische Hochschule Zürich, the Swiss Federal Institute of Technology), identified a vulnerability in the EMV network, the international standard for debit & credit card transactions. A weakness in this vast protocol was enabling attacks on payment terminals, making them believe that there was no limit on contactless payments with debit & credit cards. This vulnerability was discovered using Tamarin, a program first developed in 2012 by scientists from ETH Zurich, the CISPA (Center for IT-Security, Privacy and Accountability) in Saarbrucken, the University of Oxford and the University of Lorraine. Jannik Dreier is part of the team of developers responsible for maintenance of this open-source software.
“There is a constantly growing demand for protocol analysis, particularly during periods of standardisation, as we saw recently with the 5G protocol. The purpose of Tamarin, or ProVerif, another program developed by Inria, is to make fewer errors.” In order to find errors, specialists in the formal verification of cryptographic protocols such as Jannik Dreier analyse specification documents (technical documents used by developers before producing code) and then create mathematical models for assessing the security of protocols in the presence of an attacker: what would happen if…?, etc. “This involves a lengthy process of analysis, which used to be done entirely ‘by hand’”, explains the researcher.
Automating verification and making it accessible
Tamarin was launched in 2012 in response to a need for a tool for automating the analysis of these mathematical. As Jannik Dreier explains: “Tamarin’s originality lies in its capacity to handle highly accurate models of the cryptography of protocols and their weaknesses. The program helps you not only to identify vulnerabilities, but also to then make the right choices when it comes to correcting protocols. These different choices can be tested, without increasing working time costs, unlike with entirely manual analysis.”
The software is now used by the scientific community and a growing number of industrial partners. “Constant improvements have been made to it since 2012, drawing on a wide community of users, the aim being to make it more automatic and easier to use for non-experts. This is very pleasing for us”, says Jannik Dreier, who has participated in this project team for a number of years. Tamarin is leaving the academic world and is continuing to identify security breaches. It was recently used to identify a breach in the 5G protocol.
[more info]Presentation of Tamarin : Read the paper in HAL
