TU Darmstadt / ULB / TUprints

Modeling Advanced Security Aspects of Key Exchange and Secure Channel Protocols

Günther, Felix (2018)
Modeling Advanced Security Aspects of Key Exchange and Secure Channel Protocols.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication

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

Download (2MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Modeling Advanced Security Aspects of Key Exchange and Secure Channel Protocols
Language: English
Referees: Fischlin, Prof. Dr. Marc ; Paterson, Prof. Dr. Kenneth G.
Date: 2018
Place of Publication: Darmstadt
Date of oral examination: 6 February 2018
Abstract:

Secure communication has become an essential ingredient of our daily life. Mostly unnoticed, cryptography is protecting our interactions today when we read emails or do banking over the Internet, withdraw cash at an ATM, or chat with friends on our smartphone. Security in such communication is enabled through two components. First, two parties that wish to communicate securely engage in a key exchange protocol in order to establish a shared secret key known only to them. The established key is then used in a follow-up secure channel protocol in order to protect the actual data communicated against eavesdropping or malicious modification on the way.

In modern cryptography, security is formalized through abstract mathematical security models which describe the considered class of attacks a cryptographic system is supposed to withstand. Such models enable formal reasoning that no attacker can, in reasonable time, break the security of a system assuming the security of its underlying building blocks or that certain mathematical problems are hard to solve. Given that the assumptions made are valid, security proofs in that sense hence rule out a certain class of attackers with well-defined capabilities. In order for such results to be meaningful for the actually deployed cryptographic systems, it is of utmost importance that security models capture the system's behavior and threats faced in that 'real world' as accurately as possible, yet not be overly demanding in order to still allow for efficient constructions. If a security model fails to capture a realistic attack in practice, such an attack remains viable on a cryptographic system despite a proof of security in that model, at worst voiding the system's overall practical security.

In this thesis, we reconsider the established security models for key exchange and secure channel protocols. To this end, we study novel and advanced security aspects that have been introduced in recent designs of some of the most important security protocols deployed, or that escaped a formal treatment so far. We introduce enhanced security models in order to capture these advanced aspects and apply them to analyze the security of major practical key exchange and secure channel protocols, either directly or through comparatively close generic protocol designs.

Key exchange protocols have so far always been understood as establishing a single secret key, and then terminating their operation. This changed in recent practical designs, specifically of Google's QUIC ("Quick UDP Internet Connections") protocol and the upcoming version 1.3 of the Transport Layer Security (TLS) protocol, the latter being the de-facto standard for security protocols. Both protocols derive multiple keys in what we formalize in this thesis as a multi-stage key exchange (MSKE) protocol, with the derived keys potentially depending on each other and differing in cryptographic strength. Our MSKE security model allows us to capture such dependencies and differences between all keys established in a single framework. In this thesis, we apply our model to assess the security of both the QUIC and the TLS 1.3 key exchange design. For QUIC, we are able to confirm the intended overall security but at the same time highlight an undesirable dependency between the two keys QUIC derives. For TLS 1.3, we begin by analyzing the main key exchange mode as well as a reduced resumption mode. Our analysis attests that TLS 1.3 achieves strong security for all keys derived without undesired dependencies, in particular confirming several of this new TLS version's design goals. We then also compare the QUIC and TLS 1.3 designs with respect to a novel 'zero round-trip time' key exchange mode establishing an initial key with minimal latency, studying how differences in these designs affect the achievable key exchange security. As this thesis' last contribution in the realm of key exchange, we formalize the notion of key confirmation which ensures one party in a key exchange execution that the other party indeed holds the same key. Despite being frequently mentioned in practical protocol specifications, key confirmation was never comprehensively treated so far. In particular, our formalization exposes an inherent, slight difference in the confirmation guarantees both communication partners can obtain and enables us to analyze the key confirmation properties of TLS 1.3.

Secure channels have so far been modeled as protecting a sequence of distinct messages using a single secret key. Our first contribution in the realm of channels originates from the observation that, in practice, secure channel protocols like TLS actually do not allow an application to transmit distinct, or atomic, messages. Instead, they provide applications with a streaming interface to transmit a stream of bits without any inherent demarcation of individual messages. Necessarily, the security guarantees of such an interface differ significantly from those considered in cryptographic models so far. In particular, messages may be fragmented in transport, and the recipient may obtain the sent stream in a different fragmentation, which has in the past led to confusion and practical attacks on major application protocol implementations. In this thesis, we formalize such stream-based channels and introduce corresponding security notions of confidentiality and integrity capturing the inherently increased complexity. We then present a generic construction of a stream-based channel based on authenticated encryption with associated data (AEAD) that achieves the strongest security notions in our model and serves as validation of the similar TLS channel design. We also study the security of such applications whose messages are inherently atomic and which need to safely transport these messages over a streaming, i.e., possibly fragmenting, channel. Formalizing the desired security properties in terms of confidentiality and integrity in such a setting, we investigate and confirm the security of the widely adopted approach to encode the application's messages into the continuous data stream. Finally, we study a novel paradigm employed in the TLS 1.3 channel design, namely to update the keys used to secure a channel during that channel's lifetime in order to strengthen its security. We propose and formalize the notion of multi-key channels deploying such sequences of keys and capture their advanced security properties in a hierarchical framework of confidentiality and integrity notions. We show that our hierarchy of notions naturally connects to the established notions for single-key channels and instantiate its strongest security notions with a generic AEAD-based construction. Being comparatively close to the TLS 1.3 channel protocol, our construction furthermore enables a comparative design discussion.

Alternative Abstract:
Alternative AbstractLanguage

Sichere Kommunikation ist zu einem essentiellen Bestandteil unseres täglichen Lebens geworden. Weitgehend unbemerkt schützt Kryptographie heute unsere Interaktionen, beispielsweise beim Abrufen von E-Mails oder Online-Banking über das Internet, beim Abheben von Bargeld am Geldautomaten oder beim Chatten mit Freunden auf dem Smartphone. Sicherheit in solcher Kommunikation wird durch zwei Komponenten gewährleistet. Zwei Parteien, die sicher kommunizieren wollen, handeln zunächst in einem Schlüsselaustausch-Protokoll einen gemeinsamen geheimen Schlüssel aus. Dieser Schlüssel kann dann im sich anschließenden sicheren Kanal-Protokoll verwendet werden, um die eigentlichen zu kommunizierenden Daten gegen Abhören und bösartige Modifikation während des Transports zu schützen.

In der modernen Kryptographie wird Sicherheit durch abstrakte, mathematische Sicherheitsmodelle definiert, die die betrachtete Klasse von Angriffen beschreiben, gegen die ein bestimmtes kryptographisches System Schutz bieten soll. Solche Modelle ermöglichen eine formale Argumentation, dass kein Angreifer in vernünftiger Zeit die Sicherheit eines Systems brechen kann, unter der Annahme, dass gewisse zugrundeliegende Komponenten sicher oder bestimmte mathematische Probleme schwierig zu lösen sind. Die Gültigkeit der getroffenen Annahmen vorausgesetzt, schließen Sicherheitsbeweise in diesem Sinn bestimmte Klassen von Angreifern mit wohldefinierten Fähigkeiten aus. Damit entsprechende Resultate auf tatsächlich eingesetzte kryptographische Systeme übertragbar sind, ist es von äußerster Wichtigkeit, dass Sicherheitsmodelle das Verhalten der Systeme und ihre Bedrohungen in der 'realen Welt' so akkurat wie möglich abbilden, jedoch gleichzeitig nicht unnötig fordernd sind, um weiterhin die Konstruktion effizienter Systeme zu erlauben. Scheitert ein Sicherheitsmodell darin, einen in der Praxis realistischen Angriff abzubilden, so bleibt ein solcher Angriff selbst für ein in diesem Modell bewiesen sicheres kryptographisches System eine reale Bedrohung, die im schlimmsten Fall die gesamte Sicherheit des Systems zunichte macht.

In dieser Arbeit ergänzen wir die etablierten Sicherheitsmodelle für Schlüsselaustausch und sichere Kanäle, um fortgeschrittene Sicherheitsaspekte abzudecken, die bislang nicht berücksichtigt oder in neueren Konstruktionen wichtiger praktischer Sicherheitsprotokolle ergänzt wurden. Wir wenden unsere erweiterten Sicherheitsmodelle darüber hinaus an, um die Sicherheit weit verbreiteter Kommunikationsprotokolle direkt oder mittels ähnlicher generischer Konstruktionen zu analysieren.

Nach bisherigem Verständnis etablieren Schlüsselaustausch-Protokolle einen einzigen Schlüssel und sind dann beendet. In neueren Konstruktionen, insbesondere dem QUIC ("Quick UDP Internet Connections") Protokoll von Google und der anstehenden Version 1.3 des Transport Layer Security (TLS) Protokolls, hat sich dieses Paradigma allerdings geändert. Beide Protokolle leiten mehrere Schlüssel in einem in dieser Arbeit als mehrstufiger Schlüsselaustausch (MSKE) formalisierten Protokoll ab, wobei die Schlüssel potentiell voneinander abhängig sind und sich in ihrer Stärke unterscheiden. Unsere Arbeit erlaubt es, die Abhängigkeiten und Unterschiede aller dieser Schlüssel in einem einzigen Sicherheitsmodell abzubilden und darin die Sicherheit von QUIC und TLS 1.3 zu analysieren. Für QUIC können wir dabei die erwünschte Gesamtsicherheit bestätigen und gleichzeitig eine unnötige Abhängigkeit zwischen Schlüsseln aufzeigen. Für TLS 1.3 analysieren wir zunächst den Haupt-Schlüsselaustausch und einen verkürzten Modus, für die wir starke Sicherheitseigenschaften für alle Schlüssel ohne unnötige Abhängigkeiten bestätigen können, in Übereinstimmung mit im Entwurfsprozess von TLS gesetzten Zielen. Wir vergleichen darüber hinaus den Schlüsselaustausch in QUIC und in TLS 1.3 bezüglich eines neuen 'zero round-trip time' Modus zur Vereinbarung eines Schlüssels mit minimaler Latenzzeit und studieren, wie sich Unterschiede zwischen den beiden Entwürfen auf die erreichbare Sicherheit auswirken. Als letzten Beitrag im Bereich Schlüsselaustausch formalisieren wir schließlich eine bislang nicht umfassend formalisierte Schlüsselbestätigungseigenschaft, durch die Verfahren den Kommunikationspartnern die tatsächliche beidseitige Ableitung des Schlüssels zusichern. Unsere Formalisierung verdeutlicht dabei, dass die erreichbare Eigenschaft sich für die beiden Parteien leicht unterscheidet, und erlaubt es uns, die Sicherheit von TLS 1.3 in diesem Bezug zu analysieren.

Die Modellierung sicherer Kanäle hat bislang nur die Absicherung von Sequenzen unteilbarer (atomarer) Nachrichten unter einem einzigen Schlüssel berücksichtigt. Unser erster Beitrag zu Kanälen beruht auf der Beobachtung, dass Kanäle in der Praxis nicht den Transport atomarer Nachrichten, sondern nur das Senden von Datenströmen ohne Kennzeichnung individueller Nachrichten ermöglichen. Notwendigerweise unterscheiden sich dadurch auch die Sicherheitseigenschaften dieser Kanäle von den in bisherigen Modellen definierten, wobei insbesondere die mögliche Fragmentierung von Nachrichten in der Vergangenheit zu Verwirrungen und realen Angriffen auf wichtige Implementierungen von Kanälen geführt hat. In dieser Arbeit formalisieren wir solche strombasierten Kanäle und bilden deren inhärent höhere Komplexität in entsprechend angepassten Sicherheitsdefinitionen für Vertraulichkeit und Integrität ab. Wir geben dann eine generische Konstruktion auf Basis von authentisierter Verschlüsselung mit assoziierten Daten (AEAD) an, die starke Sicherheit erreicht und das Konstruktionsprinzip in TLS bestätigt. Des Weiteren studieren wir die Sicherheit von Anwendungen, die inhärent atomare Nachrichten sicher über einen strombasierten Kanal senden wollen. Auf Basis unserer Formalisierung dieses Sicherheitsziels (in Bezug auf Vertraulichkeit und Integrität) bestätigen wir, dass der weit verbreitete Ansatz, die Nachrichten im zu sendenden Datenstrom zu kodieren, tatsächlich sicher ist. Zuletzt wenden wir uns einem weiteren, neuen Paradigma im Entwurf des TLS 1.3 Kanals zu, nämlich der Möglichkeit, Schlüssel während der Laufzeit eines Kanalprotokolls zu erneuern, um die Sicherheit des Kanals zu erhöhen. Wir schlagen hierzu ein formales Modell für solche Kanäle mit mehreren Schlüsseln vor, welches die fortgeschrittenen Sicherheitsaspekte jenseits von Vertraulichkeit und Integrität in einer Hierarchie abbildet. Wir zeigen, dass sich unsere Hierarchie dabei auf natürliche Weise an die etablierten Definitionen für Kanäle mit nur einem Schlüssel anschließt und instanziieren die stärkste Definition in unserer Hierarchie mit einer generischen, AEAD-basierten Konstruktion, die zudem einen Vergleich mit der ähnlichen TLS 1.3 Kanalkonstruktion ermöglicht.

German
URN: urn:nbn:de:tuda-tuprints-71621
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Cryptography and Complexity Theory
Date Deposited: 21 Feb 2018 09:33
Last Modified: 09 Jul 2020 02:00
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/7162
PPN: 426679504
Export:
Actions (login required)
View Item View Item