Proving the security of a Multiparty Computation (MPC) protocol is a difficult task. Under the current simulation-based definition of MPC, a security proof consists of a simulator, which is usually specific to the concrete protocol and requires to be manually constructed, together with a theoretical analysis of the output distribution of the simulator and corrupted parties’ views in the real world. This presents an obstacle in verifying the security of a given MPC protocol. Moreover, an instance of a secure MPC protocol can easily lose its security guarantee due to careless implementation, and such a security issue is hard to detect in practice.(p)(/p)In this work, we propose a general automated framework to verify the perfect security of instances of MPC protocols against the semi-honest adversary. Our framework has perfect soundness: any protocol that is proven secure under our framework is also secure under the simulation-based definition of MPC. We demonstrate the completeness of our framework by showing that for any instance of the well-known BGW protocol, our framework can prove its security for every corrupted party set with polynomial time. Unlike prior work that only focuses on black-box privacy which requires the outputs of corrupted parties to contain no information about the inputs of the honest parties, our framework may potentially be used to prove the security of arbitrary MPC protocols. (p)(/p)We implement our framework as a prototype. The evaluation shows that our prototype automatically proves the perfect semi-honest security of BGW protocols and B2A (binary to arithmetic) conversion protocols in reasonable durations.
The aim of this paper is to present some of the recent progress in efficient secure multiparty computation (MPC). In MPC we have a set of parties owning a set of private inputs. The par ties want to compute a function of their inputs, but they do not trust each other, therefore they need a cryptographic protocol to perform the computation in a way that 1) the output is correct and 2) cheating parties will not be able to learn any information about the honest parties inputs. Even though this problem has been formulated and essentially solved almost 30 years ago, practical solutions that can be relevant for real-world applications have been discovered only in the last few years. We will present some of these advances, trying to explain to a non-specialized audience the significance of the several existing security notions.