A certifying compiler for zero-knowledge proofs of knowledge based on sigma-pro...

• Author(s): Almeida, José Bacelar ; Bangerter, Endre ; Barbosa, Manuel Bernardo ; Krenn, Stephan ; Sadeghi, Ahmad-Reza ; Schneider, Thomas
• Date: 2012
• Persistent ID: http://hdl.handle.net/1822/19403
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Zero-knowledge; Protocol compiler; Formal verification
• Document Type: Article
• Language: English

Description

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.