Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26373
Titel: Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis
Sonstige Titel: Disjunktive, konjunktive, und Verfeinerungstypen und die Beweisführung der Disjunktheit von Typen für die Analyse von Sicherheitsprotokollen
Verfasser: Hritcu, Catalin
Sprache: Englisch
Erscheinungsjahr: 2012
SWD-Schlagwörter: Sicherheitsprotokoll
Programmiersprache
Lambda-Kalkül
Typ
Verifikation
Analyse
Informationsloses Beweissystem
Beweis
Pi-Kalkül
Freie Schlagwörter: Typsystem
Protokollanalyse
Disjunktive und konjunktive Typen
Zero-Knowledge-Beweise
Protokollimplementierungen
type systems
security protocols
zero-knowledge proofs
verification
lambda calculus
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: In this thesis we present two new type systems for verifying the security of cryptographic protocol models expressed in a spi-calculus and, respectively, of protocol implementations expressed in a concurrent lambda calculus. In this thesis we present two new type systems for verifying the security of cryptographic protocol models expressed in a spi-calculus and, respectively, of protocol implementations expressed in a concurrent lambda calculus. The two type systems combine prior work on refinement types with union and intersection types and with the novel ability to reason statically about the disjointness of types. The increased expressivity enables the analysis of important protocol classes that were previously out of scope for the type-based analyses of cryptographic protocols. In particular, our type systems can statically analyze protocols that are based on zero-knowledge proofs, even in scenarios when certain protocol participants are compromised. The analysis is scalable and provides security proofs for an unbounded number of protocol executions. The two type systems come with mechanized proofs of correctness and efficient implementations.
In dieser Arbeit werden zwei neue Typsysteme vorgestellt, mit denen die Sicherheit kryptographischer Protokolle, modelliert in einem spi-Kalkül, und Protokollimplementierungen, beschrieben in einem nebenläufigen Lambdakalkül, verifiziert werden kann. Die beiden Typsysteme verbinden vorausgehende Arbeiten zu Verfeinerungstypen mit disjunktiven und konjunktiven Typen, und ermöglichen außerdem, statisch zu folgern, dass zwei Typen disjunkt sind. Die Ausdrucksstärke der Systeme erlaubt die Analyse wichtiger Klassen von Protokollen, die bisher nicht durch typbasierte Protokollanalysen behandelt werden konnten. Insbesondere ist mit den vorgestellten Typsystemen auch die statische Analyse von Protokollen möglich, die auf Zero-Knowledge-Beweisen basieren, selbst unter der Annahme, dass einige Protokollteilnehmer korrumpiert sind. Die Analysetechnik skaliert und erlaubt Sicherheitsbeweise für eine unbeschränkte Anzahl von Protokollausführungen. Die beiden Typsysteme sind formal korrekt bewiesen und effizient implementiert.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-48000
hdl:20.500.11880/26429
http://dx.doi.org/10.22028/D291-26373
Erstgutachter: Backes, Michael
Tag der mündlichen Prüfung: 10-Jan-2012
SciDok-Publikation: 29-Mär-2012
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 
catalin_phd_2012_03_24_final.pdf1,2 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.