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 17 min ago

13 hours 44 min ago

15 hours 46 min ago

18 hours 34 min ago

18 hours 56 min ago

19 hours 40 min ago

20 hours 35 min ago

20 hours 37 min ago

21 hours 10 min ago

22 hours 36 min ago