Inscriere cercetatori

Site nou !

Daca nu va puteti recupera parola (sau aveti alte probleme), scrieti-ne la pagina de contact. Situl vechi se gaseste la adresa


Union and Intersection Types for Secure Protocol Implementations

Domenii publicaţii > Ştiinţe informatice + Tipuri publicaţii > Articol în volumul unei conferinţe

Autori: Michael Backes, Cãtãlin Hriţcu, Matteo Maffei

Editorial: Springer, Theory of Security and Applications (TOSCA'11), Invited paper, p.1-28, 2011.


We present a new type system for verifying the security of cryptographic protocol
implementations. The type system combines prior work on refinement types,
with union, intersection, and polymorphic 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 protocol implementations. In particular, our types can
statically characterize: (i) more usages of asymmetric cryptography, such as signatures
of private data and encryptions of authenticated data; (ii) authenticity and
integrity properties achieved by showing knowledge of secret data; (iii) applications
based on zero-knowledge proofs. The type system comes with a mechanized
proof of correctness and an efficient type-checker.

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