Modeling advanced security aspects of key exchange and secure channel protocols

Abstract

Secure connections are at the heart of today’s Internet infrastructure, protecting the confidentiality, authenticity, and integrity of communication. Achieving these security goals is the responsibility of cryptographic schemes, more specifically two main building blocks of secure connections. First, a key exchange protocol is run to establish a shared secret key between two parties over a, potentially, insecure connection. Then, a secure channel protocol uses that shared key to securely transport the actual data to be exchanged. While security notions for classical designs of these components are well-established, recently developed and standardized major Internet security protocols like Google’s QUIC protocol and the Transport Layer Security (TLS) protocol version 1.3 introduce novel features for which supporting security theory is lacking. In my dissertation [20], which this article summarizes, I studied these novel and advanced design aspects, introducing enhanced security models and analyzing the security of deployed protocols. For key exchange protocols, my thesis introduces a new model for multi-stage key exchange to capture that recent designs for secure connections establish several cryptographic keys for various purposes and with differing levels of security. It further introduces a formalism for key confirmation, reflecting a long-established practical design criteria which however was lacking a comprehensive formal treatment so far. For secure channels, my thesis captures the cryptographic subtleties of streaming data transmission through a revised security model and approaches novel concepts to frequently update key material for enhanced security through a multi-key channel notion. These models are then applied to study (and confirm) the security of the QUIC and TLS 1.3 protocol designs.