Computational soundness of symbolic zero-knowledge proofs

raction 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) zeroknowledge 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 zeroknowledge proof system. We prove that even in the presence of arbitrary active ...

• Type: Journal
• Year: 2010
• Where: JCS
• Authors: Michael Backes, Dominique Unruh
• Keywords: Core Cryptographic Operations, Cryptographic Operations, Dolev-Yao Models, JCS 2010