SciDok

Eingang zum Volltext in SciDok

Lizenz

Dissertation zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-48000
URL: http://scidok.sulb.uni-saarland.de/volltexte/2012/4800/


Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis

Disjunktive, konjunktive, und Verfeinerungstypen und die Beweisführung der Disjunktheit von Typen für die Analyse von Sicherheitsprotokollen

Hritcu, Catalin

pdf-Format:
Dokument 1.pdf (1.201 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Sicherheitsprotokoll , Programmiersprache , Lambda-Kalkül , Typ , Verifikation , Analyse , Informationsloses Beweissystem , Beweis , Pi-Kalkül
Freie Schlagwörter (Deutsch): Typsystem , Protokollanalyse , Disjunktive und konjunktive Typen , Zero-Knowledge-Beweise , Protokollimplementierungen
Freie Schlagwörter (Englisch): type systems , security protocols , zero-knowledge proofs , verification , lambda calculus
Institut: Fachrichtung 6.2 - Informatik
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Hauptberichter: Backes, Michael (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 10.01.2012
Erstellungsjahr: 2012
Publikationsdatum: 29.03.2012
Kurzfassung auf Englisch: 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.
Kurzfassung auf Deutsch: 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.
Lizenz: Veröffentlichungsvertrag für Dissertationen und Habilitationen

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English