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.
Informationen für Demonstrator-Pilotinnen und -Piloten
Erklärung für Kinder?
Wie läuft die Demonstration ab?
Was macht diesen Demonstrator besonders?
Warum wird die Sicherheit von Internet-Protokollen erforscht?
Wer forscht dazu am CISPA?
Weitere Informationen?
Making-of des Domino-Legespiels
Hintergrund
Konzept
Prototyping
So genannte 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 so genannte Tamarin Prover . An dieser Software forscht auch das CISPA Helmholtz-Zentrum für Informationssicherheit.
Im Jahr 2023 haben die Entwickler 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.
Stellt euch vor, eure Schwester hat etwas, eine Art Geheimnis auf den Boden gelegt, und mit Dominosteinen verbunden. Diese Steine sind wie Wege oder Pfade zu ihrem Geheimnis. Aber hier ist die Herausforderung: Jeder Stein muss zu seinem Vorgänger und zu seinem Nachfolger passen, wie Puzzleteile.
Und jetzt kommt's: Eure Schwester hat die Wege zerstört, indem sie die Steine durcheinander geworfen hat. Aber hey, ihr habt einige Steine gefunden! Jetzt ist es an euch, die Steine so anzuordnen, dass sie wieder zusammenpassen und zum Geheimnis führen.
Es ist ein bisschen wie bei einem Puzzle: Ihr müsst die richtigen Teile finden und sie dann richtig zusammensetzen. Wenn ihr es schaffst, die Steine wieder richtig zusammenzusetzen, könnt ihr das Geheimnis eurer Schwester entdecken und sie wird sicher beeindruckt sein, wie schlau ihr seid!
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.
Die von Professor Cas Cremers am CISPA mitentwickelte Software , der Tamarin Prover, ermöglicht die formale Verifikation von Sicherheitsprotokollen. Am CISPA arbeiten nicht nur Professor Cremers mit Formaler Verifikation, sondern auch Rayana Dimitrova, Pryianka Golia, Swen Jakobs und Professor Bernd Finkbeiner. Da formale Verifikation inzwischen als fester Bestandteil des Software Engineering gesehen wird, kann auch Professor Andreas Zeller zu fomaler Verifikation Auskunft geben.
In dem Scrollytelling „ Trügerische Sicherheit “ hat 2023 die Abteilung „Scientific Engineering“, inzwischen „Product Labs“, aufgearbeitet, wie Professor Cas Cremers und drei Promotionsstudierende zusammen mit dem Tamarin Prover eine komplexe Sicherheitslücke im Internetstandard TLS 1.3 entdeckten. Das Scrollytelling findet ihr unter dem folgenden Link: https://tamarin-tls.cispa.de .
Der Tamarin-Prover ist ein Werkzeug zur Modellierung und Analyse von Sicherheitsprotokollen. Im Tamarin-Prover-Modell wird jeder Protokollschritt dargestellt.
Jedes Kästchen beschreibt einen Protokollschritt und besteht im Regelfall aus drei Reihen. In der ersten Reihe befindet sich ein oder mehrere Primitive. Die zweite Reihe beschreibt eine oder mehrere Aktionen, und in der dritten Reihe stehen eine oder mehrere Konklusionen. Die Primitive eines Kästchens werden aus der Konklusion eines anderen Kästchens abgeleitet oder sind im Modell festgeschrieben.
Man kann jeden Protokollschritt mit einem Domino-Spielstein vergleichen. Spielsteine mit dem gleichen Inhalt können miteinander verknüpft werden.
Ein Protokoll besteht aus vielen Schritten. Der Tamarin Prover versucht, die Protokollschritte zu einem Pfad zu verknüpfen. Findet die Software einen Pfad vom Start bis zum Angriff, kann man an geheime Informationen gelangen.
Formsprache des Spielsteins
Basierend auf der Skizze des Dominospielsteins wurden vier mögliche Formen gestaltet. Die erste wurde ausgewählt, da sie viele Möglichkeiten bietet, den Inhalt zu platzieren. Zudem sind Input-Teil und Output-Teil einfach zu unterscheiden.
Visuelle Elemente
Es wurden verschieden Farben ausgewählt und Muster entworfen, mit denen der Input und Output dargestellt werden kann.
Letzten Endes wurde sich dazu entschieden, statt abstrakter Muster und unterschiedlicher Farben sinnvolle Symbole zu verwenden, um Primitive und Konklusionen darzustellen.
Mögliche Spielmechaniken
Eine mögliche Spielmechanik entspricht den Standardregeln des Domino-Spiels. Eine andere Spielmechanik ist das Puzzle. Der Tamarin-Dominostein stellt nun ein Stück des Puzzles dar, hat aber das Potenzial, sich zu einem vollständigen Spiel weiterzuentwickeln.
Materialien und Techniken
Farbdruck und Gravur wurden auf verschiedenen Materialien wie Papier, Finnpappe und Holz ausprobiert.
Die Mock-ups zeigten, dass der Farbdruck auf Holz zwar schön, aber sehr aufwendig ist und handwerkliche Präzision erfordert. Die Gravur ist im Vergleich dazu viel effizienter. Außerdem ist das Holz ein warmes und elegantes Material.
Mit Holz wurden weitere Experimente durchgeführt. Dabei wurden verschiedene Holzarten verwendet und die Gravur sowohl mit als auch entgegen der Faser ausgerichtet. Auch Schliff und Oberflächenbehandlung (Öl und Beize) wurden in die Experimente einbezogen.
Der Lasercutter in unserer Werkstatt wurde für die Gravur verwendet.
Endprodukt
Hier ist das Endprodukt. Der Dominostein wird unter anderem auch als Geschenk für Gäste ausgegeben.
