Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26640
Titel: Abstracting cryptographic protocols
Sonstige Titel: Die Abstraktion kryptographischer Protokolle
Verfasser: Mohammadi, Esfandiar
Sprache: Englisch
Erscheinungsjahr: 2014
SWD-Schlagwörter: Kryptologie
Dechiffrierung
Informationsloses Beweissystem
Kommunikationsprotokoll
Schlüsselaustauschprotokoll
Freie Schlagwörter: computational soundness
Tor
anonymous communication
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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 zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-63333
hdl:20.500.11880/26696
http://dx.doi.org/10.22028/D291-26640
Erstgutachter: Backes, Michael
Tag der mündlichen Prüfung: 29-Jun-2015
SciDok-Publikation: 8-Jan-2016
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
final_version.pdf2,53 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.