TYPE
Live Demo / Give-away
TOPIC
Tamarin Prover, Transport Layer Security, Formal Verification
YEAR
2023
SOFTWARE
Figma, Adobe Illustrator
HARDWARE
Lasercutter
SKILLS
Prototyping, Game Design, Visual Design, Product Design, Material Research
Tamarin DominoES
Developed in June 2023, "Tamarin Dominoes" is a tile-based game that illustrates a search for a security vulnerability in an internet protocol. It is suitable for children aged seven and above.
TYPE
Live Demo / Give-away
TOPIC
Tamarin Prover, Transport Layer Security, Formal Verification
YEAR
2023
SOFTWARE
Figma, Adobe Illustrator
HARDWARE
Lasercutter
SKILLS
Prototyping, Game Design, Visual Design, Product Design, Material Research
Security protocols are at work everywhere nowadays. They enable carefree online shopping as well as cashless payment at the supermarket checkout. This of course requires that the protocols themselves are free from security vulnerabilities. Researchers make sure of this by checking the protocols with special computer programs. One of these programs is the so-called Tamarin Prover. The CISPA Helmholtz Center for Information Security contributes to this software.
In 2023, the developers at Product Labs (formerly Scientific Engineering) redesigned parts of the graphical user interface of the Tamarin Prover. Among other things, it displays the communication exchanges of an internet protocol as a graph. In these graphs, every single communication step is displayed as a box. These boxes are subdivided into several areas containing information and as such, they already resemble a domino tile. Only communication steps sharing the same information are connected to each other. The Tamarin Prover checks these information flows when searching for a vulnerability. It seemed logical, thus, to depict the software's approach as a game of dominoes.
Tamarin Dominoes visualizes the search strategy: All possible combinations of the previously specified communication steps are checked for whether they can be traced back to an attacker and enable an attack.
©Yushun Zhao
Mission accomplished: The domino tiles are laid out on the tabletop, forming a pathway to the attacker.
The domino set consists of seven tiles. The players takes the start and finish tiles and tries to complete the path between them using the remaining tiles. Ends bearing identical symbols must be placed next to each other.
Metaphors often only change the level of abstraction. The Tamarin Dominoes game is different: Not only does it illustrate the search for a security vulnerability in a protocol but also invites players to engage, ponder, and puzzle. What's more, a sense of achievement is only ever a few tiles away.
Security protocols like TLS 1.3, EMV, and IEEE 802.11 WPA 2 are more than just random letters and numbers. They represent rules ensuring that data can be sent and received securely in a computer network without being spied on, manipulated, or deleted. TLS 1.3 ensures secure internet communication, EMV secures the connection between your bank card and the supermarket checkout, and IEEE 802.11 WPA 2 aims to protect Wi-Fi networks.
These are not the only security protocols at work in our daily lives. They all act as guardians of our digital world, ensuring that our information remains safe and protected.
In their 2023 scrollytelling "Deceptive Security", the Product Labs department (formerly Scientific Engineering) details how Professor Cas Cremers and three PhD students used the Tamarin Prover to uncover a complex security flaw in the internet standard TLS 1.3.
