Explore a conference talk on computer-aided verification and software synthesis for secure multi-party computation (MPC) protocols. Delve into the progress made in developing high-assurance implementations of MPC, including the formalization of secret sharing variations and MPC protocols in EasyCrypt. Learn about the computer-checked security proofs of concrete protocol instantiations and the first computer-aided verification and automated synthesis of the fundamental BGW protocol. Discover a new toolchain for extracting high-assurance executable implementations from EasyCrypt specifications, and compare the performance of these executables to manually implemented versions. Gain insights into the benefits of high-assurance implementations for correctness and security in MPC protocols.
Computer Aided Verification and Software Synthesis for Secure Multi Party Computation Protocols
Overview
Syllabus
Intro
Proactive Security
Fundamental MPC Protocol: BGW'88
Sample Module: ElGamal
Existing Verification Work of Secure Computation
Sample Abstract Definition: Secret Sharing (SS)
Sample Abstract Definition: Verifiable SS
Sample instantiation of Primitive (SS) 1/3
Instantiation of Secret Sharing Framework
Sample Abstract (MPC) Protocol Definition
MPC Abstract Protocol Framework
Sample instantiation of Protocol (Recover)
Sample EasyCrypt Proof Skeleton (Passive)
Sample Security Game (for SS)
Toolchain to Synthesize Executable Software
Performance of Extracted Executable 1/2
Frequently Asked Questions/Objections
Conclusion
Taught by
TheIACR
