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 |
Alternativtitel: | Disjunktive, konjunktive, und Verfeinerungstypen und die Beweisführung der Disjunktheit von Typen für die Analyse von Sicherheitsprotokollen |
VerfasserIn: | Hritcu, Catalin |
Sprache: | Englisch |
Erscheinungsjahr: | 2012 |
Kontrollierte 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 |
Dokumenttyp: | Dissertation |
Abstract: | 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 |
Datum des Eintrags: | 29-Mär-2012 |
Fakultät: | MI - Fakultät für Mathematik und Informatik |
Fachrichtung: | MI - Informatik |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
catalin_phd_2012_03_24_final.pdf | 1,2 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.