Premiile Ad Astra
Revista Ad Astra
Biblioteca de știință
Cartea albă
Topul universităților
Who's who
Publicații
Teze și dizertații
Asociația Ad Astra
 
Comunicate
Știri
Evenimente
Oportunități de finanțare
 
Login
Înregistrare
 
>> English
 
   
 

Catalin Hritcu. Union, Intersection, and Re nement Types and Reasoning About Type Disjointness for Security Protocol Analysis. 2012.

Rezumat: 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 re nement 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 ecient implementations.

Cuvinte cheie: type systems , security protocols , zero-knowledge proofs , verification , lambda calculus

URL: http://scidok.sulb.uni-saarland.de/volltexte/2012/4800/pdf/catalin_phd_2012_03_24_final.pdf

Adăugată pe site de Catalin Hritcu

Înapoi

   
© Ad Astra 2001-2013