Please use this identifier to cite or link to this item: doi:10.22028/D291-26640
Title: Abstracting cryptographic protocols
Other Titles: Die Abstraktion kryptographischer Protokolle
Author(s): Mohammadi, Esfandiar
Language: English
Year of Publication: 2014
SWD key words: Kryptologie
Dechiffrierung
Informationsloses Beweissystem
Kommunikationsprotokoll
Schlüsselaustauschprotokoll
Free key words: computational soundness
Tor
anonymous communication
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
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.
Link to this record: urn:nbn:de:bsz:291-scidok-63333
hdl:20.500.11880/26696
http://dx.doi.org/10.22028/D291-26640
Advisor: Backes, Michael
Date of oral examination: 29-Jun-2015
Date of registration: 8-Jan-2016
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 
final_version.pdf2,53 MBAdobe PDFView/Open


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