A theory of types for security and privacy

Abstract

Im modernen Internet sind kryptographische Protokolle allgegenwärtig. Ihre Entwicklung ist jedoch schwierig und eine manuelle Sicherheitsanalyse mühsam und fehleranfällig. Ein Mangel an exakten Sicherheitsbeweisen führt daher zu oft gravierenden Sicherheitsmängeln in vielen Protokollen. Um Datenschutz und Sicherheit kryptographischer Protokolle zu verbessern und deren Verifikation zu vereinfachen, konzentriert sich ein Großteil der Forschung auf formale Protokollanalyse. Dies führte zur Entwicklung automatischer Tools, die auf symbolischen Kryptographie-Abstraktionen basieren. Jedoch gibt es weiterhin zahlreiche Protokolle und Sicherheitseigenschaften, deren Analyse zu komplex für aktuelle Systeme ist. Diese Dissertation stellt drei neuartige Frameworks zur Verifikation von Sicherheitsprotokollen und ihren Implementierungen vor. Sie nutzen eine leistungsstarker Typisierung für Sicherheit und Datenschutz und verbessern damit die aktuelle, Beschränkungen unterworfene Situation. Mit AF7 präsentieren wir die erste statische Typisierung von Protokollimplementierungen bezüglich Sicherheitseigenschaften, die in affiner Logik formuliert sind. Zudem sorgt unsere neuartige typbasierte, automatische Analysetechnik von elektronischen Wahlsystemen für Datenschutz und Überprüfbarkeit im Wahlprozess. Schließlich stellen wir mit DF7 das erste affine Typsystem zur statischen, automatischen Verifikation der sogenannten Distributed Differential Privacy in Protokollimplementierungen vor.

Cryptographic protocols are ubiquitous in the modern web. However, they are notoriously difficult to design and their manual security analysis is both tedious and error-prone. Due to the lack of rigorous security proofs, many protocols have been discovered to be flawed. To improve the security and privacy guarantees of cryptographic protocols and their implementations and to facilitate their verification, a lot of research has been directed towards the formal analysis of such protocols. This has led to the development of several automated tools based on symbolic abstractions of cryptography. Unfortunately, there are still various cryptographic protocols and properties that are out of the scope of current systems. This thesis introduces three novel frameworks for the verification of security protocols and their implementations based on powerful types for security and privacy, overcoming the limitations of current state-of-the-art approaches. With AF7 we present the first type system that statically enforces the safety of cryptographic protocol implementations with respect to authorization policies expressed in affine logic. Furthermore, our novel approach for the automated analysis of e-voting systems based on refinement type systems can be used to enforce both privacy and verifiability. Finally, with DF7, we present the first affine, distanceaware type system to statically and automatically enforce distributed differential privacy in cryptographic protocol implementations.