Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

IEEE Symposium on Security and Privacy (S&P)

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, Yifan Song

Published May 19, 2024• 3 citations
Publisher

Abstract

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.

DOI
10.1109/sp54263.2024.00131

Related papers

Foundations of Secure Computation: Perfect Security and Fairness

Gilad Asharov

In the setting of secure multiparty computation, several distrustful parties wish to carry out a distributed computing task on their local private data while satisfying several security properties such as correctness, privacy, independence of inputs and fairness. The aim of secure multiparty computation (MPC) is to enable the parties to carry out the computation in a secure manner, eliminating any attempt of an adversarial entity to harm the execution. The concept of secure computation is very general and fundamental in cryptography, and models any distributed computing task, including simple computations as coin-tossing and broadcast, as well as more complex tasks such as electronic auctions and anonymous transactions. In this thesis, we study two foundational aspects of secure computation: perfect security and fairness. In the first part of this thesis, we study perfect security in secure computation. A protocol that is perfectly secure cannot be broken even when the adversary has unlimited computational power and its security holds unconditionally. One of the most fundamental results of secure computation was presented by Ben-Or, Goldwasser and Wigderson (BGW) in 1988. They demonstrated that any n-party functionality can be computed with perfect security, in the private channels model. When the adversary is semi-honest this holds as long as t < n/2 parties are corrupted, and when the adversary is malicious this holds as long as t < n/3 parties are corrupted. Unfortunately, a full proof of these results was never published. In this thesis, we remedy this situation and provide a full proof of security of the BGW protocol. This also includes a full description of the protocol for the malicious setting. In addition to the above, we observe that by some simple and natural modifications, the BGW protocol can be significantly simplified and one of its expensive (and perhaps most complicated) subprotocols can be saved. We present a new multiplication protocol that is based on the original construction, but is simpler and achieves higher efficiency. In the second part of this thesis, we study fairness in secure two party computation. Informally, the fairness property guarantees that if one party receives its output, then the other party does too. The well-known impossibility result of Cleve (STOC 1986) implies that, in general, it is impossible to securely compute a function with complete fairness without an honest majority. Until recently, the accepted belief has been that nothing non-trivial can be computed with complete fairness in the two party setting. The surprising work of Gordon, Hazay, Katz and Lindell (STOC 2008) shows that this belief is false, and that there exist some non-trivial (deterministic, finite-domain) Boolean functions that can be computed fairly. This raises the fundamental question of characterizing complete fairness in secure two-party computation. We focus on this question and give both positive and negative results. We first characterize

•Jan 1, 2014•0 citations

A Full Proof of the BGW Protocol for Perfectly-Secure Multiparty Computation.

Gilad Asharov, Yehuda Lindell

In the setting of secure multiparty computation, a set of n parties with private inputs wish to jointly compute some functionality of their inputs. One of the most fundamental results of information-theoretically secure computation was presented by Ben-Or, Goldwasser and Wigderson (BGW) in 1988. They demonstrated that any n-party functionality can be computed with perfect security, in the private channels model. When the adversary is semi-honest this holds as long as t < n/2 parties are corrupted, and when the adversary is malicious this holds as long as t < n/3 parties are corrupted. Unfortunately, a full detailed proof of these results was never given. In this paper, we remedy this situation and provide a full proof of security of the BGW protocol. We also derive corollaries for security in the presence of adaptive adversaries and under concurrent general composition (equivalently, universal composability). In addition, we give a full specification of the protocol for the malicious setting. This includes one new step

Electronic colloquium on computational complexity•Jan 1, 2011•23 citations

A Framework for Constructing Fast MPC over Arithmetic Circuits with Malicious Adversaries and an Honest-Majority

Yehuda Lindell, Ariel Nof

Protocols for secure multiparty computation enable a set of parties to compute a function of their inputs without revealing anything but the output. The security properties of the protocol must be preserved in the presence of adversarial behavior. The two classic adversary models considered are semi-honest (where the adversary follows the protocol specification but tries to learn more than allowed by examining the protocol transcript) and malicious (where the adversary may follow any arbitrary attack strategy). Protocols for semi-honest adversaries are often far more efficient, but in many cases the security guarantees are not strong enough.

ACM SIGSAC Conference on Computer and Communications Security (CCS)•Oct 27, 2017•96 citations

A New Paradigm for Practical Maliciously Secure Multi-Party Computation

Xiao Wang

Secure Multi-Party Computation (MPC) protocols allow a group of mutually distrusting users to compute a function jointly on their inputs without revealing any information beyond the output. For many years, implementations of MPC protocols have targeted security against semi-honest adversaries, i.e., attackers are assumed to execute the protocol honestly but try to learn private information after the fact. Protocols secure against stronger and more realistic malicious adversaries, who could behave arbitrarily during the protocol execution, were known to exist but were much less efficient. This thesis introduces a new paradigm to construct extremely efficient MPC protocols with malicious security. In particular, this thesis consists of three major contributions. 1. We introduce the authenticated garbling framework, and present an efficient concrete instantiation of the protocol. The resulting protocol partially closes the gap between semi-honest and malicious MPC protocols asymptotically; the implementation of the protocol represents the state-of-the-art system for malicious two-party computation. 2. We discuss how to apply authenticated garbling to the multi-party setting, where all-but-one parties can be corrupted by the adversary. The resulting protocol improves upon the best previous constant-round protocol by orders of magnitude. We also present a system that, for the first time, enables MPC executions among hundreds of parties, distributed globally. 3. We present a series of optimizations to two-party authenticated garbling by interpreting authenticated garbling in a new way. The improved malicious protocol has essentially the same concrete efficiency as the best semi-honest protocol in the preprocessing model. 4. We develop these protocols in EMP-toolkit, a practical and efficient MPC tool that can be used to build new protocols and to develop applications using our existing protocols.

•Jan 1, 2018•2 citations

On Definitions for Semi-Honest Secure Multiparty Computation

Koji Nuida

Secure multiparty computation (MPC) is a cryptographic technology to perform some computation on multiple parties' input data while concealing the individual inputs from other parties. For the case of semi-honest adversaries, the security definition in Goldreich's famous book is widely used as a standard definition. In this paper, however, we point out that there is an MPC protocol where a semi-honest adversary receives only a ciphertext of one-time pad with unknown key but the protocol is not secure under the standard security definition, which may look inconsistent with the perfect secrecy of one-time pad that its ciphertext leaks no information at all. We propose a variant of the security definition that resolves this issue. We also show that a somewhat restrictive version of the Composition Theorem holds for our modified security definition.

IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences•Jun 24, 2025•0 citations

Round-Optimal Secure Multiparty Computation from Minimal Assumptions

Akshayaram Srinivasan

Secure Multiparty Computation (MPC) allows a set of parties, each having its own private data, to compute a function of their joint data such that the parties only learn the output of this function and everything else about their data is hidden. MPC is a fundamental cryptographic abstraction that captures many other natural cryptographic primitives as special cases. It also has a wide range of practical applications such as conducting secure electronic auctions, delegating sensitive computation to untrusted cloud service providers, secure computation on genomic data and training machine learning models on private data.A long-standing open problem in this area is to construct MPC protocols that have {\\it optimal} (two-round) round complexity under the {\\it weakest} possible cryptographic hardness assumptions.We {\\it completely resolve} this problem by showing lower bounds and matching upper bounds on the hardness assumptions required for constructing round-optimal MPC. Specifically, we obtain the following results.\\begin{itemize}\\item \\textbf{Black-Box Separation.} We show that there exists no construction of two-round semi-honest MPC protocol for general functions that makes black-box use of a two-round oblivious transfer. As a corollary, a similar separation holds when starting with any 2-party functionality other than oblivious transfer. \\item \\textbf{Non-Black-Box Construction.} We show that the above negative result can be bypassed by making non-black-box use of a two-round oblivious transfer. Specifically, starting from a semi-honest (resp. malicious) secure two-round oblivious transfer protocol, we construct a two-round MPC protocol against semi-honest (resp. malicious) adversaries. \\end{itemize}Since any two-round MPC protocol for general functionalities implies a two-round oblivious transfer as a special case, the above two results show that non-black-box use of oblivious transfer is {\\it necessary and sufficient} to construct round-optimal MPC protocols.

•Jan 1, 2020•0 citations
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.
In the setting of secure multiparty computation, several distrustful parties wish to carry out a distributed computing task on their local private data while satisfying several security properties such as correctness, privacy, independence of inputs and fairness. The aim of secure multiparty computation (MPC) is to enable the parties to carry out the computation in a secure manner, eliminating any attempt of an adversarial entity to harm the execution. The concept of secure computation is very general and fundamental in cryptography, and models any distributed computing task, including simple computations as coin-tossing and broadcast, as well as more complex tasks such as electronic auctions and anonymous transactions. In this thesis, we study two foundational aspects of secure computation: perfect security and fairness. In the first part of this thesis, we study perfect security in secure computation. A protocol that is perfectly secure cannot be broken even when the adversary has unlimited computational power and its security holds unconditionally. One of the most fundamental results of secure computation was presented by Ben-Or, Goldwasser and Wigderson (BGW) in 1988. They demonstrated that any n-party functionality can be computed with perfect security, in the private channels model. When the adversary is semi-honest this holds as long as t < n/2 parties are corrupted, and when the adversary is malicious this holds as long as t < n/3 parties are corrupted. Unfortunately, a full proof of these results was never published. In this thesis, we remedy this situation and provide a full proof of security of the BGW protocol. This also includes a full description of the protocol for the malicious setting. In addition to the above, we observe that by some simple and natural modifications, the BGW protocol can be significantly simplified and one of its expensive (and perhaps most complicated) subprotocols can be saved. We present a new multiplication protocol that is based on the original construction, but is simpler and achieves higher efficiency. In the second part of this thesis, we study fairness in secure two party computation. Informally, the fairness property guarantees that if one party receives its output, then the other party does too. The well-known impossibility result of Cleve (STOC 1986) implies that, in general, it is impossible to securely compute a function with complete fairness without an honest majority. Until recently, the accepted belief has been that nothing non-trivial can be computed with complete fairness in the two party setting. The surprising work of Gordon, Hazay, Katz and Lindell (STOC 2008) shows that this belief is false, and that there exist some non-trivial (deterministic, finite-domain) Boolean functions that can be computed fairly. This raises the fundamental question of characterizing complete fairness in secure two-party computation. We focus on this question and give both positive and negative results. We first characterize
In the setting of secure multiparty computation, a set of n parties with private inputs wish to jointly compute some functionality of their inputs. One of the most fundamental results of information-theoretically secure computation was presented by Ben-Or, Goldwasser and Wigderson (BGW) in 1988. They demonstrated that any n-party functionality can be computed with perfect security, in the private channels model. When the adversary is semi-honest this holds as long as t < n/2 parties are corrupted, and when the adversary is malicious this holds as long as t < n/3 parties are corrupted. Unfortunately, a full detailed proof of these results was never given. In this paper, we remedy this situation and provide a full proof of security of the BGW protocol. We also derive corollaries for security in the presence of adaptive adversaries and under concurrent general composition (equivalently, universal composability). In addition, we give a full specification of the protocol for the malicious setting. This includes one new step
Protocols for secure multiparty computation enable a set of parties to compute a function of their inputs without revealing anything but the output. The security properties of the protocol must be preserved in the presence of adversarial behavior. The two classic adversary models considered are semi-honest (where the adversary follows the protocol specification but tries to learn more than allowed by examining the protocol transcript) and malicious (where the adversary may follow any arbitrary attack strategy). Protocols for semi-honest adversaries are often far more efficient, but in many cases the security guarantees are not strong enough.
Secure Multi-Party Computation (MPC) protocols allow a group of mutually distrusting users to compute a function jointly on their inputs without revealing any information beyond the output. For many years, implementations of MPC protocols have targeted security against semi-honest adversaries, i.e., attackers are assumed to execute the protocol honestly but try to learn private information after the fact. Protocols secure against stronger and more realistic malicious adversaries, who could behave arbitrarily during the protocol execution, were known to exist but were much less efficient. This thesis introduces a new paradigm to construct extremely efficient MPC protocols with malicious security. In particular, this thesis consists of three major contributions. 1. We introduce the authenticated garbling framework, and present an efficient concrete instantiation of the protocol. The resulting protocol partially closes the gap between semi-honest and malicious MPC protocols asymptotically; the implementation of the protocol represents the state-of-the-art system for malicious two-party computation. 2. We discuss how to apply authenticated garbling to the multi-party setting, where all-but-one parties can be corrupted by the adversary. The resulting protocol improves upon the best previous constant-round protocol by orders of magnitude. We also present a system that, for the first time, enables MPC executions among hundreds of parties, distributed globally. 3. We present a series of optimizations to two-party authenticated garbling by interpreting authenticated garbling in a new way. The improved malicious protocol has essentially the same concrete efficiency as the best semi-honest protocol in the preprocessing model. 4. We develop these protocols in EMP-toolkit, a practical and efficient MPC tool that can be used to build new protocols and to develop applications using our existing protocols.
Secure multiparty computation (MPC) is a cryptographic technology to perform some computation on multiple parties' input data while concealing the individual inputs from other parties. For the case of semi-honest adversaries, the security definition in Goldreich's famous book is widely used as a standard definition. In this paper, however, we point out that there is an MPC protocol where a semi-honest adversary receives only a ciphertext of one-time pad with unknown key but the protocol is not secure under the standard security definition, which may look inconsistent with the perfect secrecy of one-time pad that its ciphertext leaks no information at all. We propose a variant of the security definition that resolves this issue. We also show that a somewhat restrictive version of the Composition Theorem holds for our modified security definition.
Secure Multiparty Computation (MPC) allows a set of parties, each having its own private data, to compute a function of their joint data such that the parties only learn the output of this function and everything else about their data is hidden. MPC is a fundamental cryptographic abstraction that captures many other natural cryptographic primitives as special cases. It also has a wide range of practical applications such as conducting secure electronic auctions, delegating sensitive computation to untrusted cloud service providers, secure computation on genomic data and training machine learning models on private data.A long-standing open problem in this area is to construct MPC protocols that have {\\it optimal} (two-round) round complexity under the {\\it weakest} possible cryptographic hardness assumptions.We {\\it completely resolve} this problem by showing lower bounds and matching upper bounds on the hardness assumptions required for constructing round-optimal MPC. Specifically, we obtain the following results.\\begin{itemize}\\item \\textbf{Black-Box Separation.} We show that there exists no construction of two-round semi-honest MPC protocol for general functions that makes black-box use of a two-round oblivious transfer. As a corollary, a similar separation holds when starting with any 2-party functionality other than oblivious transfer. \\item \\textbf{Non-Black-Box Construction.} We show that the above negative result can be bypassed by making non-black-box use of a two-round oblivious transfer. Specifically, starting from a semi-honest (resp. malicious) secure two-round oblivious transfer protocol, we construct a two-round MPC protocol against semi-honest (resp. malicious) adversaries. \\end{itemize}Since any two-round MPC protocol for general functionalities implies a two-round oblivious transfer as a special case, the above two results show that non-black-box use of oblivious transfer is {\\it necessary and sufficient} to construct round-optimal MPC protocols.