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.

Rezumat:

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

URL: http://www.infsec.cs.uni-saarland.de/~hritcu/publications/rcf-and-or-coq-tosca2011-post.pdf