Formal security analysis of MPC-in-the-headzero-knowledge protocols
summary
Formal claim: define a reusable decomposition interface for MPC-in-the-head, move sigma-protocol soundness into the MPC layer, and prove a generic transformation (commit+challenge+verify) secure under new properties. Tools: full machine-checked proof in EasyCrypt formalization using probabilistic and relational logics. Built and verified: a formalized ZKBoo instantiation that satisfies verifiability privacy extractability. Result is the first machine-checked security proof for this style; code extraction is possible but not produced.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:14What is MPC
- 2:07What is an MPC
- 4:32What does an MPC protocol do
- 6:51Sigbrew protocol
- 9:39General interface
- 12:24special soundness
- 14:35decomposition
- 18:01special sound
- 22:05Takeaways
- 26:22Questions
- 29:44Complexity of MPCs
- 32:30Verification effort
- 35:16More work
- 38:42Efficiency
- 45:38SS Proof System
- 49:59Reference document
- 52:15Wrapping up
related talks
41mMPC-in-the-Head based Zero Knowledge Proofs
35mEfficient Zero Knowledge Protocols: The Modular Approach
05mπMPC: Automatic Security Proofs for MPC Protocols
32mSoK: Private Programmability on Blockchain Systems
41mGKR based Zero-Knowledge Proofs
51mWhy you shouldn't trust me
33mInteraction Preserving Compilers for Secure Computation
27mUniversally Composable Security for Program Partitioning