πMPC: Automatic Security Proofs for MPC Protocols
summary
A domain-specific language plus static analyzer aims to produce automatic simulator synthesis for secure multiparty computation by validating programs in two stages: type inference to enforce preconditions, then probabilistic-programming checks that certify posterior inference guarantees about input distributions given outputs. Work in progress: no πMPC language yet, prototypes show posterior sampling and conditional-independence are the hard parts, Bayes nets and product networks fail to express real MPC protocols, and efficiency constraints force design tradeoffs.
AI-written summary · about
chapters (8)
- 0:00Start
- 0:24What is MPC and why do we want it?
- 0:45What does "secure" mean for an MPC system?
- 1:23The behavior of a simulator needs to be "just right".
- 1:55The problem is posterior inference (and sampling)
- 2:39Probabilistic independence suffices for simulation.
- 3:07Use type annotations to provide partial invertablity
- 3:45Options for Exact Inference?
related talks
23mRecent progress in MPC-in-the-Head protocols
49mCompiling to preserve our privacy
53mFormal security analysis of MPC-in-the-headzero-knowledge protocols
41mMPC-in-the-Head based Zero Knowledge Proofs
45mPrice of Active Security in Multiparty Computation
51mDistributed Zero-Knowledge Proofs and Applications to Secure Computation
33mInteraction Preserving Compilers for Secure Computation
34mIs It Even Possible? On the Parallel Composition of Asynchronous MPC Protocols