Full proof cryptography: Verifiable compilation of efficient zero-knowledge protocols Conference Paper

Author(s): Almeida, José Bacelar; Barbosa, Manuel; Bangerter, Endre; Barthe, Gilles; Krenn, Stephan; Béguelin, Santiago Zanella
Title: Full proof cryptography: Verifiable compilation of efficient zero-knowledge protocols
Affiliation IST Austria
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 this task 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 achieving 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 integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage, ZKCrypt provides assurance that the output implementation securely realizes the abstract 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.
Keywords: Zero-Knowledge; Cryptographic compiler; verifying compilation
Conference Title: CCS: Computer and Communications Security
Conference Dates: October 16-18, 2012
Conference Location: Raleigh, NC, USA
ISBN: 978-145031650-7
Publisher: ACM  
Date Published: 2012-01-01
Start Page: 488
End Page: 500
DOI: 10.1145/2382196.2382249
Notes: This work was partially funded by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project ENI-AC/2224/2009, by ENIAC Joint Undertaking under grant agreement number 120224, European Projects FP7-256980 NESSoS and FP7-229599 AMAROUT, Spanish National project TIN2009-14599 DESAFIOS 10, and Madrid Regional project S2009TIC-1465 PROMETIDOS.
Open access: yes (repository)
IST Austria Authors
  1. Stephan Krenn
    11 Krenn
Related IST Austria Work