Please use this identifier to cite or link to this item: doi:10.22028/D291-26965
Title: A theory of types for security and privacy
Author(s): Eigner, Fabienne Sophie
Language: English
Year of Publication: 2015
SWD key words: Typsystem
Computersicherheit
Formale Methode
Lineare Logik
Privatsphäre
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
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.
Link to this record: urn:nbn:de:bsz:291-scidok-ds-269653
hdl:20.500.11880/26909
http://dx.doi.org/10.22028/D291-26965
Advisor: Maffei, Matteo
Date of oral examination: 12-Dec-2016
Date of registration: 14-Dec-2017
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
eigner - thesis-final.pdf2,87 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.