Mit dem Test-Of-Time-Award würdigt das CSF seit 2023 Arbeiten „von bleibender Bedeutung und herausragender Wirkung“ – eine besondere Ehre für Forschende. Doch worin genau besteht der wissenschaftliche Beitrag der ausgezeichneten Arbeit?
Im Mittelpunkt der Arbeit stehen moderne Schlüsselaustauschprotokolle, die auf dem Diffie-Hellman-Prinzip beruhen. Das bereits in den 1970er-Jahren entwickelte Verfahren ermöglicht es zwei Kommunikationspartnern, über ein unsicheres Netzwerk einen gemeinsamen geheimen Schlüssel zu vereinbaren, ohne ihn direkt austauschen zu müssen. In den folgenden Jahrzehnten entstanden darauf aufbauend immer komplexere kryptografische Protokolle mit erweiterten Sicherheitsgarantien. Die zugrunde liegenden algebraischen Eigenschaften des Diffie-Hellman-Verfahrens erschwerten jedoch die automatische Sicherheitsanalyse solcher Protokolle erheblich, weil sie von den bestehenden Analysewerkzeugen nicht vollständig erfasst werden konnten.
Diese Lücke konnten Prof. David Basin vom Departement für Informatik der ETH Zürich, seine damaligen Doktoranden Dr. Benedikt Schmidt und Dr. Simon Meier sowie sein ehemaliger Postdoc und heutiger CISPA-Faculty Prof. Cas Cremers mit ihrer Arbeit schließen. Die Forschenden entwickelten einen allgemeinen formalen Rahmen, in dem sich sowohl kryptografische Protokolle als auch ihre Sicherheitseigenschaften mathematisch beschreiben lassen. Auf dieser Grundlage entwarfen sie einen neuartigen Analysealgorithmus, der systematisch alle möglichen Abläufe eines Protokolls untersucht. Dieser Algorithmus kann automatisch nachweisen, dass ein Protokoll die gewünschten Sicherheitseigenschaften erfüllt oder einen Beweis für die Falsifikation dieser Eigenschaften erbringen, was einem Angriff auf das Protokoll entspricht. Die Forschenden implementierten ihren neuartigen Analysealgorithmus auch im Tamarin Prover. Das Paper beschreibt den Kernalgorithmus, der die Grundlage für einen Großteil der späteren Weiterentwicklung des Tools bildete.
Warum ist die Arbeit heute noch relevant?
Die Autoren demonstrierten die Leistungsfähigkeit ihres Ansatzes an anspruchsvollen Fallstudien, darunter dem damals hochmodernen NAXOS-Protokoll. Sie zeigten, dass sich auch komplexe kryptografische Protokolle automatisch auf ihre Sicherheit überprüfen lassen.
Seit ihrer Veröffentlichung haben die in der Arbeit entwickelten Methoden zahlreiche nachfolgende Arbeiten im Bereich der formalen Sicherheitsanalyse beeinflusst. Auch der Tamarin Prover selbst hat sich erheblich weiterentwickelt: Im Laufe der Jahre wurde sein Anwendungsbereich deutlich über die ursprünglich in der Arbeit betrachtete Klasse von Protokollen hinaus erweitert. Heute gilt er als eines der weltweit führenden Werkzeuge zur Modellierung und Analyse kryptografischer Protokolle. Erst kürzlich wurden David Basin und Cas Cremers sowie Dr. Ralf Sasse und Dr. Jannik Dreier auf der Real World Cryptography Conference für ihre Beiträge zur Entwicklung des Tamarin Provers mit dem renommierten Levchin-Preis ausgezeichnet.
Die Sicherheitsprotokolle, die Tamarin analysieren kann, bilden nach wie vor die Grundlage für Anwendungen wie Online-Banking, sichere Webkommunikation, Messaging-Dienste und viele andere sicherheitskritische Systeme.
