TU Darmstadt / ULB / TUprints

Real-World Aspects of Secure Channels: Fragmentation, Causality, and Forward Security

Marson, Giorgia Azzurra (2017)
Real-World Aspects of Secure Channels: Fragmentation, Causality, and Forward Security.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication

[img]
Preview
Text
main.pdf - Submitted Version
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: Real-World Aspects of Secure Channels: Fragmentation, Causality, and Forward Security
Language: English
Referees: Fischlin, Prof. Dr. Marc ; Stam, Dr. Martijn
Date: 2017
Place of Publication: Darmstadt
Date of oral examination: 12 October 2016
Abstract:

A secure channel is a cryptographic protocol that adds security to unprotected network connections. Prominent examples include the Transport Layer Security (TLS) and the Secure Shell (SSH) protocols. Because of their large-scale deployment, these protocols received a lot of attention from academia. Starting with the seminal work of Bellare, Kohno, and Namprempre (BKN; CCS 2002) on the security of SSH, numerous authors analyzed channel protocols using the same approach of BKN to model a channel as a stateful authenticated encryption scheme. However, deployed protocols such as TLS and SSH are inherently complex, and a single mathematical abstraction can hardly capture all aspects that are relevant to security.

In this thesis we reconsider the suitability of the stateful authenticated encryption abstraction for the analysis of real-world channel protocols. In particular, we highlight that such an abstraction is too restrictive, in a sense that we clarify next, to capture three important aspects that do not appear in existing cryptographic models for secure channels.

Firstly, we question the common approach that treats secure channels using atomic encryption and decryption interfaces to transport a sequence of messages. This approach ignores that many real-world protocols, including TLS and SSH, offer a streaming interface instead. To formalize the non-atomic behavior of these protocols we initiate the study of stream-based channels and their security. We formalize notions of confidentiality and integrity by extending the BKN model for stateful authenticated encryption to take the peculiarities of streams into account. Inspired by the TLS 1.3 protocol we present a generic construction of a stream-based channel from any authenticated encryption scheme with associated data (AEAD), and prove its security.

Secondly, we note that while TLS, SSH, and many other channel protocols are typically used for bidirectional interaction, cryptographic models assessing the security of these protocols exclusively account for unidirectional communication, from one sender to one receiver. We correspondingly ask: Do security results for unidirectional channels extend to the bidirectional case? And, in the first place, what does security in the bidirectional setting actually mean? How does all this scale when more than two participants are involved? To answer these questions we conduct a rigorous study of security notions for bidirectional channels and their generalization to the broadcast setting with more than two participants. In a broadcast scenario, confidentiality and integrity need to capture aspects related to the causality of events in distributed systems that have no counterpart in the much simpler unidirectional case. The causality between exchanged messages is particularly relevant, both in terms of functionality and of security, in the context of instant messaging protocols such as TextSecure. Furthermore, we provide generic constructions of broadcast channels from AEAD. We also analyze and validate a traditional heuristic (used, among others, in TLS) of combining two unidirectional channels to realize a bidirectional one.

Finally, we look at forward security, which strengthens regular security by demanding that even if an adversary eventually obtains the secret key in use (by corruption), past uses of the cryptosystem are not compromised. While being a standard requirement for authenticated key exchange, so far, providing forward security was not considered a goal of cryptographic channels in the BKN model and its follow-ups. However, it is considered folklore that forward-secure authenticated encryption schemes can be constructed in a modular way by replacing the key generation procedure with one that produces a sequence of forward-secure keys and then using these keys for re-keying the encryption and decryption routines in use. This approach may also be applied for realizing forward-secure channels. Following this idea, in the last part of the thesis we leave the domain of channels and focus on building forward-secure key generation mechanisms. Secure solutions for the latter primitive have been proposed already in the past. In this thesis we complement the current picture by contributing certain efficiency improvements for sequential key generators. In particular, we illustrate that our solutions find a natural application in the authentication of log files. Implementations of one of our schemes are installed on millions of computers world-wide.

Alternative Abstract:
Alternative AbstractLanguage

Ein sicherer Kanal ist ein kryptographisches Protokoll das ungeschützte Netzwerkverbindungen absichert. Die prominentesten Beispiele, Transport Layer Security (TLS) und Secure Shell (SSH), erhielten aufgrund ihrer weiten Verbreitung besondere Aufmerksamkeit von Seiten akademischer Forschung. Beginnend mit den Arbeiten von Bellare, Kohno, und Namprempre (BKN; CCS 2002) über die Sicherheit von SSH haben zahlreiche Autoren kryptographische Kanalprotokolle mit einem Ansatz ähnlich dem von BKN analysiert, nämlich Kanäle als zustandsbehaftete authentisierte Verschlüsselung modellierend. Verbreitete Protokolle wie TLS und SSH sind jedoch ihrem Wesen nach komplex, und eine einzelne mathematische Abstraktion kann schwerlich alle für ihre Sicherheit relevanten Aspekte berücksichtigen.

In dieser Dissertation stellen wir die Eignung der Abstraktion als zustandsbehaftete authentisierte Verschlüsselung für die Analyse von Kanalprotokollen in der realen Welt in Frage. Insbesondere zeigen wir auf, dass eine solche Abstraktion zu restriktiv ist, auf eine Weise die wir im Folgenden erklären, um drei wichtige Aspekte abzudecken, die in bisher existierenden kryptographischen Modellierungen von Kanälen nicht auftreten.

Zunächst stellen wir den allgegenwärtigen Ansatz in Frage, der Kanäle aufgrund entsprechend formalisierter Schnittstellen als Transportmittel für atomare Nachrichten auffasst. Der genannte Ansatz ignoriert, dass viele Protokolle in der realen Welt, einschließlich TLS und SSH, tatsächlich strom-orientierte Schnittstellen anbieten. Zum Studieren des nicht-atomaren Verhaltens solcher Protokolle und ihrer Sicherheit entwickeln wir Vertraulichkeits- und Integritätsbegriffe auf Basis des Modells für zustandsbehaftete authentisierte Verschlüsselung von BKN, um den Eigenheiten von strom-basierten Protokollen Rechnung zu tragen. Inspiriert vom TLS 1.3-Protokoll präsentieren wir eine generische Konstruktion eines strom-basierten Kanals, auf Grundlage von authentisierter Verschlüsselung mit assoziierten Daten (AEAD), und beweisen ihre Sicherheit.

Zweitens stellen wir fest, dass TLS, SSH, und viele weitere Kanalprotokolle typischerweise für bidirektionale Interaktion verwendet werden, während kryptographische Modelle solche Protokolle ausschließlich im Hinblick auf unidirektionale Kommunikation bewerten, d.h., mit genau einem Sender und einem Empfänger. Entsprechend fragen wir: Lassen sich Ergebnisse über unidirektionale Kanäle auf den bidirektionalen Fall übertragen? Und, unmittelbarer, was bedeutet Sicherheit im bidirektionalen Fall überhaupt? Wie skalieren diese Eigenschaften wenn mehr als zwei Teilnehmer vorhanden sind? Um diese Fragen zu beantworten studieren wir Sicherheitsbegriffe für bidirektionale Kanäle und ihre Verallgemeinerung zum Broadcast Setting, in dem mehrere Teilnehmer vorhanden sind und jede Sendung eines Teilnehmers alle übrigen Teilnehmer erreicht. Im letzteren Fall müssen die Definitionen von Vertraulichkeit und Integrität Aspekte von Kausalität in Verteilten Systemen umfassen, die keine Entsprechung im viel einfacheren Fall unidirektionaler Kommunikation haben. Kausale Zusammenhänge zwischen ausgetauschten Nachrichten sind besonders relevant, in Hinblick auf sowohl Funktionalität als auch Sicherheit, im Kontext von Protokollen zum Instant Messaging, etwa TextSecure. In diesem Teil der Dissertation geben wir generische Konstruktionen von Broadcast-Kanälen auf Basis von AEAD an. Wir analysieren und validieren die traditionelle heuristische Methode (benutzt etwa für TLS), einen bidirektionalen Kanal durch die Kombination zweier unidirektionaler Kanäle zu erhalten.

Im dritten Teil dieser Arbeit studieren wir Vorwärtssicherheit, die reguläre Sicherheitsdefinitionen durch die Forderung stärkt, dass sogar im Fall wenn Angreifer (durch Korrumpierung) zu einem Zeitpunkt Zugriff auf verwendetes Schlüsselmaterial erhalten, vergangene Anwendungen des Kryptosystems nicht kompromittiert werden. Obwohl dies ein standardmäßiges Sicherheitsziel von authentisiertem Schlüsselaustausch ist, wurde sein Erreichen bisher nicht als ein Ziel von kryptographischen Kanälen verstanden, zumindest nicht nach den Modellen von BKN und seinen Nachfolgern. Es wird jedoch als Folklore-Ergebnis aufgefasst, dass vorwärtssichere authentisierte Verschlüsselung auf modulare Weise erreicht werden kann durch Ersetzen der Schlüsselerzeugungsprozedur durch eine, die eine Folge von vorwärtssicheren Schlüsseln erzeugt, um dann diese zum Erneuern der Schlüssel von Ver- und Entschlüsselungsroutine zu verwenden. Dieser Ansatz kann auch zum Realisieren vorwärtssicherer Kanäle verwendet werden. Dem folgend verlassen wir im dritten Teil der Dissertation das Gebiet sicherer Kanäle und konzentrieren uns auf die Konstruktion vorwärtssicherer Schlüsselerzeugungsmechanismen. Sichere Lösungen bereits in der Vergangenheit vorgeschlagen worden. Hier komplementieren wir das aktuelle Bild durch explizit effizienzsteigernde Verbesserungen für vorwärtssicheren Schlüsselerzeugungsmechanismen, und illustrieren, dass unsere Lösungen insbesondere eine natürliche Anwendung in der Authentisierung von Log-Dateien finden. Implementationen einer unserer Konstruktionen sind auf Millionen von Computern weltweit installiert.

German
URN: urn:nbn:de:tuda-tuprints-60212
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: 06 Mar 2017 13:04
Last Modified: 06 Mar 2017 13:04
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/6021
PPN: 400283581
Export:
Actions (login required)
View Item View Item