Abstracting cryptographic protocols

Abstract

Cryptographic protocols can be used to harden the security of IT systems, but only if these protocols are carefully woven into the system. Thus, a security analysis of the overall system is necessary to ensure that the cryptographic protocols are effectively applied. The classical proof technique for computational security proofs (reduction proofs) are, due to their complexity, hard to automatically derive, already for medium-sized IT systems. Hence, there is a successful line of research about abstracting cryptographic protocols. In this thesis, we consider two kinds of abstractions: i) symbolic abstractions, where formal rules characterize the attacker’s capabilities and the functionality of the cryptographic operations, and ii) ideal functionalities, where all honest parties are replaced by one single incorruptible machine. For symbolic abstractions, we study their accuracy (called computational soundness), i.e., under which conditions these abstractions capture all cryptographic attacks. We establish a computational soundness result for malleable zero-knowledge proofs, and we establish two results for re-using existing computational soundness proofs, in particular for obtaining strong equivalence properties. Additionally, we devise an ideal functionality for the most-widely used anonymous communication protocol Tor and (using the UC framework) prove its accuracy. For improving Tor’s performance, we moreover propose a novel, provably secure key-exchange protocol.

Kryptographische Protokolle haben den Zweck die Sicherheit von IT Systemen zu härten, allerdings sind diese Protokolle nur dann wirksam, wenn sie sorgfältig in ein System eingearbeitet werden. Da kryptographische Sicherheitsbeweise, eine Standardtechnik für Sicherheitsbeweise, inhärent komplex und fehleranfällig sind, gibt es erfolgreiche Ansätze zur modularen Abstraktion von kryptographischen Protokollen. Die vorliegende Arbeit analysiert die Fehlerfreiheit von zwei Arten von Abstraktionen: ideale Funktionalitäten, ein Szenario in dem die ehrlichen Parteien als unkorrumpierbare Maschine mit einem geteilten Speicher dargestellt werden, und symbolische Abstraktionen, ein Szenario in dem als Berechnungsmodell ein symbolisches Kalkül betrachtet wird und kryptographische Operationen mittels simplen, formalen Regeln charakterisiert werden. Die Fehlerfreiheit von symbolischen Abstraktionen wird Computational Soundness genannt. Wir präsentieren Resultate, um Wiederbenutzbarkeit von existierenden Computational Soundness Beweisen zu ermöglichen, insbesondere um Garantien für starke äquivalenzbasierte Eigenschaften zu erhalten. Wir benutzen ideale Funktionalitäten, um anonyme Kommunikationstechniken zu analysieren. Wir analysieren die Sicherheit von Tor (dem meistegenutzten Anonymitätsnetzwerk) zugrundeliegenden Protokolls und schlagen Techniken zur Verbesserung der Leistung des Tor Netzwerkes vor.