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


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.

Available format(s)
Publication info
Published elsewhere. Minor revision. ACM CCS 2021
Zero-KnowledgeSecure Multiparty ComputationFormal Verification
Contact author(s)
hpacheco @ fc up pt
mbb @ fc up pt
jba @ di uminho pt
vitor pereira @ sri com
2021-09-15: revised
2021-09-10: received
See all versions
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.