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

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