Home

Type-Checking Zero Knowledge

Type-Checking Zero Knowledge

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.

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.

By Paul Snively at 2008-11-18 06:18 | Functional | Implementation | Type Theory | other blogs | 13619 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Interesting, but...

Sadly, I've been too busy lately to give this more than a quick scan over the past week, but what I've seen is at least interesting enough for me to stick it in my "read thoroughly when there's time" folder. I just wonder, however, if this isn't yet another piece of work laden with the sorts of problems Neal Koblitz discusses in his critique of automated therom provers for cryptography from last year.

It certainly seems (given my shallow reading) to suffer from the forest-for-the-trees aspect in that it doesn't prove the ZKP to be correct, sound, and robust, but rather that the protocol doesn't leak any information to the verifier, assuming that all of the crypto surrounding the protocol is secure; this is of course a huge assumption.

It's also hard to see just how useful such a type-checker can be, as the kind of checks that it seems to be doing are the kind of things that seemed to follow, for free, from the proofs done on the math outside of the communication. It would have been nice to see some examples where the type-checker uncovers a faulty ZKP protocol, where the flaw is not so obvious to a cryptographer who may be doing a security proof by hand.

Where this may have most value is as a part of a tool along the lines of Bangerter, Camenisch, Krenn, Sadeghi, and Schneider's recent Automatic Generation of Sound Zero-Knowledge Protocols. Which uses libraries of common techniques to compile a specification of a ZK Proof of Knowledge down to a sound implementation of the protocol, output either as Java code, or as detailed documentation in LaTeX.

By William D. Neumann at Wed, 2008-11-26 16:37 | login or register to post comments

Thank you for the reference

Thank you for the reference to the zero-knowledge compiler. Seems very interesting.

By Catalin Hritcu at Fri, 2008-12-05 14:52 | login or register to post comments