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 privacypreserving 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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Almeida, J. B., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, A. R., & Schneider, T. (2010). A certifying compiler for zero-knowledge proofs of knowledge based on ∑-protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6345 LNCS, pp. 151–167). Springer Verlag. https://doi.org/10.1007/978-3-642-15497-3_10
Mendeley helps you to discover research relevant for your work.