Type-Checking Zero Knowledge

This paper presents the ï¬rst 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.

A little dependent type theory, a little Pi calculus, a little cryptography... there's something for everyone! This is follow-up work to this story that Ehud posted.

The source code can be found here.

## Recent comments

9 hours 47 min ago

11 hours 56 min ago

19 hours 10 min ago

1 day 10 min ago

1 day 21 min ago

1 day 2 hours ago

1 day 9 hours ago

1 day 10 hours ago

1 day 13 hours ago

1 day 14 hours ago