Type-checking zero-knowledge

This paper presents the first type system for statically analyzing security protocols that are based on zero-knowledge proofs. We show how several 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 and of our type-checker to real-world protocols by verifying the authenticity properties of the Direct Anonymous Attestation (DAA) protocol. The analysis of DAA takes less than three seconds.

• Type: Conference
• Year: 2008
• Where: CCS
• Authors: Michael Backes, Catalin Hritcu, Matteo Maffei
• Keywords: CCS 2008, Security Privacy, Security Protocols, Type System, Zero-knowledge Proofs