Paper 2008/152

Computational soundness of symbolic zero-knowledge proofs

Michael Backes and Dominique Unruh


The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev-Yao models offering the core cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Recent work, however, has started to extend Dolev-Yao models to more sophisticated operations with unique security features. Zero-knowledge proofs arguably constitute the most amazing such extension. In this paper, we first identify which additional properties a cryptographic (non-interactive) zero-knowledge proof needs to fulfill in order to serve as a computationally sound implementation of symbolic (Dolev-Yao style) zero-knowledge proofs; this leads to the novel definition of a symbolically-sound zero-knowledge proof system. We prove that even in the presence of arbitrary active adversaries, such proof systems constitute computationally sound implementations of symbolic zero-knowledge proofs. This yields the first computational soundness result for symbolic zero-knowledge proofs and the first such result against fully active adversaries of Dolev-Yao models that go beyond the core cryptographic operations.

Note: 2008-04-08: Original version 2008-04-17: Minor corrections 2008-06-24: The definition of symbolically-sound zero-knowledge was missing a condition: length-regularity. This revision adds that condition. 2008-09-10: Complete overhaul. Strongly extended proofs.

Available format(s)
Publication info
Published elsewhere. A short version appears at CSF 2008
Computational soundnessformal methodszero knowledge
Contact author(s)
unruh @ mmci uni-saarland de
2009-09-10: last of 3 revisions
2008-04-08: received
See all versions
Short URL
Creative Commons Attribution


      author = {Michael Backes and Dominique Unruh},
      title = {Computational soundness of symbolic zero-knowledge proofs},
      howpublished = {Cryptology ePrint Archive, Paper 2008/152},
      year = {2008},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.