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

5 hours 40 min ago

1 day 5 hours ago

1 day 22 hours ago

2 days 8 hours ago

4 days 4 hours ago

4 days 9 hours ago

4 days 20 hours ago

4 days 20 hours ago

1 week 1 day ago

1 week 1 day ago