Advancing security protocol verification: A journey along the boundaries of the symbolic model

Abstract

Cryptographic protocols underpin modern digital security, yet their formal verification remains a significant challenge. The symbolic model of cryptography addresses this, representing bitstrings as terms and cryptographic operations as semantics of function symbol applications. This approach allows a more abstract representation of protocols, improving scalability and automation during analysis. However, this high level of abstraction can overlook attacks that exploit the subtleties of underlying cryptographic operations. This thesis advances the accuracy of symbolic analysis by refining the abstraction of cryptographic primitives and by assessing the limits of leading verification tools. First, we propose more detailed symbolic models for cryptographic hash functions, authenti- cated encryption with associated data (AEAD), and key encapsulation mechanisms (KEMs). We integrate these models into Tamarin, a leading symbolic verification tool, and demonstrate their ability to automatically detect both known and novel attacks in real-world security protocols. Second, we present the first formal analysis of the Security Protocol and Data Model (SPDM), a widely deployed industry security standard. Our work results in one of the largest Tamarin models to date, pushing the boundaries of symbolic analysis and revealing a severe authentication vulnerability. This discovery led to our proposed fixes being included in both the specification and the reference implementation.

Kryptographische Protokolle sind die Grundlage moderner digitaler Sicherheit, doch ihre formale Verifikation bleibt eine große Herausforderung. Aus diesem Grund wurde das symbolische Modell entwickelt, welches eine abstraktere Darstellung von Protokollen ermöglicht und dadurch höhere Skalierbarkeit und Automatisierung erlaubt. Diese hohe Abstraktionsebene kann jedoch Angriffe übersehen, die die Feinheiten der zugrunde liegenden kryptografischen Operationen ausnutzen. Diese Dissertation verbessert die Genauigkeit der symbolischen Analyse durch die Verfeinerung der Abstraktion von kryptographischen Primitiven und wertet währenddessen die Grenzen von aktuellen Verifikationstools aus. Zunächst erstellen wir detailliertere symbolische Modelle für kryptografische Hash Funktionen, authentifizierte Verschlüsselung mit zugehörigen Daten, und Schlüsselkapselungsmechanismen. Wir integrieren diese Modelle in Tamarin, ein führendes symbolisches Verifikationstool, und demonstrieren ihre Fähigkeit, automatisch bekannte und neue Angriffe in realen Sicherheitsprotokollen zu erkennen. Zweitens präsentieren wir die erste formale Analyse des Security Protocol and Data Model (SPDM), einem weit verbreiteten Industriesicherheitsstandard. Diese Analyse resultiert in einem der bisher umfangreichsten Tamarin-Modelle, das die Grenzen der symbolischen Analyse erweitert und eine schwerwiegende Schwachstelle in der Authentifizierung aufgedeckt.