A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on $\Sigma$-Protocols
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.
Automatic Generation of Sound Zero-Knowledge Protocols
Efficient zero-knowledge proofs of knowledge (ZK-PoK) are basic building blocks of many practical cryptographic applications such as identification schemes, group signatures, and secure multiparty computation. Currently, first applications that essentially rely on ZK-POKs are being deployed in the real world. The most prominent example is Direct Anonymous Attestation (DAA), which was adopted by the Trusted Computing Group (TCG) and implemented as one of the functionalities of the cryptographic chip Trusted Platform Module (TPM). Implementing systems using ZK-PoK turns out to be challenging, since ZK-PoK are, loosely speaking, significantly more complex than standard crypto primitives, such as encryption and signature schemes. As a result, implementation cycles of ZK-PoK are time-consuming and error-prone, in particular for developers with minor or no cryptographic skills. To overcome these challenges, we have designed and implemented a compiler with corresponding languages that given a high-level ZK-PoK protocol specification automatically generates a sound implementation of this. The output is given in form of $\Sigma$-protocols, which are the most efficient protocols for ZK-PoK currently known. Our compiler translates ZK-PoK protocol specifications, written in a high-level protocol description language, into Java code or \LaTeX\ documentation of the protocol. The compiler is based on a unified theoretical framework that encompasses a large number of existing ZK-PoK techniques. Within this framework we present a new efficient ZK-PoK protocol for exponentiation homomorphisms in hidden order groups. Our protocol overcomes several limitations of the existing proof techniques.
Sufficient Conditions for Computational Intractability Regarding Generic Algorithms
The generic group model is a valuable methodology for analyzing the computational hardness of the number-theoretic problems used in cryptography. Although generic hardness proofs exhibit many similarities, still the computational intractability of every newly introduced problem needs to be proven from scratch, a task that can easily become complicated and cumbersome when done rigorously. In this paper we make the first steps towards overcoming this problem by identifying verifiable criteria which if met by a cryptographic problem guarantee its hardness with respect to generic algorithms. As useful means for formalization of definitions and proofs we relate the concepts of generic algorithms and straight-line programs that have only been used independently in cryptography so far. The class of problems we cover includes a significant number of the cryptographic problems currently known, and is general enough to also include many future problems. Moreover, we strengthen the conventional generic model by incorporating a broader class of possible oracles (operations) since the underlying algebraic groups may possibly be related through mappings such as isomorphisms, homomorphisms or multilinear maps. Our approach could serve as an appropriate basis for tool-aided hardness verification in the generic model.