GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols
Xingyu Xie, Yifei Li, Wei Zhang, Tuowei Wang, Shizhen Xu, Jun Zhu
IEEE Symposium on Security and Privacy 2024 · Day 1 · Continental Ballroom 6
Multiparty Computation (MPC) protocols are foundational to privacy-preserving technologies, enabling multiple parties to jointly compute a function over their private inputs without revealing those inputs to each other. However, proving the security of MPC protocols, particularly **simulation-based security**, is notoriously complex and prone to human error. This talk introduces GAuV, a novel **graph-based automated verification framework** designed to formally verify the **perfect semi-honest security** of MPC protocols. By transforming protocols into a formal, machine-readable representation, GAuV aims to eliminate the need for laborious and often fallible manual proofs, offering a robust and scalable solution for ensuring the cryptographic integrity of these intricate systems.
AI review
GAuV presents a truly novel and critical automated verification framework for the perfect semi-honest security of MPC protocols. By formalizing protocols as data flow graphs and employing "vintage transformations," it eliminates the notorious complexity and error-proneness of manual simulation-based proofs. This research offers a robust, scalable solution that will significantly enhance the trustworthiness and adoption of privacy-preserving computation.