TY - THES
T1 - Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis
A1 - Hritcu,Catalin
Y1 - 2012/03/29
N2 - 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.
KW - Sicherheitsprotokoll
KW - Programmiersprache
KW - Lambda-Kalkül
KW - Typ
KW - Verifikation
KW - Analyse
KW - Informationsloses Beweissystem
KW - Beweis
KW - Pi-Kalkül
CY - Saarbrücken
PB - Saarländische Universitäts- und Landesbibliothek
AD - Postfach 151141, 66041 Saarbrücken
UR - http://scidok.sulb.uni-saarland.de/volltexte/2012/4800
ER -