Das Logo der Tamarin Prover Software. Ein Tamarin-Affe im Pixel-Art-Stil.

Bitte nutze die für Mobilgeräte optimierte Version.

Trügerische Sicherheit

Ein wichtiger Internetstandard wird überarbeitet. Es dürfen keine Fehler passieren.

Cas Cremers sitzt hinter seinem Schreibtisch vor einem PC. Auf dem Schreibtisch sitzt ein Tamarin Plüschtier.
Eine Software, die den Namen einer Affengruppe trägt und das Potenzial hat, die Welt vor Unheil zu bewahren.
Ein Forscher verfolgt seit seiner Dissertation eine Idee und hält daran fest, obwohl seine Kollegschaft sie als Spielerei abtut.
Drei Promovierende und ein Professor, die das Unmögliche wagen, um andere zu schützen.
Und doch geht es in Wahrheit um die Frage, was getan werden kann, was getan werden muss, damit das Fundament des Internets sicher ist und sicher bleibt.
Alle vier Geschichten sind mit einer Person verbunden. Sie lebt seit 2018 in Saarbrücken, forscht und lehrt am CISPA-Helmholtz-Zentrum für Informationssicherheit: Professor Cas Cremers.
Das CISPA Gebäude in Saarbrücken, Deutschland
Casimier Joseph Franciscus Cremers kommt 1974 in den Niederlanden zur Welt. Schon als Kind interessiert er sich für zu viele Dinge. Bis heute rufen ihn die meisten einfach nur Cas.

Mit zehn Jahren sitzt er zum ersten Mal vor einem Computer. Leider steht der Rechner, ein „Philips MSX-2“, bei einem Freund. Da seine Eltern ihm keinen kaufen, leiht er sich in der Stadtbücherei ein Buch über die Programmiersprache „Basic“ aus und verschlingt es. Dann schreibt der öffentlich-rechtliche Rundfunk einen Programmierwettbewerb aus. Der elfjährige Cas löst die Aufgaben mit Bleistift auf Rechenpapier - und gewinnt. Der Hauptpreis ist kein Computer, sondern ein Buch über Kindererziehung. Titel: „Fatherhood“
Zwei Jahre vergehen, dann steht ein Philips MSX-2 endlich auch im elterlichen Haushalt und nur zwei Programmierbücher zu „Z80“ später stellt Cas sein erstes Computerspiel fertig. Ein rotes Raumschiff gleitet durch ein Labyrinth aus Festungsmauern und schießt sich seinen Weg frei. Es befreit die auf dem Planeten Vectron lebenden Menschen, die von den Batman-ähnlichen „Ketaren“ unterdrückt werden. Mit diesem Spiel gewinnt Cas erneut. Diesmal bei einem Spieleprogrammierwettbewerb der niederländischen Ausgabe des „MSX Computer Magazine“. Mit 15 gründet er die Firma „Parallax“, um noch mehr Computerspiele zu entwickeln. Ein Freund steigt mit ein.  Gemeinsam bringen sie sechs Spiele heraus: Weltraumpirat:innen, Zauberer:innen, Roboter. Bei allen davon ist der Designer, Komponist und Autor - Cas.
Nachdem er sein Abitur in der Tasche hat, will Cas weniger programmieren und mehr über die Theorie der Informatik lernen. Er beginnt ein Informatikstudium in Eindhoven. Nach einem weiteren Jahr schreibt er sich auch für Philosophie an der Universität Tilburg ein und gründet eine Internetfirma. Obwohl alles gut läuft, merkt Cas: Das ist zu viel.
Er schließt sein Unternehmen und stürzt sich auf die theoretische Informatik. Sein neues Abenteuer. Cas entdeckt seine Liebe für „formale Methoden“. Besonders die Vorlesung über „Sicherheitsprotokolle“ von Professor Sjouke Mauw hat es ihm angetan. Als Professor Mauw eine Promotionsstelle ausschreibt, bewirbt er sich und bekommt den Job. Das Thema seiner Dissertation - Sicherheitsprotokolle.

Rund fünf Milliarden Menschen [1] lesen, schreiben und spielen heute im Internet. Und das bei einer Weltbevölkerung von acht Milliarden Menschen [2] . Jede Sekunde schicken sie Datenpakete durch das Netz der Netze.

Natürlich kommt dabei auch das Einkaufen per Mausklick nicht zu kurz.

Der weltweite Umsatz im E-Commerce wird 2023 sogar auf 5,9 Billionen US-Dollar [3] geschätzt.

Zur Veranschaulichung dieser Zahl:
Das Saarland, Sitz des CISPA, hat eine Fläche von 2.570 Quadratkilometern [4] .

Würden wir uns 5,9 Billionen US-Dollar in 20-Dollar-Noten auszahlen lassen, bekämen wir 295 Milliarden Scheine.

Damit könnten wir das gesamte Saarland einmal pflastern.

Wenn wir im Internet einkaufen und bezahlen, kommuniziert der Online-Shop natürlich auch mit unserer Bank.

Dabei sorgt das Sicherheitsprotokoll „Transport Layer Security“ (TLS) dafür, dass die gesendeten Datenpakete verschlüsselt werden.

TLS ist zwar nur eines von vielen Protokollen, mit denen sich unsere Datenpakete ihren Weg durch das Internet bahnen, ...

aber erst die mit TLS verschlüsselte Verbindung ermöglicht ...

den sicheren Zahlungsverkehr und damit den weltweiten Online-Handel.
Das macht TLS zu einem der wichtigsten Sicherheitsprotokolle.

2006 beendet Cas seine Promotion. Er geht als Postdoc an die ETH in Zürich, danach an die Universität von Oxford. Im Juli 2015 ernennt ihn die ältestete Universität der englischsprachigen Welt zum Professor für Informationssicherheit.
Im selben Jahr wächst das Internet rasant weiter. Bereits drei Milliarden Menschen nutzen es [5] , mehr als doppelt so viele wie Indien Einwohner hat. Sie schreiben nicht nur E-Mails, sondern verfassen Artikel, teilen Filme und kommentieren Fotos. Mittlerweile surfen sie auch mit Smartphones. Auch der amerikanische Auslandsgeheimdienst NSA ist aktiv und Edward Snowden warnt weltweit. Selbst Deckenlampen, Heizung, Lüftung und Auto kommunizieren über das Internet. Sie alle vertrauen darauf, dass sich die Datenpakete ihren Weg durch die vernetzten Rechner suchen, geleitet und geschützt von Protokollen. Doch dieses technische Fundament knarrt unter der neuen Last. Das gilt vor allem für ein Protokoll - die „Transport Layer Security“.

Der Transport Layer Security (TLS) ist eines der wichtigsten Sicherheitsprotokolle im Internet. Spezifiziert 1999, schuftet es 2015 unter der Versionsnummer 1.2 bereits seit sieben Jahren [6] und schützt so die Integrität und Vertraulichkeit von Online-Daten. Mit der Zeit zeigen sich Schwachstellen. TLS 1.2 benötigt dringend ein Update.

Das ist seit 1986 die Aufgabe der internationalen „Internet Engineering Taskforce“, kurz IETF. Sie finanziert sich über Spenden, zu den geldgebenden Firmen gehören Technologiekonzerne wie „Cisco“, „Ericsson“, „Huawei“ und „Nokia“. In der IETF selbst organisieren sich ehrenamtlich Expert:innen aus Wissenschaft und Industrie. In Arbeitsgruppen diskutieren sie über öffentlich zugängliche Mailinglisten. Persönlich treffen sie sich maximal drei Mal im Jahr. „We reject kings, presidents and voting. We believe in rough consensus and running code“ [7] , lautet ihr Mantra.
Eric Rescorla in Jeans und schlichtem schwarzen Oberteil, daneben das von ihm geschriebenen Buch als Illustration.

Die Arbeitsgruppe für die Nachfolgeversion von TLS 1.2 wird von Eric Rescorla geleitet, Yale-Absolvent, ehemaliger Sicherheitsarchitekt bei „Skype“ [8] und bis Juni 2023 technischer Direktor für den Internetbrowser „Firefox“ bei der „Mozilla Foundation“ im US-Bundesstaat Kalifornien. Der Amerikaner hat bereits ein Buch [9] über TLS und dessen Vorgänger „Secure Sockets Layer“ (SSL) geschrieben. Expert:innen wie Bruce Schneier loben es. [10] Rescorla ist besorgt. Schon ein Fehler in der Spezifikation von TLS 1.3 könnte das Internet in die Knie zwingen. Er kontaktiert deswegen auch Forschende außerhalb des IETF. Noch hat er einen nicht auf der Liste - Cas.

2015, ein Sommerabend in Oxford. Als Professor hat sich Cas vorgenommen, mehr auf die Balance zwischen Leben und Arbeit zu achten. Spät abends E-Mails zu beantworten, gehört nicht dazu. Doch als der Name Thyla Van Der Merve auftaucht, zögert er nicht. Die Doktorandin von der „Royal Holloway University of London“ kennt er bereits. Van Der Merve ist auf der Suche nach der besten Software für ein neues, hochkarätiges Projekt. Sieben E-Mails und 90 Minuten später hat sie noch viel mehr. Das Team steht.

Neben Thyla Van Der Merve gehört ihr Kollege Sam Scott dazu, hinzu kommen Cas und sein Doktorand Marko Horvat. Gemeinsam wagen die vier, was sich bisher niemand getraut hat: Die „formale Verifikation“ von TLS 1.3 mit all seinen Komponenten.

Illustration - Verschiedene Geräte (Laptop, Tablet, Smartphone) mit typischen Internetanwendungen (Paypal, Youtube, Amazon)

Seit dem Untergang des Passagierschiffes „RMS Titanic“ kennen wir die Tücke von Eisbergen: Auf hoher See ist ein großer Teil von ihnen nicht sichtbar.
Auch das Surfen im Internet verbirgt vieles: Egal, ob wir Bücher online bestellen, auf dem Smartphone per Internetverbindung Musikstücke hören oder gar herunterladen, die wichtigsten Vorgänge geschehen in der Tiefe der Technik.

Illustration - Verschiedene Bildschirme mit Softwareentwickler Werkzeuge und Programmiersprachen

Bevor wir auch nur ein Bild sehen oder Text lesen, haben das eigene Gerät und Rechner im Internet bereits Nachrichten ausgetauscht und Programmcode ausgeführt. Alles greift wie Zahnräder ineinander. Bereits ein kleiner Fehler kann daher ein ganzes Programm, einen ganzen Dienst lahmlegen. Erst leuchten Warnlampen rot, dann sehen wir rot.

Formale Verifikation soll dies verhindern.

Das Besondere an formaler Verifikation: Mit ihrer Hilfe können wir garantieren, was uns das Testen nur hoffen lässt: Programme und Protokolle funktionieren ohne Fehler.
Formale Verifikation ersetzt Hoffen durch Beweise.

Der Nachteil: Formale Verifikation ist sehr aufwändig. Sie benötigt eine präzise mathematische Definition des Verhaltens des zu überprüfenden Programms oder Protokolls. Diese sogenannte Spezifikation muss mathematisch bewiesen werden.

Der berühmte britische Informatiker Sir Tony Hoare rief daher auf, Software-Werkzeuge zu entwickeln, die „soweit es geht, automatisiert, Programme formal verifizieren“ [11] . Die Entwicklung eines solchen Werkzeuges bezeichnete er als „a grand challenge for computing research“ [12] .

Formal verifizierte Software ist wie ein mathematischer Beweis: Jede Aussage folgt logisch aus der vorangegangenen. Daher muss jede Programmzeile, jeder durch sie beschriebene Rechenweg, mathematisch bewiesen werden.

Jeder, der das Hoare-Kalkül kennt, weiß, wie anstrengend es ist, damit ein Programm formal zu verifizieren. Selbst, wenn es nur wenige Zeilen umfasst.

Heutzutage bestehen Programme und Protokolle aus Tausenden bis mehreren Hunderttausenden Zeilen Programmcode.

Wer sich dieser Herausforderung der formalen Verifikation stellt, fühlt sich schnell in einem Garten voller Irrgänge und ohne Grenzen. Formale Verifikation überfordert uns Menschen.

Wir brauchen Hilfe.

Computer! Sie handeln an der Börse, schlagen Schachgroßmeister und gewinnen Quizsendungen. Ihre Rechenkraft und Schnelligkeit übertrifft uns Menschen.
Können sie die formale Verifikation übernehmen?

Leider erkennen sie nicht, dass eine meterlange Zahnbürste Unsinn ist. Sie kommen auch nicht darauf, kochendes Wasser einzufrieren, um lieber klare statt trübe Eiswürfel im Glas zu haben.
Ihnen fehlt damit sowohl das Wissen über unsere reale Welt als auch die Fähigkeit, um die Ecke zu denken. Aber genau das verlangt formale Verifikation.

Mensch und Computer müssen daher zusammenarbeiten, ihre Stärken wie Zahnräder ineinander greifen lassen und die Schwächen ausgleichen.

Computer und Mensch sind
„Team Formale Verifikation“ .

Inzwischen verwenden nicht nur Technologie-Konzerne wie NVIDIA [13] und Microsoft [14] formale Verifikation. Auch andere Unternehmen setzten sie ein, in der Hardware- und Softwareentwicklung.

Ein Grund dafür ist auch das Internet: Es erhöht die Brisanz von Fehlern in Software und Protokollen wie Benzin einen Brand beschleunigt.

Am CISPA erkunden Forschende daher formale Verifikation, um neben der Betriebssicherheit von Software und Protokollen auch deren IT-Sicherheit garantieren zu können.

Auf diese Weise kann formale Verifikation der Technik-Tiefe ihre Tücken nehmen. Die Warnlampen leuchten nicht mehr rot, alles ist im grünen Bereich. Das ist die Vision.

Für Eisberge hat man solch eine Technologie nicht gefunden. Stattdessen wird ihre Wanderschaft im Nordatlantik und in der Antarktis per Flugzeug und Radarsatelliten überwacht. Die Internationale Eispatrouille warnt dann per E-Mail.

„Wenn wir keinen Angriff finden, werden sie sagen: Was ihr macht, ist irrelevant und bringt keinen Mehrwert.“ Cas spricht das Risiko gegenüber Thyla, Sam und Marko offen an. Es ist Sommer 2015, die Gruppe steht am Anfang des Projektes. Cas kennt die Skepsis anderer Wissenschaftler. Bereits während seiner Zeit in Zürich hat man ihre Zweifel an ihn herangetragen. Er macht sich auch Sorgen um die Karriere der Promovierenden. Wenn sie keine Sicherheitslücke entdecken, werden sie nur kostbare Zeit verschwenden, anstatt ihre Dissertationen voranzutreiben. Cas fasst einen Entschluss [15] : Sie werden es nicht bereuen.

Ein neues Sicherheitsprotokoll entsteht. Expert:innen studieren es sorgfältig und zeigen mit dem Daumen nach oben oder nach unten [16] . So sah die Überprüfung bisher aus. Jedoch Cas & Co. wollen die Sicherheit von TLS 1.3 mittels mathematischer Beweise garantieren. Ein wichtiges Werkzeug ist dabei eine Software, die solche Beweise liefern kann. Expert:innen nennen diese Programme „Beweiser“. Im Englischen heißen sie „Prover“.

Die Forschenden setzen auf einen Prover, für den Cas bereits während seiner Dissertation erste Ideen hatte und den er zusammen mit Simon Meier, Benedikt Schmidt und Professor David Basin in Zürich entwickelt hat. Wie damals während seiner Computerspielzeit übernimmt Cas weitere Rollen. Er sucht nach einem Namen, der in mehreren Sprachen funktioniert, kein Schimpfwort, keine Abkürzung ist. Cas lässt sich von Tieren inspirieren und stößt auf einen Affen mit einem weißen Schnurrbart. Er schlägt das Affengesicht als Logo, seine Tribus-Bezeichnung als Namen vor, geboren ist der „Tamarin Prover“ [17] .

Der Tamarin Prover analysiert, ob die Schritte eines Sicherheitsprotokolls sicher sind oder von einer angreifenden Person ausgenutzt werden können. Das Programm kann Protokolle mit komplexen Abläufen und vielen beteiligten Personen oder Endgeräten überprüfen. Bei der rasanten Entwicklung des Internets, ein Muss.
Der Tamarin Prover geht dabei wie eine Ermittlerin, ein Ermittler am Tatort vor. Er folgt Spuren und prüft, welche zu der Täterin, dem Täter führen. Werkzeuge sind hierbei nicht Lupe und Fingerabdruckpinsel, sondern mathematische Methoden. Hat die Software alle Fährten abgearbeitet und ist dabei auf keine angreifende Person gestoßen, ist das Protokoll sicher. Q.E.D .

Ein dekorativer Pfad der nach einer Abzweigung zu zwei Informationsblöcken führt.
Ein an ein Verkehrsschild angelehntes Warnung-Symbol.

Attacke gefunden

Ein Sicherheitsschloss.

Keine Attacke gefunden

Thyla und Sam sind bereits mitten in ihrem Praktikum bei Eric Rescorla und der Mozilla Foundation in Kalifornien, USA. Sie versuchen mit dem Tamarin Prover warm zu werden. Sie arbeiten die Dissertationen durch, die über den Prover geschrieben wurden, extrahieren alles, was ihnen hilft, das Werkzeug von Grund auf zu verstehen. Marko ist in Oxford und immer nur einen Skype-Anruf entfernt. Er gibt ihnen einen Crashkurs, mit Baby-Beispielen, wie „endliche Automaten“ und grundlegende Sicherheitsprotokolle. Nach einigen Wochen können Thyla und Sam unabhängig von Marko mit dem Prover experimentieren. Auch bei der formalen Verifikation machen sie enorme Fortschritte. Sie sind bereit für TLS 1.3.

Damit der Tamarin Prover TLS 1.3 durchleuchten kann, braucht die Software vorab drei Puzzlestücke.
Sam, Thyla und Marko spezifizieren, was der imaginäre Angreifer kann. Sie entscheiden sich für einen alten Bekannten. Er kann das gesamte Netzwerk kontrollieren, Nachrichten einschleusen, abfangen, verändern und löschen. Sein Name steht seit Jahren in der einschlägigen Forschungsliteratur: „Dolev-Yao“.

Ein Stapel Papier, bedruckt mit der Spezifikation von TLS1.3. Daneben ein Bleistift und ein Radierer.

Sie diskutieren lange und oft, um zu entscheiden, welche Sicherheitsbedingungen TLS 1.3 erfüllen muss.

Ein dekorativer Pfad zum nächsten Bild.

Auch das halten sie in einer so genannten spthy-Datei für den Tamarin Prover fest.

Ein Monitor der einen Ausschnitt des mathematischen Modells zeigt. Davor eine Tastatur und eine Maus.

Die Expert:innen des IETF schreiten mit dem Entwurf von TLS 1.3 voran. Sie produzieren minimalistischen Text. Die Promovierenden sind froh, dass dieser immerhin digital verfügbar ist und sie ihn durchsuchen können. Denn sie müssen die in Englisch beschriebenen Kommunikationsschritte des Protokolls in spe in eine Sprache übersetzen, die auch der Tamarin Prover versteht. Sie bauen das „Modell“.

Im Prover-Modell wird jeder Protokollschritt dargestellt. Man kann sich jeden Protokollschritt als einen Spielstein vorstellen.

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.

„Royal Holloway University of London“, Fachbereich Mathematik, McCrea Gebäude, Raum 255. Sams Schreibtisch ist übersät mit ausgedruckten Fachartikeln [18] . Acht Promovierende sitzen in dem Büro, das etwa die Größe eines Klassenzimmers besitzt. Die Arbeitsplätze unterscheiden sich nur durch die Bücher in den kleinen Regalen dahinter. Es geht um Fachgebiete wie „Kategorientheorie“, „Geometrie“ und „Kryptografie“. Sam ist wieder zurück in England. Immer wieder haben die vier Forschenden Designänderungen der IETF in ihr Modell eingearbeitet und dabei höllisch aufgepasst, jede betroffene Stelle zu aktualisieren. Sie haben beim Prover den Luxus einer Entwicklungsumgebung vermisst und sich mit einem „Makroprozessor“ beholfen. Drei Monate nach Projektstart sind alle Vorarbeiten für den Beweiser fertig. Das Beweisen beginnt.

Erst denkt der Mensch, dann rechnet der Tamarin Prover.

Ein Mensch analysiert den Graphen ...

... und zieht daraus Schlüsse, wie er das Modell ändern muss.

Das Programm sucht nach Angriffen. Wenn es nicht terminiert, kann das verschiedene Gründe haben.

Der Tamarin Prover stellt deshalb den Informationsfluss des Protokolls als Graph dar. Dieser geht bis zum Stopppunkt.

Der Zyklus beginnt von Neuem.

Der Tamarin Prover bietet zwei Möglichkeiten, Beweise zu konstruieren. Es gibt einen vollautomatischen Modus, der Logik und „Heuristiken“ kombiniert, um Beweise zu finden. Wenn das Werkzeug die automatische Beweissuche beendet, gibt es entweder einen Korrektheitsbeweis oder ein Gegenbeispiel, das einen Angriff ermöglicht.
Da die Korrektheit von Sicherheitsprotokollen ein sogenanntes unentscheidbares Problem ist, kann der Tamarin Prover die Beweisführung manchmal nicht abschließen. Er benötigt dann Hilfe, die er über seinen interaktiven Modus erhält. Ein Mensch muss die Beweiszustände überprüfen und den Informationsfluss, den die Software als „Graphen“ visualisiert, durchgehen. Die manuelle Beweisführung wird mit automatischer Beweissuche kombiniert.

Von den vier Forschenden übernimmt Sam diese Aufgabe. Ihn zieht es schon lange von der Grundlagenforschung in die Anwendung. Während seines Grundstudiums an der Universität Warwick hat er Mathematik studiert und sich zu Beginn seiner Dissertation mit „Kryptographie“ und „Zahlentheorie“ beschäftigt. Jetzt ist beweisbare Sicherheit sein Thema und der Tamarin Prover sein Sparringspartner.

„Der Tamarin Prover kann einem nicht wirklich sagen, was man falsch gemacht hat, weil er seines Wissens nach nur das Protokoll ausführt, das man ihm vorgegeben hat“, erklärt Sam. Wenn der Prover nicht weiterkommt oder sogar eine Attacke markiert, überprüft Sam deswegen immer zuerst das Modell des Protokolls. Er schaut nach, ob nicht doch irgendwo ein Argument, ein Parameter oder eine Variable vergessen wurde. Glaubt er, den Fehler behoben zu haben, startet er den Prover samt korrigiertem Modell erneut. Immer eine große Hilfe: Die grafische Benutzeroberfläche.

Da die Berechnung des gesamten Beweises zu viel Rechenzeit in Anspruch nimmt, teilen die vier Forschenden den Beweis in 40 Beweisdateien auf. Mit Hilfe von über 100 kleinen, selbst geschriebenen Hinweisen für den Prover, so genannten Lemmata, schaffen sie es, dass der Tamarin Prover 35 der 40 Beweisdateien automatisch beweisen kann. Den Rest erledigt Sam interaktiv mit dem Prover. Sie sind Team Tamarin.

Oktober 2015, es ist Abend. Wieder sitzt Sam im Großraumbüro in Royal Holloway, wieder zeigt sein Bildschirm die grafische Benutzeroberfläche des Tamarin Provers. Er klickt, um Lemmata zu beweisen. Doch der Tamarin Prover bleibt bei seinen roten Pfeilen. Damit sagt die Software: Hier kommt die Angreiferin, der Angreifer an Informationen, an die er nie kommen sollte. Immer wieder geht Sam den Graphen durch. Warum funktioniert der Beweis nicht? Es liegt nicht am Modell. Sam ist sich ziemlich sicher [19] . Er schreibt eine E-Mail an die Gruppe und an Eric Rescorla, mit dem er seit dem Mozilla-Praktikum in Kontakt steht. An die E-Mail hängt er die Bilddatei mit dem riesigen Graphen. Der Betreff der E-Mail zu später Stunde lautet: „Habe etwas Seltsames gefunden.“

Ein Brief der aus einen Briefumschlag herausschaut. Als Betreff: „Found something odd“ mit den Adressaten aus der Geschichte. Dazu ein Warnungssymbol und ein Papierflieger.

Zwei Stunden später. Eric Rescorla ist der erste, der sich meldet. Es ist ein Angriff.

Der nächste Morgen im Team. Laut Sam herrscht weder Krisen- noch Partystimmung, sondern Konzentration. Die Gruppe überprüft den Angriff und macht sich sofort daran, eine Gegenmaßnahme zu entwickeln. Sie wollen den Angriff entschärfen, der sogar Hacker beeindrucken würde. Mindestens 18 Netzwerknachrichten muss die imaginäre angreifende Person verschicken, drei verschiedene Mechanismen von TLS 1.3 kombinieren [20] , dann kann er in die Identität eines Opfers schlüpfen und beispielsweise dessen Online-Geldkonto plündern, während die Bank nur eine legale Überweisung wahrnimmt. Die Authentifizierung ist gebrochen.
Wieder hilft der Tamarin Prover der Gruppe. Zu seinen Stärken gehört die schnelle Entwicklung von Protokollen, das sogenannte Rapid Prototyping. Immer wieder lassen Sam, Thyla, Marko und Cas den Tamarin Prover rechnen. So bekommen sie die Bestätigung, dass ihre neue Lösung wirklich sicher ist. Nach knapp einer Woche, am Samstag, den 31. Oktober 2015, um 12:35 Uhr Ortszeit, verkündet Sam dann den Angriff und den Fix auf der Mailingliste der IETF [21] . Lehrmaterial für die Experten. Q.E.D.

Der Graph zu TLS 1.3: Der Tamarin Prover ermöglicht die Analyse in mehreren Detailstufen.

Der Graph zu TLS 1.3: Der Tamarin Prover ermöglicht die Analyse in mehreren Detailstufen.

Wissenschaft und Industrie schenken den vier Forschenden nun Aufmerksamkeit. Sam präsentiert die Ergebnisse im Januar 2016 auf der Industrie-Konferenz „Real World Crypto“ in Stanford, Kalifornien, Marko tut dies [22] auf der weltweit renommierten Konferenz „IEEE Symposium on Security & Privacy“ ein paar Monate später. Bei allen drei Promovierenden geht nun auch ein großer Teil ihrer Dissertation über TLS 1.3. Sie schreiben auch zwei Fachartikel, die bis heute ihre Publikationsliste in Anzahl der Zitationen anführen. Cas wird von Eric Rescorla sogar zu einer Besprechung der TLS-Arbeitsgruppe in das Hauptquartier von Mozilla in Kalifornien eingeladen. Ein Ritterschlag für die vier und den Tamarin Prover.

Sommer 2022.
Der Tamarin Prover hat bereits rund 50 Protokolle [23] erfolgreich untersucht. Die Anwendungen reichen vom heimischen WLAN über elektronisches Bezahlen bis hin zur Kommunikation zwischen Kraftwerken [23] .
Thyla ist jetzt „Security Engineering Manager“ bei Google in Zürich, Sam hat ein Start-up namens „Oso“ in New York mitgegründet und Marko lehrt an der Universität Zagreb.
Cas sitzt in seinem Eckbüro im ersten Stock im CISPA Helmholtz-Zentrum für Informationssicherheit in Saarbrücken. Das Interview über TLS 1.3 neigt sich dem Ende zu. „Ich bin mir sicher, dass sie diesen Angriff nie entdeckt hätten“, sagt er rückblickend und fügt hinzu: „Nach mehr als zehn Jahren Erfahrung kann ich mit Sicherheit sagen, dass es meistens etwas zu finden gibt.“

Auf die Frage nach der Wirkung der formalen Verifikation von TLS 1.3 antwortet Eric Rescorla per E-Mail: „TLS 1.3 hat als Blaupause für zukünftige Protokollarbeit gedient. Seither half uns die formale Verifizierung in mehreren Fällen potenzielle schwerwiegende Mängel zu finden und zu beseitigen.“

Einige Wochen nach dem Interview. Der Parkettboden im Hörsaal des CISPA riecht nach Reinigungsmittel und die Wanduhr zeigt zwanzig vor zwölf. Die letzten Minuten der Vorlesung laufen. „Real-world protocols“ heißt das Thema heute. Cas hält sie. Seine Arme, seine Hände, sogar seine Finger bewegen sich. Sie formen imaginäre Kugeln, malen Kreise, ziehen Linien in die Luft. Sie umrahmen, teilen, zählen auf. Auch die Füße machen mit. Wiegeschritt, vor und zurück. Cas tanzt durch seine Vorlesung. Er ist in seinem Element.

Das Logo der Tamarin Prover Software. Ein Tamarin-Affe im Pixel-Art-Stil.

CREDITS

Research & Text - Gordon Bolduan
Visual Design - Yushun Zhao
Motion Design - Sascha Schäfer, Yushun Zhao
Web Development - Sascha Schäfer
Project Management - Georg Demme
Development Support - Johannes Ebersold, Wolfgang Herget, Sebastian Weisgeber
User Research - Sarah Cieslik

Special Thanks

Videography - Tobias Ebelshäuser
Interviewees - Cas Cremers, Niklas Medinger, Aurora Naska, Sam Scott

Quellen

1

Cisco. “Cisco Annual Internet Report (2018-2023) White Paper” . Cisco, 2019. [Online]. Available: Link (External) [Accessed: May 5, 2023].

2

United Nations, “World Population Prospects 2022: Summary of Results” , Department of Economic and Social Affairs, Population Division, 2022. [Online]. Available: Link (External) [Accessed: May 5, 2023].

3

U.S. Department of Commerce. (2021). “ Global E-Commerce Sales: Size and Forecast” . International Trade Administration. Link (External) [Accessed: May 5, 2023].

4

“Saarland”, Wikipedia, [Online]. Available: Link (External) . [Accessed: May 5, 2023].

5

ITU. (2015). “ ICT facts and figures 2015 ”. International Telecommunication Union. [Online]. Available: Link (External) . [Accessed: May 4, 2023].

6

T. Dierks, E. Rescorla, (2008). “ The Transport Layer Security (TLS) Protocol Version 1.2” . IETF RFC 5246. [Online]. Available: Link (External) . [Accessed: May 4, 2023].

7

A. L. Russell, (2006). “'Rough Consensus and Running Code' and the Internet-OSI Standards War” . IEEE Annals of the History of Computing, 28(3), 48–61. Link (External)

8

E. Rescorla, [LinkedIn-Profil]. (n.d.). Available: Link (External) . [Accessed: May 4, 2023].

9

E. Rescorla, SSL and TLS: Designing and Building Secure Systems . Addison-Wesley Professional, 2000. Available: Link (External) . [Accessed: May 4, 2023].

10

E. Rescorla, SSL and TLS: Designing and Building Secure Systems , Addison-Wesley Professional, 2000. Available: Link (External) . [Accessed: May 4, 2023].

11

C. Jones, P. O'Hearn, J. Woodcock, “Verified Software: A Grand Challenge” , Computer, vol. 39, pp. 93–95, April 2006.

12

T. Hoare, "The verifying compiler: A grand challenge for computing research" , Journal of the ACM, vol. 50, no. 1, pp. 63-69, January 2003.

13

J. Alben. “Formal Verification Specialist Oski Joins NVIDIA | NVIDIA Blog” . NVIDIA Blog. Available: Link (External) . [Accessed: February 10, 2023].

14

T. Ball, B. Cook, V. Levin, S. K. Rajamani, "SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft" , January 28, 2004, Publications of the SLAM project, Redmond, WA 98052, United States of America. [Online]. Available: Link (External) . [Accessed: February 10, 2023].

15

Prof. Dr. C. Cremers, personal communication, April 5, 2022.

16

G. Bella, Formal Correctness of Security Protocols , Berlin, Germany: Springer, 2007.

17

“Tamarin Prover” , Available: Link (External) . [Accessed: May 25, 2023].

18

Dr. S. Scott, personal communication, May 28, 2020.

19

Dr. S. Scott, personal communication, May 28, 2020.

20

D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols” , IEEE Security and Privacy Magazine, Institute of Electrical and Electronics Engineers.

“Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication” , YouTube, [Video published on Sep 2, 2016], Available: Link (External) . [Accessed: May 30, 2023].

D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols” , IEEE Security and Privacy Magazine, Institute of Electrical and Electronics Engineers.

21
22
23

S. Scott, “[TLS] Revision 10: possible attack if client authentication is allowed during PSK” , TLS Mailing List, message sent on October 31, 2015. Available: Link (External)