A Dolev-Yao Model for Zero Knowledge

In cryptographic protocols, zero knowledge proofs are employed for a principal A to communicate some non-trivial information t to B while at the same time ensuring that B cannot derive any information "stronger" than t. Oen this implies that B can verify that some property holds without being able to produce a proof of this. While a rich theory of zero knowledge proofs exists, there are few formal models addressing verification questions. We propose an extension of the standard Dolev-Yao model of cryptographic protocols which involves not only constructibility of terms but also a form of verifiability. 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 specification.

• Type: Conference
• Year: 2009
• Where: ASIAN
• Authors: Anguraj Baskar, Ramaswamy Ramanujam, S. P. Suresh
• Keywords: Algorithms, ASIAN 2009, Cryptographic Protocols, Models Addressing Verification, Zero Knowledge Proofs