English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis

MPS-Authors
/persons/resource/persons44646

Hritcu,  Catalin
International Max Planck Research School, MPI for Informatics, Max Planck Society;

Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Hritcu, C. (2012). Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD Thesis, Universität des Saarlandes, Saarbrücken. doi:10.22028/D291-26373.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0027-9EFA-D
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. The two
type systems combine prior work on renement 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 typebased 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.