Please use this identifier to cite or link to this item: doi:10.22028/D291-26373
Title: Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis
Other Titles: Disjunktive, konjunktive, und Verfeinerungstypen und die Beweisführung der Disjunktheit von Typen für die Analyse von Sicherheitsprotokollen
Author(s): Hritcu, Catalin
Language: English
Year of Publication: 2012
SWD key words: Sicherheitsprotokoll
Programmiersprache
Lambda-Kalkül
Typ
Verifikation
Analyse
Informationsloses Beweissystem
Beweis
Pi-Kalkül
Free key words: Typsystem
Protokollanalyse
Disjunktive und konjunktive Typen
Zero-Knowledge-Beweise
Protokollimplementierungen
type systems
security protocols
zero-knowledge proofs
verification
lambda calculus
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
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 to this record: urn:nbn:de:bsz:291-scidok-48000
hdl:20.500.11880/26429
http://dx.doi.org/10.22028/D291-26373
Advisor: Backes, Michael
Date of oral examination: 10-Jan-2012
Date of registration: 29-Mar-2012
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 
catalin_phd_2012_03_24_final.pdf1,2 MBAdobe PDFView/Open


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