A Dolev-Yao model for Zero Knowledge
Chennai Mathematical Institute
We propose an extension of the standard Dolev-Yao model of cryptographic protocols to facilitate symbolic reasoning about zero- knowledge proofs. This is accomplished by communicating typed terms, and providing a proof amounts to certifying that a term is of a particular type. We present a proof system for term derivability, which is employed to yield a decision procedure for checking whether a given protocol meets its zero knowledge speciﬁcation.