Mobile applications have access to the data contained on our smartphones. They are also notorious for collecting and transmitting data to advertisers and known trackers despite the presence of strict data protection legislation. This has severe implications for our privacy, as the data collected and transmitted is not necessarily benign and can provide deep insights into the everyday smartphone users. It is important to understand what data is transmitted to whom, what happens to the data, whether the user can influence the data transmission, and whether constant network communication is not already a privacy problem.

In this thesis, those questions are addressed by developing the required tooling to collect encrypted and decrypted app traffic, as well as to conduct an in-depth traffic analysis. We apply this tooling to over 10 000 apps across Android and iOS. Our results prove that apps transmit more data than they publicly admit and that even though users are occasionally asked for consent to data collection, it does not impact overall data transmission. We also find evidence that transmitted personal messages of some chat apps are processed by their providers, and that the constant traffic of apps by itself already presents a privacy risk. Thus, privacy and data protection in mobile apps are contested spaces. Apps frequently skirt European data protection laws, which has implications for users’ privacy, and users need to be aware of this when using their smartphones and apps.

Die Migration zu Post‑Quantum Cryptography (PQC) gewinnt an Bedeutung, da klassische Public‑Key‑Verfahren langfristig nicht mehr als sicher gelten. Der Vortrag gibt einen kurzen Überblick über HAETAE, den koreanischen PQC‑Signaturstandard, und stellt anschließend einen automatisierten Design‑Flow für kryptographische Hardwaremodule vor. Durch eine metadatenbasierte Analyse ersetzt der Ansatz erfahrungsgetriebene Designentscheidungen und integriert Sicherheitsmechanismen bereits während der Entwurfsphase. Dadurch lassen sich effiziente und zugleich seitenkanalresistente Implementierungen neuartiger PQC‑Verfahren systematisch generieren.

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.