Scientific knowledge map · Paper #58
Machine-Checked ZKP for NP Relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
2021 · 28th ACM Conference on Computer and Communications Security (CCS)
- Theory
- Applied
- protocol
- algorithm
Research question
What does the paper try to establish?
Can the generic MPC-in-the-Head transformation for NP zero-knowledge relations be specified and proved modularly in a proof assistant, then extracted into an executable verified implementation?
Central answer
What is the proposed answer?
The paper formalizes MitH in EasyCrypt with abstract interfaces for secret sharing, MPC, commitments, and zero knowledge; proves completeness, soundness, and zero knowledge; instantiates the framework with five-party BGW and two commitment choices; and extracts benchmarkable OCaml code.
Evidence profile
Six dimensions, kept separate
The chart summarizes documented evidence and process. It is not a correctness probability, confidence score, or ranking, and no composite score is calculated.
LowMediumHighN/A = not assessed
A smaller value means less documented support for that dimension, not that the paper is false or unimportant.
- Epistemic evidence High
-
The paper links formal definitions, machine-checked proofs, concrete verified components, executable extraction, public code, and preliminary measurements, while stating the concrete instantiation's limits.
Formal MitH transformation and security arguments Five-party BGW arithmetic-circuit instantiation Verified code extraction paths Preliminary performance results - Auditability High
-
A checked-in full manuscript with page count and SHA-256, archive and DOI identities, and a public formal-development repository make the evidence directly inspectable.
MitH motivation and contributions Public EasyCrypt and extracted-code repository Official ACM CCS publication identity - Production provenance Medium
-
Authors, venue, archive versions, repository, toolchain, and benchmark machine are documented, but exact commit-to-paper correspondence and contributor roles are not fully captured.
Public EasyCrypt and extracted-code repository Official ACM CCS publication identity Preliminary performance results - External scrutiny Medium
-
ACM CCS publication and public source provide external exposure, but review reports and an independent rerun are not represented.
Official ACM CCS publication identity Public EasyCrypt and extracted-code repository - Reception Low
-
The dated exact-DOI OpenAlex record located 1 citation. Under the author-defined rule, 0 through 8 located citations is Low; counts vary by index and date.
Dated citation-count snapshot - Contribution significance Medium
-
The source claims the first end-to-end machine-checked MitH development for general NP relations, but independent priority and broad downstream uptake are not established by this map.
MitH motivation and contributions Instantiation and evaluation boundaries
Assessment: Ai draft author review pending · 2026-07-11 · rubric 0.2. These dimensions describe documented support and process, not truth, correctness, or a universal ranking. No composite score is calculated.
Top-down and bottom-up view
Hierarchical knowledge map
Collapse a branch for a top-level reading, or follow its source links and child nodes to audit the evidence and boundaries underneath it.
Machine-Checked ZKP for NP Relations
A modular EasyCrypt formalization of MPC-in-the-Head, with machine-checked security arguments, concrete five-party arithmetic-circuit instantiation, and extracted executable code.
MitH motivation and contributions-
question Research question
research questionCan generic MitH proofs and their implementations be connected end to end through machine-checked definitions, modular components, and code extraction?
MitH motivation and contributions -
contribution Central answer
machine checked and extractedSpecify each cryptographic layer as an EasyCrypt interface, prove the generic transformation once, instantiate its assumptions with verified components, and extract the resulting concrete protocol into OCaml.
Formal MitH transformation and security arguments Five-party BGW arithmetic-circuit instantiation Verified code extraction paths -
scope Concrete instantiation
explicitly scopedThe represented executable uses Shamir sharing and five-party BGW arithmetic-circuit evaluation tolerating two semi-honest corruptions; the abstract framework permits other components, but those alternatives are not all verified here.
MitH motivation and contributions Five-party BGW arithmetic-circuit instantiation -
protocol Commit-challenge-response MitH
formally specifiedThe prover emulates an MPC evaluation on shared witness data, commits to party views, opens a verifier-selected subset, and is accepted when the views are pairwise consistent and produce an accepting circuit result.
ZK syntax, completeness, soundness, and simulation Formal MitH transformation and security arguments -
method Modular EasyCrypt framework
machine checkedAbstract theories define ZK protocols, relations, secret sharing, MPC circuits, party views, commitments, adversaries, simulators, and games; concrete clones discharge the interfaces and inherit the generic result.
Cryptographic definitions and EasyCrypt background ZK syntax, completeness, soundness, and simulation Abstract MPC syntax and privacy -
claim group Verified security properties machine checked
The development proves perfect completeness, concrete single-execution soundness and zero-knowledge bounds, and repetition meta-arguments in EasyCrypt rather than idealizing the commitment layer away.
ZK syntax, completeness, soundness, and simulation Formal MitH transformation and security arguments-
claim Perfect completeness
machine checkedFor a valid witness-statement pair and honest randomness, the formal protocol's verifier accepts with probability one.
ZK syntax, completeness, soundness, and simulation Formal MitH transformation and security arguments -
claim Soundness and zero knowledge
machine checked under component assumptionsSoundness follows from MPC correctness and commitment binding, while simulation-based zero knowledge follows from privacy of the opened MPC views and commitment hiding; repetition reduces the one-shot error under the formalized meta-argument.
ZK syntax, completeness, soundness, and simulation Formal MitH transformation and security arguments
-
-
method Verified arithmetic-circuit components concretely instantiated
The concrete stack fixes five BGW parties, Shamir sharing, addition, multiplication, scalar multiplication, and refresh gates over a finite field, and proves circuit correctness and two-view privacy compositionally.
Five-party BGW arithmetic-circuit instantiation-
algorithm Pedersen and PRF commitment choices
machine checkedOne path reuses Pedersen commitments; a faster path commits to a whole serialized view with a collision-resistant PRF instantiated by HMAC/SHA-256, with EasyCrypt reductions for binding and hiding.
PRF-based commitment proof
-
-
artifact group Executable extraction
verified code extractedAn EasyCrypt extraction tool produces OCaml from concrete specifications. The efficient path manually preserves the modular scaffold while automatically extracting concrete components, a boundary distinct from fully automatic end-to-end module extraction.
Verified code extraction paths Public EasyCrypt and extracted-code repository -
evidence Preliminary benchmark evidence
preliminary measurementSmall arithmetic circuits are benchmarked on a 2016 dual-core MacBook Pro. The SHA-256 commitment path substantially reduces commit and verify time relative to Pedersen in the reported examples, but the experiments are not application-scale.
Preliminary performance results -
limitation group Boundaries
materialThe concrete protocol fixes five parties and passive two-party corruption, evaluates arithmetic circuits represented as less-efficient trees, benchmarks only tiny circuits, and leaves actively secure or highly optimized MitH families and low-level optimized arithmetic to future work.
MitH motivation and contributions Five-party BGW arithmetic-circuit instantiation Preliminary performance results Instantiation and evaluation boundaries -
artifact group Auditable paper and development
publicly availableThe complete checked-in arXiv source has fixity metadata, the IACR ePrint and ACM DOI establish version identities, and the linked repository exposes formalization and extracted code. This audit did not rerun EasyCrypt or benchmarks.
Public EasyCrypt and extracted-code repository Official ACM CCS publication identity -
scrutiny External scrutiny
venue reviewedThe work appeared at ACM CCS 2021 and makes its formal development public. Review reports and independent reproduction are not linked.
Official ACM CCS publication identity Public EasyCrypt and extracted-code repository -
lineage Builds on verified MPC extraction
documentedThe work reuses the earlier high-assurance BGW development and extraction mechanism, then lifts them through a generic MitH transformation to verified zero-knowledge protocols.
MitH motivation and contributions Five-party BGW arithmetic-circuit instantiation
Audit trail
Source index
Locators state the depth of the current audit. PDF page numbers, where present, are one-based file pages; metadata-, summary-, and abstract-bounded records explicitly identify their limitations.
- MitH motivation and contributions Abstract and Section 1, PDF pages 1-4
- Cryptographic definitions and EasyCrypt background Section 3, PDF pages 5-8
- ZK syntax, completeness, soundness, and simulation Section 4.1, PDF pages 9-12
- Abstract MPC syntax and privacy Section 4.2, PDF pages 12-14
- Formal MitH transformation and security arguments Sections 4.3-4.4, PDF pages 14-20
- Five-party BGW arithmetic-circuit instantiation Section 5.1, PDF pages 20-23
- PRF-based commitment proof Section 5.2, PDF pages 23-25
- Verified code extraction paths Section 5.3, PDF page 25
- Preliminary performance results Section 5.4 and Table 1, PDF pages 25-26
- Instantiation and evaluation boundaries Sections 1 and 5, PDF pages 3-4 and 20-26
- Public EasyCrypt and extracted-code repository Repository path cited in Section 1; not rebuilt during this audit
- Official ACM CCS publication identity DOI 10.1145/3460120.3484771
- Dated citation-count snapshot OpenAlex reported 1 citation when accessed 2026-07-11