Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

José Bacelar Almeida; Manuel Barbosa; Manuel L Correia; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco; Vitor Pereira

Paper 2021/1149

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

José Bacelar Almeida, Manuel Barbosa, Manuel L Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, and Vitor Pereira

Abstract

MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero- knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of this transformation. We begin with an EasyCrypt formalization that preserves modular structure of the original MitH construction and can be instantiated with arbitrary MPC protocols, secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first approach realizes a fully automated extraction from EasyCrypt to OCaml. The second one reduces the trusted computing base (TCB) and provides better performance for the extracted executable by combining code extraction with manual formal verification of low-level components implemented in the Jasmin language. We conclude the paper with a discussion of the trade-off between formal verification effort and performance, and also discuss how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. Minor revision. ACM CCS 2021
DOI: 10.1145/3460120.3484771
Keywords: Zero-Knowledge Secure Multiparty Computation Formal Verification
Contact author(s): hpacheco @ fc up pt
mbb @ fc up pt
jba @ di uminho pt
vitor pereira @ sri com
History: 2021-09-15: revised; 2021-09-10: received; See all versions
Short URL: https://ia.cr/2021/1149
License: CC BY

BibTeX

@misc{cryptoeprint:2021/1149,
      author = {José Bacelar Almeida and Manuel Barbosa and Manuel L Correia and Karim Eldefrawy and Stéphane Graham-Lengrand and Hugo Pacheco and Vitor Pereira},
      title = {Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1149},
      year = {2021},
      doi = {10.1145/3460120.3484771},
      note = {\url{https://eprint.iacr.org/2021/1149}},
      url = {https://eprint.iacr.org/2021/1149}
}