Provable security and real-world protocols : theory and practice

Abstract

In our modern life, network communication has become one of the primary mediums for information transmission, e.g., instant messaging, online shopping, and video conferencing. In order to protect the security of information transmitted over networks, real-world applications are often equipped with cryptographic communication protocols. While some of these protocols are built from small cryptographic primitives and expected to offer strong security guarantees based on some intuition or informal arguments, their comprehensive formal analyses are however missing. A natural question arises: whether these protocols really satisfy their expected security guarantees? This thesis presents the provable security analysis of five cryptographic primitives and large-scale communication protocols: (1) one of the most efficient digital signature implementations Ed25519, (2) the generic authenticated encryption with associated data scheme, (3) the latest version of passwordless authentication standard FIDO2, (4) the popular video conferencing library Zoom, and (5) our own proposal of extended secure messaging protocol eSM. Moreover, this thesis highlights their essential security features in theory and provides suggestions for their practical deployments. In the end, this thesis addresses common obstacles to (large-scale) protocol designs and provable security analyses, provides intuition on the feasibility, and leaves a complete and provable solution as my future work.

In unserer modernen Welt ist die Kommunikation über Netzwerke ein wichtiges Mittel zur übertragung von Informationen. Um die Sicherheit der über Netzwerke übertragenen Informationen zu gewährleisten, werden reale Anwendungen oft mit kryptografischen Kommunikationsprotokollen ausgestattet. Einige dieser Protokolle werden aus kleinen kryptografischen Grundelementen entwickelt und sollen aufgrund von informellen Argumenten starke Sicherheitsgarantien bieten. Dennoch fehlen umfassende formale Analysen für diese Protokolle. Eine naheliegende Frage lautet: Erfüllen diese Protokolle tatsächlich ihre Sicherheitsgarantien? Diese Arbeit präsentiert die nachweisbare Sicherheitsanalyse von fünf kryptografischen Grundlagen und Kommunikationsprotokollen: (1) eine der effizientesten digitalen Signaturen Ed25519, (2) das generische Authenticated Encryption with Associated Data Schema, (3) die neueste Version des kennwortlosen Authentifizierungsstandards FIDO2, (4) die beliebte Videokonferenzbibliothek Zoom, und (5) unseren eigenen Vorschlag für ein erweitertes sicheres Nachrichtenprotokoll, eSM. Zudem hebt diese Arbeit ihre wesentlichen Sicherheitsmerkmale in der Theorie hervor und gibt Empfehlungen für ihre praktische Implementierung. Abschließend behandelt diese Arbeit häufig auftretende Hindernisse bei groß Protokolldesigns sowie deren nachweisbare Sicherheitsanalysen, bietet Einblicke in die Durchführbarkeit und lässt eine vollständige und nachweisbare Lösung als zukünftige Arbeit offen.