@conference {DBLP:conf/esorics/AlmeidaBBKSS10,
	title = {A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols},
	booktitle = {European Symposium on Research in Computer Security - ESORICS},
	year = {2010},
	month = {September},
	pages = {151-167},
	address = {Saint Malo, France},
	abstract = {<p>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.<br />
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.</p>
},
	url = {http://dx.doi.org/10.1007/978-3-642-15497-3_10},
	attachments = {https://haslab.uminho.pt/sites/default/files/jba/files/10esorics.pdf},
	author = {Jos{\'e} Bacelar Almeida and Endre Bangerter and Manuel Bernardo Barbosa and Stephan Krenn and Ahmad Reza Sadeghi and Thomas Schneider}
}