International Association
for Cryptologic Research

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 hard 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.