Paper 2012/258

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols

José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, and Santiago Zanella Béguelin


Developers building cryptography into security-sensitive applications face a daunting task. Not only must they understand the security guarantees delivered by the constructions they choose, they must also implement and combine them correctly and efficiently. Cryptographic compilers free developers from having to implement cryptography on their own by turning high-level specifications of security goals into efficient implementations. Yet, trusting such tools is risky as they rely on complex mathematical machinery and claim security properties that are subtle and difficult to verify. In this paper, we present ZKCrypt, an optimizing cryptographic compiler that achieves an unprecedented level of assurance without sacrificing practicality for a comprehensive class of cryptographic protocols, known as Zero-Knowledge Proofs of Knowledge. The pipeline of ZKCrypt tightly integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage in the pipeline, ZKCrypt provides assurance that the implementation it outputs securely realizes the high-level proof goal given as input. We report on the main characteristics of ZKCrypt, highlight new definitions and concepts at its foundations, and illustrate its applicability through a representative example of an anonymous credential system.

Note: Added material on latest developments in the compiler.

Available format(s)
Publication info
Published elsewhere. Unknown where it was published
zero-knowledgecryptographic compilercertifying compilerformal verification
Contact author(s)
santiago @ microsoft com
2012-06-29: last of 3 revisions
2012-05-09: received
See all versions
Short URL
Creative Commons Attribution


      author = {José Bacelar Almeida and Manuel Barbosa and Endre Bangerter and Gilles Barthe and Stephan Krenn and Santiago Zanella Béguelin},
      title = {Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2012/258},
      year = {2012},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.