Paper 2010/339

A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on $\Sigma$-Protocols

Jose Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, and Thomas Schneider


Zero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have very useful properties, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation is time-consuming and error-prone. We contribute to overcoming these challenges as follows: We present a comprehensive specification language and a certifying compiler for ZK-PoK protocols based on $\Sigma$-protocols and composition techniques known in literature. The compiler allows the fully automatic translation of an abstract description of a proof goal into an executable implementation. Moreover, the compiler overcomes various restrictions of previous approaches, e.g., it supports the important class of exponentiation homomorphisms with hidden-order co-domain, needed for privacy-preserving applications such as idemix. Finally, our compiler is certifying, in the sense that it automatically produces a formal proof of security (soundness) of the compiled protocol (currently covering special homomorphisms) using the Isabelle/HOL theorem prover.

Available format(s)
Publication info
Published elsewhere. An extended abstract of this work will be presented at ESORICS 2010
Zero-KnowledgeProtocol CompilerFormal Verification
Contact author(s)
stephan krenn @ bfh ch
thomas schneider @ trust rub de
2010-08-04: last of 3 revisions
2010-06-13: received
See all versions
Short URL
Creative Commons Attribution


      author = {Jose Bacelar Almeida and Endre Bangerter and Manuel Barbosa and Stephan Krenn and Ahmad-Reza Sadeghi and Thomas Schneider},
      title = {A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on $\Sigma$-Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2010/339},
      year = {2010},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.