Cryptology ePrint Archive: Report 2012/258

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

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

Abstract: 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.

Category / Keywords: implementation / zero-knowledge, cryptographic compiler, certifying compiler, formal verification

Date: received 7 May 2012, last revised 29 Jun 2012

Contact author: santiago at microsoft com

Available format(s): PDF | BibTeX Citation

Note: Added material on latest developments in the compiler.

Version: 20120629:101510 (All versions of this report)

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]