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 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.
This work was in part funded by the European Community’s Seventh Framework Programme (FP7) under grant agreement no. 216499. The compiler can be found at http://zkc.cace-project.eu , and a full version of this paper is given in [1].
Chapter PDF
Similar content being viewed by others
References
Almeida, J., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, A.R., Schneider, T.: A certifying compiler for zero-knowledge proofs of knowledge based on Σ-protocols. Cryptology ePrint Archive, Report 2010/339 (2010)
Bellare, M., Goldreich, O.: On defining proofs of knowledge. In: Brickell, E.F. (ed.) CRYPTO 1992. LNCS, vol. 740, pp. 390–420. Springer, Heidelberg (1993)
Han, W., Chen, K., Zheng, D.: Receipt-freeness for Groth e-voting schemes. Journal of Information Science and Engineering 25, 517–530 (2009)
Kikuchi, H., Nagai, K., Ogata, W., Nishigaki, M.: Privacy-preserving similarity evaluation and application to remote biometrics authentication. Soft Computing 14, 529–536 (2010)
Camenisch, J.: Group Signature Schemes and Payment Systems Based on the Discrete Logarithm Problem. PhD thesis, ETH Zurich, Konstanz (1998)
Camenisch, J., Michels, M.: Proving in zero-knowledge that a number is the product of two safe primes. In: Stern, J. (ed.) EUROCRYPT 1999. LNCS, vol. 1592, pp. 107–122. Springer, Heidelberg (1999)
Brands, S.: Untraceable off-line cash in wallet with observers. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 302–318. Springer, Heidelberg (1994)
Lindell, Y., Pinkas, B., Smart, N.P.: Implementing two-party computation efficiently with security against malicious adversaries. In: Ostrovsky, R., De Prisco, R., Visconti, I. (eds.) SCN 2008. LNCS, vol. 5229, pp. 2–20. Springer, Heidelberg (2008)
Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: ACM CCS 2004, pp. 132–145. ACM Press, New York (2004)
Camenisch, J., Herreweghen, E.V.: Design and implementation of the idemix anonymous credential system. In: ACM CCS 2002, pp. 21–30. ACM Press, New York (2002)
Kunz-Jacques, S., Martinet, G., Poupard, G., Stern, J.: Cryptanalysis of an efficient proof of knowledge of discrete logarithm. In: Yung, M., Dodis, Y., Kiayias, A., Malkin, T.G. (eds.) PKC 2006. LNCS, vol. 3958, pp. 27–43. Springer, Heidelberg (2006)
Bangerter, E., Camenisch, J., Maurer, U.: Efficient proofs of knowledge of discrete logarithms and representations in groups with hidden order. In: Vaudenay, S. (ed.) PKC 2005. LNCS, vol. 3386, pp. 154–171. Springer, Heidelberg (2005)
Schnorr, C.: Efficient signature generation by smart cards. Journal of Cryptology 4, 161–174 (1991)
Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 129–140. Springer, Heidelberg (1992)
Camenisch, J., Lysyanskaya, A.: An efficient system for non-transferable anonymous credentials with optional anonymity revocation. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol. 2045, pp. 93–118. Springer, Heidelberg (2001)
Lipmaa, H.: On diophantine complexity and statistical zeroknowledge arguments. In: Laih, C.-S. (ed.) ASIACRYPT 2003. LNCS, vol. 2894, pp. 398–415. Springer, Heidelberg (2003)
Paulson, L.: Isabelle: a Generic Theorem Prover. Volume 828 of LNCS. Springer (1994)
MacKenzie, P., Oprea, A., Reiter, M.K.: Automatic generation of two-party computations. In: ACM CCS 2003, pp. 210–219. ACM, New York (2003)
Malkhi, D., Nisan, N., Pinkas, B., Sella, Y.: Fairplay — a secure two-party computation system. In: USENIX Security 2004 (2004)
Damgård, I., Geisler, M., Krøigaard, M., Nielsen, J.B.: Asynchronous multiparty computation: Theory and implementation. In: Jarecki, S., Tsudik, G. (eds.) Public Key Cryptography – PKC 2009. LNCS, vol. 5443, pp. 160–179. Springer, Heidelberg (2009)
Briner, T.: Compiler for zero-knowledge proof-of-knowledge protocols. Master’s thesis, ETH Zurich (2004)
Camenisch, J., Rohe, M., Sadeghi, A.R.: Sokrates - a compiler framework for zero-knowledge protocols. In: WEWoRC 2005 (2005)
Bangerter, E., Camenisch, J., Krenn, S., Sadeghi, A.R., Schneider, T.: Automatic generation of sound zero-knowledge protocols. Cryptology ePrint Archive, Report 2008/471, Poster Session of EUROCRYPT 2009 (2008)
Bangerter, E., Briner, T., Heneka, W., Krenn, S., Sadeghi, A.R., Schneider, T.: Automatic generation of Σ-protocols. In: EuroPKI 2009 (to appear, 2009)
Bangerter, E., Krenn, S., Sadeghi, A.R., Schneider, T., Tsay, J.K.: On the design and implementation of efficient zero-knowledge proofs of knowledge. In: Software Performance Enhancements for Encryption and Decryption and Cryptographic Compilers – SPEED-CC 2009, October 12-13 (2009)
Meiklejohn, S., Erway, C., Küpçü, A., Hinkle, T., Lysyanskaya, A.: ZKPDL: A language-based system for efficient zero-knowledge proofs and electronic cash. In: USENIX 10 (to appear, 2010)
Rivest, R., Shamir, A., Adleman, L.: A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM 21, 120–126 (1978)
Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: IEEE Symposium on Security and Privacy – SP 2008, pp. 202–215. IEEE, Los Alamitos (2008)
Baskar, A., Ramanujam, R., Suresh, S.P.: A dolev-yao model for zero knowledge. In: Datta, A. (ed.) ASIAN 2009. LNCS, vol. 5913, pp. 137–146. Springer, Heidelberg (2009)
Blanchet, B.: ProVerif: Cryptographic protocol verifier in the formal model (2010)
Backes, M., Hritcu, C., Maffei, M.: Type-checking zero-knowledge. In: ACM CCS 2008, pp. 357–370. ACM, New York (2008)
Backes, M., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs against active attackers. In: IEEE Computer Security Foundations Symposium - CSF 2008, 255–269 Preprint on IACR ePrint 2008/152 (2008)
Barthe, G., Hedin, D., Zanella Béguelin, S., Grégoire, B., Heraud, S.: A machine-checked formalization of Σ-protocols. In: 23rd IEEE Computer Security Foundations Symposium, CSF 2010, IEEE, Los Alamitos (2010)
Barthe, G., Grégoire, B., Béguelin, S.: Formal certification of code-based cryptographic proofs. In: ACM SIGPLAN-SIGACT POPL 2009, pp. 90–101 (2009)
Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005)
Bhargavan, K., Fournet, C., Gordon, A., Tse, S.: Verified interoperable implementations of security protocols. ACM Trans. Program. Lang. Syst. 31(1), 1–61 (2008)
Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: ACM CCS 2008, pp. 459–468. ACM, New York (2008)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Workshop on Computer Security Foundations – CSFW 2001, p. 82. IEEE, Los Alamitos (2001)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy – SP 2006, pp. 140–154. IEEE, Los Alamitos (2006)
Camenisch, J., Stadler, M.: Efficient group signature schemes for large groups (extended abstract). In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol. 1294, pp. 410–424. Springer, Heidelberg (1997)
Cramer, R.: Modular Design of Secure yet Practical Cryptographic Protocols. PhD thesis, CWI and University of Amsterdam (1997)
Damgård, I.: On Σ-protocols, Lecture on Cryptologic Protocol Theory, Faculty of Science, University of Aarhus (2004)
Guillou, L., Quisquater, J.J.: A “paradoxical” identity-based signature scheme resulting from zero-knowledge. In: Goldwasser, S. (ed.) CRYPTO 1988. LNCS, vol. 403, pp. 216–231. Springer, Heidelberg (1990)
Cramer, R., Shoup, V.: A practical public key cryptosystem provably secure against adaptive chosen ciphertext attack. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 13–25. Springer, Heidelberg (1998)
Fujisaki, E., Okamoto, T.: Statistical zero knowledge protocols to prove modular polynomial relations. In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol. 1294, pp. 16–30. Springer, Heidelberg (1997)
Damgård, I., Fujisaki, E.: A statistically-hiding integer commitment scheme based on groups with hidden order. In: Zheng, Y. (ed.) ASIACRYPT 2002. LNCS, vol. 2501, pp. 77–85. Springer, Heidelberg (2002)
Bangerter, E.: Efficient Zero-Knowledge Proofs of Knowledge for Homomorphisms. PhD thesis, Ruhr-University Bochum (2005)
Smart, N.P. (ed.): Final Report on Unified Theoretical Framework of Efficient Zero-Knowledge Proofs of Knowledge. CACE project deliverable (2009)
Cramer, R., Damgård, I., Schoenmakers, B.: Proofs of partial knowledge and simplified design of witness hiding protocols. In: Desmedt, Y.G. (ed.) CRYPTO 1994. LNCS, vol. 839, pp. 174–187. Springer, Heidelberg (1994)
Shamir, A.: How to share a secret. Communications of the ACM 22, 612–613 (1979)
Fiat, A., Shamir, A.: How to prove yourself: practical solutions to identification and signature problems. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol. 263, pp. 186–194. Springer, Heidelberg (1987)
Brands, S.: Rapid demonstration of linear relations connected by boolean operators. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 318–333. Springer, Heidelberg (1997)
Bresson, E., Stern, J.: Proofs of knowledge for non-monotone discrete-log formulae and applications. In: Chan, A.H., Gligor, V.D. (eds.) ISC 2002. LNCS, vol. 2433, pp. 272–288. Springer, Heidelberg (2002)
Granlund, T.: The GNU MP Bignum Library (2010), http://gmplib.org/
Nipkow, T., Paulson, L.: Isabelle (2010), http://isabelle.in.tun.de
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Ballarin, C., Kammüller, F., Paulson, L.: The Isabelle/HOL Algebra Library (2008), http://isabelle.in.tum.de/library/HOL/HOL-Algebra/document.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Almeida, J.B., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, AR., Schneider, T. (2010). A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Σ-Protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds) Computer Security – ESORICS 2010. ESORICS 2010. Lecture Notes in Computer Science, vol 6345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15497-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-15497-3_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15496-6
Online ISBN: 978-3-642-15497-3
eBook Packages: Computer ScienceComputer Science (R0)