ART
Live Demo / Give-away
THEMA
Tamarin Prover, Transport Layer Security, Formal Verification
JAHR
2023
SOFTWARE
Figma, Adobe Illustrator
HARDWARE
Lasercutter
SKILLS
Prototyping, Game Design, Visual Design, Produkt Design, Materialrecherche
Tamarin Domino
Das im Juni 2023 entwickelte Spiel „Tamarin Domino“ stellt die Suche nach einer Sicherheitslücke in einem Internet-Protokoll als Domino-Legespiel dar. Es eignet sich für Kinder ab sieben Jahren.
ART
Live Demo / Give-away
THEMA
Tamarin Prover, Transport Layer Security, Formal Verification
JAHR
2023
SOFTWARE
Figma, Adobe Illustrator
HARDWARE
Lasercutter
SKILLS
Prototyping, Game Design, Visual Design, Produkt Design, Materialrecherche
Sogenannte Sicherheitsprotokolle arbeiten heute überall für uns. Sie ermöglichen das sorglose Einkaufen im Internet ebenso wie das bargeldlose Bezahlen an der Supermarktkasse. Voraussetzung ist, dass die Protokolle selbst keine Sicherheitslücken aufweisen. Forschende stellen dies sicher, indem sie die Protokolle mit speziellen Computerprogrammen überprüfen. Eines dieser Programme ist der sogenannte Tamarin Prover. An dieser Software forscht auch das CISPA Helmholtz-Zentrum für Informationssicherheit.
Im Jahr 2023 haben die Entwickler:innen der Abteilung, die damals noch „Scientific Engineering“ hieß, Teile der grafischen Benutzeroberfläche des „Tamarin Prover“ überarbeitet. Sie stellt unter anderem die Kommunikationsschritte des jeweiligen Protokolls Schritt für Schritt als „Graph“ dar. Ein einzelner Kommunikationsschritt wird in diesem Graphen als Kasten angezeigt. Er ist in mehrere Bereiche unterteilt, die Informationen enthalten, und ähnelt damit schon einem Dominostein. Da nur Kommunikationsschritte mit miteinander verbunden sind, die über gleiche Informationen verfügen, und der Tamarin Prover während seiner Suche nach einer Sicherheitslücke diese Informationsflüsse überprüft, lag es nahe, die Vorgehensweise der Software als Domino-Legespiel greifbar zu machen.
Das Domino-Legespiel veranschaulicht somit die Suchstrategie: Für alle möglichen Kombinationen der zuvor spezifizierten Kommunikationsschritte ist zu prüfen, ob sie zu einem Angreifer zurückverfolgt werden können und einen Angriff ermöglichen.
©Yushun Zhao
Mission erfüllt: Die Spielsteine liegen auf der Tischplatte und bilden einen Pfad zum Angreifer.
Das gesamte Domino besteht aus sieben Plättchen. Der Spieler nimmt das Start- und das Zielplättchen und versucht, den Weg zwischen Start und Ziel zu vervollständigen. Dabei müssen gleiche Symbole an den Rändern aneinandergelegt werden.
Metaphern ändern oft nur den Abstraktionsgrad. Das hier beschriebene Tamarin Domino ist anders: Es veranschaulicht nicht nur die Suche nach einer Sicherheitslücke in einem Protokoll, sondern lädt auf niederschwellige Weise zum Machen, Knobeln, Puzzeln ein. Mehr noch: Das Erfolgserlebnis ist nur wenige Spielsteine entfernt.
Sicherheitsprotokolle wie TLS 1.3, EMV und IEEE 802.11 WPA 2 sind mehr als bloße Buchstaben und Zahlen. Sie repräsentieren Regelwerke, die dafür sorgen, dass Daten in einem Computernetzwerk sicher gesendet und empfangen werden können, ohne dass sie ausspioniert, manipuliert oder gelöscht werden. TLS 1.3 gewährleistet eine sichere Internetkommunikation, EMV sichert die die Verbindung zwischen Eurer Geldkarte und der Supermarktkasse ab und IEEE 802.11 WPA 2 soll jedes WLAN schützen. Sie sind nicht die einzigen Sicherheitsprotokolle, die in unseren Alltag unsichtbar wirken. Sie alle sind die Hüter unserer digitalen Welt und sorgen dafür, dass unsere Informationen sicher und geschützt bleiben.
In dem Scrollytelling „Trügerische Sicherheit“ hat die Abteilung „Product Labs“ aufgearbeitet, wie CISPA-Faculty Cas Cremers und drei Promotionsstudierende zusammen mit dem Tamarin Prover eine komplexe Sicherheitslücke im Internetstandard TLS 1.3 entdeckten.
