---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: José
      foaf_name: Almeida, José
      foaf_surname: Almeida
  - foaf_Person:
      foaf_givenName: Manuel
      foaf_name: Barbosa, Manuel
      foaf_surname: Barbosa
  - foaf_Person:
      foaf_givenName: Endre
      foaf_name: Bangerter, Endre
      foaf_surname: Bangerter
  - foaf_Person:
      foaf_givenName: Gilles
      foaf_name: Barthe, Gilles
      foaf_surname: Barthe
  - foaf_Person:
      foaf_givenName: Stephan
      foaf_name: Krenn, Stephan
      foaf_surname: Krenn
      foaf_workInfoHomepage: http://www.librecat.org/personId=329FCCF0-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0003-2835-9093
  - foaf_Person:
      foaf_givenName: Santiago
      foaf_name: Béguelin, Santiago
      foaf_surname: Béguelin
  bibo_doi: 10.1145/2382196.2382249
  dct_date: 2012^xs_gYear
  dct_language: eng
  dct_publisher: ACM@
  dct_title: 'Full proof cryptography: Verifiable compilation of efficient zero-knowledge
    protocols@'
...