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
1 week 21 hours ago
1 week 5 days ago
1 week 6 days ago
1 week 6 days ago
2 weeks 5 days ago
3 weeks 1 day ago
3 weeks 1 day ago
3 weeks 1 day ago
4 weeks 3 days ago
4 weeks 4 days ago