Analysis of modern real-world protocol faces several key challenges. While the overall complexity of protocols have increased considerably and new security goals have been established over time, our standards for an analysis have increased at the same time. In particular, we require that at least the core idea of security arguments is not only accessible to a small group of experts and we expect computer-aided verification at least for the most important protocols.

In this thesis we prove key-indistinguishability and pseudo-randomness of TLS 1.3 and high-light several methods to address the above-mentioned challenges. In particular we introduce the concept of key-schedule-security and justify it. We consistently phrase our analysis in the language of state-separating proofs (Brzuska, Delignat-Lavaud, Fournet, Kohbrok, and Kohlweiss, AsiaCrypt’18) and prove a generalisation of the concrete TLS key schedule which simplifies the analysis. We choose TLS 1.3 as a realistic example of complex, modern-day cryptographic protocol where a proof of security is in itself a valuable contribution. The concept of key schedule proofs can be applied to other protocols as Brzuska, Cornelissen, and Kohbrok (IEEE S&P ’22) showed for the case of MLS.

State-Separating Proofs (SSP) improves accessibility of proofs by allowing visual arguments with a formal semantic – aiding presentation without sacrificing on rigidity and therefore allowing to efficiently communicate proofs. At the same time we comprehensively specify our components in pseudo-code which allows us to precisely argue on their behaviour. At the same time this formalisation is an important step towards computer-aided verification. As shown by Dupressoir, Kohbrok, and Oechsner (CSF’22), a SSP proof has a natural and direct translation to the EasyCrypt proof assistant.

Key-Schedule Security describes security properties expected of a key schedule. A key schedule isolates the derivation of output keys in a key exchange protocol in terms of the derived, shared secret. Together with the derivation of a shared secret (e. g.via the Diffie-Hellman exchange) and authentication the derivation is a central part of an key exchange protocol. In the following, we consider three aspects of key schedules. In Kapitel 4 we give a formal model of key schedule security. In Kapitel 7 we demonstrate how the property of key schedule security can be used in the proof of a key exchange protocol and in Kapitel 8 we show that TLS 1.3 realises the security notion. Together, the results justify the notion of key schedule security as a building block for analysing key exchange protocols.

Die Analyse moderner und praktisch relevanter Protokolle stellt uns vor mehrere zen- trale Herausforderungen. Nicht nur hat die Komplexität solcher Protokolle über die Jahre zugenommen, zeitgleich ist auch unser Anspruch an eine angemessene Beurteilung ist gewachsen. Dies äußert sich einerseits in der Anforderung, die Ergebnisse einer solchen Analyse einer breiteren Leserschaft zugänglich zu machen und andererseits darin, dass vermehrt Computer-unterstütze Methoden gefordert werden.

In der vorliegenden Arbeit zeigen wir am Beispiel eines Beweises von key-indistinguishability und pseudo-randomness von TLS 1.3 mehrere Methoden um Fortschritt in den oben genannten Problemfeldern zu machen. Namentlich wird die Sicherheitseigenschaft eines Key-Schedule eingeführt und untermauert und die Technik der „State-Separating Proofs“ (Brzuska, Delignat-Lavaud, Fournet, Kohbrok und Kohlweiss, AsiaCrypt’18) konsequent umgesetzt. An Stelle des konkreten Key-Schedules zeigen wir die gewünschten Eigenschaften an einer zulässigen Verallgemeinerung wodurch die Analyse vereinfacht werden kann. TLS dient dabei sowohl als Studie die unbestritten realistisch die Komplexität moderner Protokolle abbildet und der Sicherheitsbeweis ist für sich genommen ein wertvoller Beitrag. Dabei lassen sich die Ergebnisse auf andere Protokolle übertragen wie Brzuska, Cornelissen und Kohbrok (IEEE S&P ’22) am Beispiel von MLS gezeigt haben.

State-Separating Proofs (SSP) bieten dabei im Hinblick auf die Zugänglichkeit von Beweisen visuelle Argumente, die trotzdem eine formale Semantik haben und nicht nur der Anschaulichkeit dienen. Entsprechend wird es ermöglicht die Beweisidee kompakt zu kommunizieren. Gleichzeitig können wir die einzelnen Komponenten vollständig in Pseudocode spezifizieren, was uns einerseits erlaubt sehr präzise über das Verhalten von einzelnen Bestandteilen des Beweises zu Argumentieren und andererseits bereits einen großen Schritt in Richtung von Computer-unterstützter formaler Verifikation darstellt. In diesem Kontext haben Dupressoir, Kohbrok und Oechsner (CSF’22) gezeigt, dass ein Beweis in der SSP Methodik sich direkt und natürlich im Beweisassistenten EasyCrypt umsetzen lässt.

Key-Schedule Sicherheit beschreibt Sicherheitseigenschaften, die von einem Key Schedule erwartet werden. Der Key Schedule isoliert die Ableitung der von einem Key-Exchange-Protokoll zurückgegebenen Schüssel und ist neben der Bereitstellung eines geteilten Geheimnisses (zum Beispiel durch das Diffie-Hellman Protokoll) und der Authentifizierung eine Zentrale Komponente. Wir betrachten dabei drei Gesichtspunkte des Key-Schedules. Wir geben eine formale Definition in Kapitel 4 und zeigen dann in Kapitel 7 dass Key-Schedule-Sicherheit verwendet werden kann um die Sicherheit eines Key-Exchange Protokolls zu beweisen und in Kapitel 8 dass der Key Schedule von TLS 1.3 die gegebene Sicherheitseigenschaft erfüllt. Zusammen rechtfertigen die Ergebnisse Key-Schedule-Sicherheit als Baustein für die Analyse von Key-Exchange-Protokollen.