TU Darmstadt / ULB / TUprints

Future-Proofing Key Exchange Protocols

Brendel, Jacqueline (2019)
Future-Proofing Key Exchange Protocols.
Technische Universität
doi: 10.25534/tuprints-00009642
Ph.D. Thesis, Primary publication

[img]
Preview
Text
thesis_published.pdf
Copyright Information: CC BY-NC-ND 4.0 International - Creative Commons, Attribution NonCommercial, NoDerivs.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Future-Proofing Key Exchange Protocols
Language: English
Referees: Fischlin, Prof. Dr. Marc ; Cremers, Prof. Dr. Cas
Date: 1 October 2019
Place of Publication: Darmstadt
Date of oral examination: 28 November 2019
DOI: 10.25534/tuprints-00009642
Abstract:

Key exchange protocols, first introduced by Diffie and Hellman in 1976, are one of the most widely-deployed cryptographic protocols. They allow two parties, that have never interacted before, to establish shared secrets. These shared cryptographic keys may subsequently be used to establish a secure communication channel. Use cases include the classic client-server setting that is for example at play when browsing the internet, but also chats via end-to-end-encrypted instant messaging applications.

Security-wise, we generally demand of key exchange protocols to achieve key secrecy and authentication. While, informally, authentication ensures that the communicating parties have confidence in the identity of their peers, key secrecy ensures that any shared cryptographic key that is established via the key exchange protocol is only known to the participants in the protocol and can be used securely in cryptographic protocols, i.e., is sufficiently random. In 1993, Bellare and Rogaway gave a first formalization of key exchange protocol security that captures these properties with respect to powerful adversaries with full control over the network. Their model constitutes the basis of the many subsequent treatments of authenticated key exchange security, including the models presented in this thesis.

The common methodological approach underlying all of these formalizations is the provable security paradigm, which has become a standard tool in assessing the security of cryptographic protocols and primitives. So-called security models specify the expected security guarantees of the scheme in question with regards to a well-defined class of adversaries. Proofs that validate these security claims do so by reducing the security of the overall scheme to the security of the underlying cryptographic primitives and hardness assumptions. However, advances in computational power and more sophisticated cryptanalytic capabilities often render exactly these components insecure. Especially the advent of quantum computers will have a devastating effect on much of today's public key cryptography. This is especially true for key exchange protocols since they rely crucially on public-key algorithms.

In this thesis, our focus in future-proofing key exchange protocols is two-fold. First, we focus on extending security models for key exchange protocols to capture the (un)expected break of cryptographic primitives and hardness assumptions. The aim is to gain assurances with respect to future adversaries and to investigate the effects of primitive failures on key exchange protocols. More specifically, we explore how key exchange protocols can be safely transitioned to new, post-quantum secure algorithms with hybrid techniques. Hybrids combine classical and post-quantum algorithms such that the overall key agreement scheme remains secure as long as one of the two base schemes remains secure. For this, we introduce security notions for key encapsulation mechanisms that account for adversaries with varying levels of quantum capabilities and present three new constructions for hybrid key encapsulation mechanisms. Our hybrid designs are practice-inspired and for example capture draft proposals for hybrid modes in the Transport Layer Security (TLS) protocol, which is one of the most widely-deployed cryptographic protocols that enables key agreement.

Furthermore, our notion of breakdown resilience for key exchange protocols allows to gauge the security of past session keys in the event of a failure of a cryptographic component in the key exchange. We exercise our model on variants of the post-quantum secure key exchange protocol NewHope by Alkim et al. Thereby, we confirm the intuition that, in order to guard against adversaries that only have access to quantum computing power in the (more distant) future, it is sufficient to use classically-secure authentication mechanisms alongside post-quantum key agreement to achieve authenticated key exchange.

As with any mathematical statement, theorems in the provable security paradigm are only as valid as the underlying assumptions. A careful consideration of any newly made assumption is thus essential to ensure the meaningfulness of the statement itself and make the assumption a viable tool for future analyses. Thus, secondly, we systematically classify the PRF-ODH assumption, a complexity-theoretic hardness assumption that has been used in key exchange security analyses of such prominent protocols as TLS, Signal, and Wireguard. In particular, we give a unified, parametrized definition of the assumption encompassing different variants that are present in the literature. We relate the resulting parametrized notions in terms of their strength and show where these assumptions fit in the collection of well-understood related hardness assumptions. We finally sketch our result on the impossibility of instantiating this assumption in the standard model, thereby disposing of the uncertainty in the community whether PRF-ODH is in fact a standard model assumption, i.e., removes the usage of some idealized assumptions in key exchange protocol proofs.

Alternative Abstract:
Alternative AbstractLanguage

Schlüsselaustauschverfahren wurden erstmals 1976 von Diffie und Hellman vorgestellt und gehören zu den weitverbreitesten kryptografischen Protokollen. Sie ermöglichen zwei Protokollteilnehmern, welche zuvor noch nicht miteinander in Kontakt standen, einen gemeinsamen geheimen kryptografischen Schlüssel abzuleiten. Dieser kann anschließend dazu verwendet werden, einen sicheren Kommunikationskanal zwischen ihnen aufzubauen. Zu den Hauptanwendungsfällen für kryptographischen Schlüsselaustausch zählt die klassische Client-Server-Kommunikation, wie sie beispielsweise beim Surfen im Internet auftritt. Aber auch Ende-zu-Ende-verschlüsselte Chats werden etwa mit Schlüsselaustauschprotokollen abgesichert.

Die Sicherheitseigenschaften, die wir von Schlüsselaustauschverfahren im Allgemeinen erwarten sind zum einen die Zufälligkeit und Vertraulichkeit der ausgehandelten Schlüssel, sodass diese nur den legitimen Protokollteilnehmern bekannt sind und sich für den sicheren Einsatz in kryptographischen Protokollen eignen.Andererseits soll auch die Identität (einzelner oder aller) Protokollteilnehmer mittels Authentifizierung zweifelsfrei sichergestellt werden. Die erste formale Betrachtung dieser zentralen Sicherheitseigenschaften für authentifizierten Schlüsselaustausch geht auf Bellare und Rogaway aus dem Jahre 1993 zurück. Sie setzten damit den Grundstein für viele weitere Sicherheitsdefinitionen für Schlüsselaustauschprotokolle in Gegenwart eines starken Angreifers, der die Kontrolle über das gesamte Netzwerk verfügt. Auch die Arbeiten in dieser Thesis stützen sich im Kern auf diese ursprüngliche Definition und erweitern diese.

Der zugrundeliegende wissenschaftliche Ansatz für all diese Betrachtungen ist das Konzept der beweisbare Sicherheit, welches nicht mehr wegzudenken ist aus modernen kryptographischen Sicherheitsanalysen. Sogenannte Sicherheitsmodelle spezifizieren die erwarteten Sicherheitseigenschaften des zu analysierenden Verfahrens gegenüber einer wohldefinierten Klasse von Angreifern. Beweise, dass ein Verfahren tatsächlich die definierten Sicherheitsziele erreicht, reduzieren die Sicherheit des Gesamtverfahrens auf die Sicherheit seiner kryptographischen Komponenten.

Unglücklicherweise ist jedoch genau die Sicherheit dieser Komponenten unentwegt durch leistungsfähigere Rechner und neue Techniken in der Kryptanalyse gefährdet. Insbesondere die erwartete technische Revolution durch rechenstarke Quantencomputer droht die moderne Kryptographie stark zu erschüttern. Ein großer Teil der heutzutage verwendeten kryptographischen Algorithmen, die sogenannte Public-Key-Kryptographie, die auch in Schlüsselaustauschverfahren zum Einsatz kommt, wird durch die gesteigerte Rechenleistung von Quantencomputern gebrochen. In dieser Arbeit beleuchten wir, wie Schlüsselaustauschverfahren und ihre Sicherheitsanalysen dieser und weiteren Anforderungen der Zukunft gerecht werden können.

Zum einen zeigen wir, wie bestehende Sicherheitsmodelle für Schlüsselaustauschverfahren so erweitert werden können, dass sie dem (un)erwarteten Bruch kryptographischer Primitive und komplexitätstheoretischer Annahmen standhalten können. Ziel ist es hier, die gewünschten Sicherheitsgarantien im Hinblick auf zukünftige Angreiferarten zu definieren und dann zu untersuchen, wie sich der Bruch bestimmter kryptographischer Bausteine auf die Sicherheit von der Protokolle auswirkt. Konkreter untersuchen wir, wie man derzeit verwendete Algorithmen in Schlüsselaustauschverfahren mittels sogenannter Hybride durch quantencomputerresistente Algorithmen ersetzen kann. Hybride kombinieren die heuzutage verwendeten klassischen Verfahren mit quantencomputerresistenten Verfahren, sodass der Schlüsselaustausch sicher bleibt, solange zumindest eines der zugrundeliegenden Verfahren sicher bleibt. Zu diesem Zweck erweitern wir die bestehenden Sicherheitsmodelle so, dass sie unterschieldich starke Quantenangreifer abbilden können. Zusätzlich präsentieren wir drei praxisnahe Hybridkonstruktionen, die sich an Designvorschlägen für Hybride in einem der am weitesten verbreiteten kryptographischen Protokolle, dem Transport Layer Security (TLS) Protokoll, orientieren.

Unser Breakdown Resilience Modell erlaubt uns weiterhin die Sicherheit von bereits etablierten Schlüsseln zu untersuchen, falls kryptographische Komponenten im Schlüsselaustauschprotokoll in der Zukunft unsicher werden. Wir wenden dieses Modell dann auf Varianten des quantencomputerresistenten Schlüsselaustauschverfahrens NewHope von Alkim et al. an. Unsere Analyse unterstützt nun mit einem formalen Argument die weitherrschende Meinung, dass Schlüsselaustauschverfahren gegen Quantenangreifer in der fernen Zukunft ausreichend geschützt sind, wenn nur die Schlüsselerstellung quantencomputerresistent gestaltet ist, die Authentifizierungmechanismen jedoch nicht.

Wie bei jedem mathematischen Theorem, sind auch Theoreme über die beweisbare Sicherheit von kryptographischen Verfahren nur insofern gültig, als es die darin getroffenen Annahmen sind. Eine strukturierte Untersuchung von bisher unbekannten komplexitätstheoretischen Annahmen in Theoremen ist daher essentiell für deren Richtigkeit und Aussagekraft. Nur dies gewährleistet die bedenkenlose künftige Anwendbarkeit der Annahme selbst, als auch des Theorems.

Dieser Argumentation folgend klassifizieren wir im zweiten Teil der Thesis die komplexitätstheoretische PRF-ODH Annahme, welche sich in Sicherheitsanalysen bedeutender Schlüsselaustauschprotokolle wie TLS, Signal, und Wireguard wiederfindet. Zunächst geben wir hierzu eine vereinheitlichende, parametrisierte Definition der Annahme wieder, welche verschiedene Varianten von PRF-ODH aus der einschlägigen Literatur umfasst. Wir zeigen, wie sich die Annahmen je nach Parameterwahl in ihrer Stärke unterscheiden und wie sie in das Spektrum bereits bekannter, verwandter komplexitätsbasierter Annahmen einzuordnen sind. Seit Einführung von PRF-ODH wurde diskutiert, ob die Verwendung von PRF-ODH es erlaubt, Beweise für Schlüsselaustauschprotokolle ohne idealisierte Annahmen (im sogenannten Standardmodell) zu führen. Zu guter Letzt skizzieren wir unser Unmöglichkeitsresultat, wonach diese Betrachtungsweise unplausibel erscheint und es sich dementsprechend bei PRF-ODH um keine Annahme im Standardmodell handelt.

German
URN: urn:nbn:de:tuda-tuprints-96427
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science > Cryptography and Complexity Theory
DFG-Graduiertenkollegs > Research Training Group 2050 Privacy and Trust for Mobile Users
DFG-Collaborative Research Centres (incl. Transregio) > Collaborative Research Centres > CRC 1119: CROSSING – Cryptography-Based Security Solutions: Enabling Trust in New and Next Generation Computing Environments
Date Deposited: 11 Dec 2019 14:58
Last Modified: 09 Jul 2020 02:58
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/9642
PPN: 456850082
Export:
Actions (login required)
View Item View Item