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.
Category / Keywords: foundations / Computational soundness, formal methods, zero knowledge Publication Info: A short version appears at CSF 2008 Date: received 4 Apr 2008, last revised 10 Sep 2009 Contact author: unruh at mmci uni-saarland de Available format(s): PDF | BibTeX Citation 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.
Version: 20090910:162926 (All versions of this report) Short URL: ia.cr/2008/152