Paper 2012/081

Computational Soundness of Symbolic Zero-knowledge Proofs: Weaker Assumptions and Mechanized Verification

Michael Backes, Fabian Bendun, and Dominique Unruh


The abstraction of cryptographic operations by term algebras, called symbolic models, is essential in almost all tool-supported methods for analyzing security protocols. Significant progress was made in proving that symbolic models offering basic cryptographic operations such as encryption and digital signatures can be sound with respect to actual crypto- graphic realizations and security definitions. Even abstractions of sophisticated modern cryptographic primitives such as zero- knowledge (ZK) proofs were shown to have a computationally sound cryptographic realization, but only in ad-hoc formalisms and at the cost of placing strong assumptions on the underlying cryptography, which leaves only highly inefficient realizations. In this paper, we make two contributions to this problem space. First, we identify weaker cryptographic assumptions that we show to be sufficient for computational soundness of symbolic ZK proofs. These weaker assumptions are fulfilled by existing efficient ZK schemes as well as generic ZK constructions. Second, we conduct all computational soundness proofs in CoSP, a recent framework that allows for casting com- putational soundness proofs in a modular manner, independent of the underlying symbolic calculi. Moreover, all computational soundness proofs conducted in CoSP automatically come with mechanized proof support through an embedding of the applied $\pi$-calculus.

Available format(s)
Publication info
Published elsewhere. Unknown where it was published
symbolic zero-knowledgecomputational soundnessweaker assumptionsmechanized proofs
Contact author(s)
bendun @ cs uni-saarland de
2012-02-23: received
Short URL
Creative Commons Attribution


      author = {Michael Backes and Fabian Bendun and Dominique Unruh},
      title = {Computational Soundness of Symbolic Zero-knowledge Proofs: Weaker Assumptions and Mechanized Verification},
      howpublished = {Cryptology ePrint Archive, Paper 2012/081},
      year = {2012},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.