A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols Conference Paper


Author(s): Almeida, José Bacelar; Bangerter, Endre; Barbosa, Manuel; Krenn, Stephan; Sadeghi, Ahmad-Reza; Schneider, Thomas
Editor(s): Gritzalis, Dimitris; Preneel, Bart; Theoharidou, Marianthi
Title: A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols
Title Series: LNCS
Affiliation
Abstract: Zero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have a high potential impact, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation are time-consuming and error-prone. We contribute to overcoming these challenges as follows: We present a comprehensive specification language and a compiler for ZK-PoK protocols based on Σ-protocols. 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 DAA. Finally, our compiler is certifying, in the sense that it automatically produces a formal proof of the soundness of the compiled protocol for a large class of protocols using the Isabelle/HOL theorem prover.
Keywords: Formal verification; Zero-Knowledge; Protocol Compiler
Conference Title: ESORICS: European Symposium on Research in Computer Security
Volume: 6345
Conference Dates: September 20-22, 2010
Conference Location: Athens, Greece
Publisher: Springer  
Date Published: 2010-08-30
Start Page: 151
End Page: 167
Sponsor: This work was in part funded by the European Community's Seventh Framework Programme (FP7) under grant agreement no. 216499.
URL:
DOI: 10.1007/978-3-642-15497-3
Notes: A preliminary version of the compiler can be found at http://zkc.cace-project.eu.
Open access: yes (repository)
IST Austria Authors
  1. Stephan Krenn
    11 Krenn
Related IST Austria Work