Type-checking zero-knowledge
- 27 October 2008
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 357-370
- https://doi.org/10.1145/1455770.1455816
Abstract
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.Keywords
This publication has 24 references indexed in Scilit:
- System Description: Spass Version 3.0Published by Springer Nature ,2007
- Formal analysis of Kerberos 5Theoretical Computer Science, 2006
- Pattern-matching spi-calculusInformation and Computation, 2006
- Timed Spi-Calculus with Types for Secrecy and AuthenticityPublished by Springer Nature ,2005
- Secrecy Despite Compromise: Types, Cryptography, and the Pi-CalculusPublished by Springer Nature ,2005
- A Type Discipline for Authorization PoliciesPublished by Springer Nature ,2005
- Analyzing security protocols with secrecy types and logic programsJournal of the ACM, 2005
- Secrecy by typing in security protocolsJournal of the ACM, 1999
- Rewrite-based Equational Theorem Proving with Selection and SimplificationJournal of Logic and Computation, 1994
- Blind Signatures for Untraceable PaymentsPublished by Springer Nature ,1983