Inscriere cercetatori

Type-checking Zero-knowledge

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

Autori: Michael Backes, Catalin Hritcu, and Matteo Maffei

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


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

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