Autori: Michael Backes, Catalin Hritcu, and Matteo Maffei

Editorial: ACM Press, 15th ACM Conference on Computer and Communications Security (CCS 2008), 2008.

Rezumat:

This paper presents the first type system for statically analyzing security
protocols that are based on zero-knowledge proofs. We show how certain
properties offered by zero-knowledge proofs can be characterized in terms of
authorization policies and statically enforced by a type system. The analysis is
modular and compositional, and provides security proofs for an unbounded number
of protocol executions. We develop a new type-checker that conducts the analysis
in a fully automated manner. We exemplify the applicability of our technique to
real-world protocols by verifying the authenticity and secrecy properties of the
Direct Anonymous Attestation (DAA) protocol. The analysis of DAA takes less than three
seconds.

Cuvinte cheie: formal methods, language-based security, security protocols, type-systems, protocol verification, authentication, secrecy, zero-knowledge proofs

URL: http://www.infsec.cs.uni-sb.de/~hritcu/publications/zk-types-full.pdf