Web-basierte Authentifizierungs- und Autorisierungsprotokolle wie OAuth 2.0 und OpenID Connect sind heute das Fundament digitaler Identität. Sie ermöglichen Single Sign-On, sichern Cloud-Dienste und schützen Milliarden von Accounts weltweit.
Was dabei als komfortabler "Social Login" begann, wird inzwischen in Hochrisikobereichen eingesetzt:
Mit Erweiterungen wie FAPI 2.0 - die spezifisch für den Einsatz in Hochrisikoumgebungen entwickelt wurden - bilden diese Protokolle heute die sicherheitstechnische Grundlage für (regulatorisch vorgeschriebene) Open Banking-, Open Insurance- und Gesundheitsanwendungen.
Parallel zur wachsenden gesellschaftlichen Bedeutung steigen jedoch auch Komplexität und Angriffsfläche. Zugleich greift "klassische" Protokollanalyse, wie sie für kryptografische Protokolle verwendet wird, oft zu kurz: Bei der Analyse von Web-Protokollen muss eine Vielzahl von Details der Web-Infrastruktur berücksichtigt werden, etwa die genaue Semantik verschiedener Redirect-Techniken, die möglichen Interaktionen zwischen Webseiten innerhalb eines Browsers und so weiter.

Im Rahmen meiner Dissertation habe ich neue und grundlegende Techniken und Modelle zur formalen Analyse von Web-Protokollen entwickelt. Diese habe ich unter anderem eingesetzt, um eine der bislang umfassendsten Web-Protokoll-Sicherheitsanalysen in der Literatur durchzuführen: Meiner formalen Sicherheitsanalyse der FAPI 2.0-Protokollfamilie liegen über 1.000 Seiten direkt relevanter Spezifikationen zugrunde und die zugehörigen formalen Sicherheitsbeweise füllen über 100 Seiten. Entscheidend ist dabei aber nicht nur der Umfang, sondern vor allem auch der Prozess: Die Analyse begleitete die Standardisierung aktiv. So konnte eine ganze Reihe von Schwachstellen identifiziert werden, bevor die Protokolle produktiv eingesetzt wurden - in Zusammenarbeit mit dem zuständigen Standardisierungsgremium habe ich entsprechende Lösungen erarbeitet, welche in die inzwischen finalisierten Standards übernommen wurden und dazu beitragen, die Finanz- und Gesundheitsdaten von Millionen Nutzern zu sichern.

Im Rahmen der Analyse zeigte sich außerdem, dass eine der entdeckten Schwachstellen auch etwa ein Dutzend verwandter Protokollstandards betrifft - Protokolle, die weltweit Milliarden von Accounts absichern, etwa bei Google, Microsoft und Meta. In einem entsprechenden Responsible Disclosure-Prozess wurden - nebst der Information betroffener Softwareanbieter - auch hier Änderungen der betroffenen Spezifikationen angestoßen.

Neben der unmittelbaren praktischen Relevanz der Analyseergebnisse unterstreichen diese auch den allgemeinen Nutzen der entwickelten Techniken für die Analyse von Web-basierten Protokollen und Standards.

Ein weiterer zentraler Beitrag meiner Dissertation war die Mitentwicklung eines Ansatzes zur Mechanisierung von Sicherheitsbeweisen für Web-Protokolle, der maschinell überprüfbare Beweise komplexer Sicherheitseigenschaften für ausführbare und hochgradig detaillierte Modelle erlaubt. Das daraus entstandene DY*-Framework habe ich anschließend in der ersten formalen Analyse des finalen ACME-Standards eingesetzt - dem Protokoll, über das heute die Mehrheit aller TLS-Zertifikate im Web ausgestellt wird.

Der Vortrag gibt einen Einblick in diese Arbeiten und zeigt, wie die entwickelten formalen Methoden nicht nur Sicherheitslücken finden, sondern die Entwicklung zentraler Internetstandards - durch formale Sicherheitsbeweise in aussagekräftigen Modellen - konkret und nachhaltig mitgestalten können.