GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols

GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols

Speakers: Xingyu Xie, Yifei Li, Wei Zhang, Tuowei Wang, Shizhen Xu, Jun Zhu

Conference: IEEE S&P

YouTube: https://www.youtube.com/watch?v=LnvewUHVM7U

Overview

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.

The framework, developed by researchers from Tsinghua University and Real AI, addresses a critical gap in the field: the lack of automated tools that can provide strong security guarantees for MPC. The speakers highlight the difficulty of understanding and writing traditional simulation-based proofs, which often contain "notorious mistakes." GAuV tackles this challenge head-on by applying formal verification techniques to automatically check if a given MPC protocol is secure under a specific threat model. This innovation is crucial for the broader adoption of MPC in sensitive applications, where mathematical certainty of security is paramount.

The significance of GAuV lies in its potential to democratize the rigorous security analysis of MPC protocols. By automating a process that currently demands specialized expertise and significant manual effort, GAuV can help protocol designers and implementers identify vulnerabilities early, thereby enhancing the trustworthiness and reliability of privacy-preserving computations. The framework's focus on perfect semi-honest security – a strong security notion that relies on no cryptographic assumptions and assumes an honest-but-curious adversary – further underscores its value for high-assurance applications.

Background

▶ Watch: Introduction to automated MPC security verification (0:00)

Multiparty Computation (MPC) protocols allow a set of participants to jointly compute a function f(x1, ..., xn) where each participant Pi holds a private input xi. The core security guarantee for MPC is that no participant learns anything about the other participants' private inputs beyond what can be inferred from their own input and the final output of the function. This is formally captured by simulation-based security.

The concept of simulation-based security is often explained through the ideal/real world paradigm. In the ideal world, all parties submit their private inputs to a single, trusted third party, known as the ideal functionality. This trusted party computes the function f and returns the correct outputs to each participant. No participant learns anything beyond their own input and output, as the trusted party does not leak intermediate information.

In the real world, there is no trusted third party. Instead, participants interact via a cryptographic protocol. To prove that a real-world protocol is secure, one must demonstrate that it is indistinguishable from the ideal world. This is achieved by constructing an algorithm called a simulator. The simulator's role is to mimic the "view" of any corrupted party (a party controlled by an adversary) in the real world, using only the corrupted party's own input and output, and the ideal functionality's behavior. If such a simulator exists, it implies that the corrupted parties in the real world see no more information than they would in the ideal world, thus preserving privacy.

The challenge lies in the construction of these simulators. Manual construction and proof are intricate, error-prone, and require deep cryptographic expertise. The complexity of tracking variable dependencies, message flows, and random number generation across multiple parties makes it a daunting task, often leading to "notorious mistakes" in published proofs. Prior work in MPC verification has often relied on general-purpose formal verification tools like SMT solvers (e.g., Z3) or proof assistants (e.g., Coq), which can be powerful but often require significant manual effort to model the cryptographic primitives and protocols correctly. GAuV aims to provide a more specialized and automated approach for this specific problem domain, focusing on the structural properties of MPC protocols rather than low-level cryptographic details. The framework specifically targets perfect security, meaning it does not rely on computational assumptions (like the hardness of factoring) but rather on information-theoretic properties, and operates under the semi-honest adversary model, where corrupted parties follow the protocol specification but try to extract additional information.

Key Findings

▶ Watch: Walkthrough: 3-party addition protocol and simulator goal (3:45)

The central contribution of the GAuV framework is its ability to automatically verify the perfect semi-honest security of MPC protocols by transforming them into a simulator. The key findings and contributions can be summarized as follows:

1. Graph-Based Intermediate Representation: GAuV models MPC protocols as data flow graphs. This representation captures the essential relationships between variables, inputs, outputs, and computations, making the protocol amenable to formal analysis and transformation.
2. Definition of Vintage Transformation: The framework introduces the concept of a vintage transformation, which is a formalized set of rules for manipulating data flow graphs. A vintage transformation from graph G to H is an injection from the nodes of H to G that satisfies three critical requirements:

• Preservation of Basic Nodes and Properties: Corrupted party nodes and other fundamental protocol properties must remain intact.
• Preservation of View Distribution: The distribution of the views of corrupted parties must be preserved across the transformation. This is crucial for maintaining the simulation-based security guarantee.
• Preservation of Correctness: The transformed graph H must remain correct with respect to the ideal functionality, meaning its outputs must match those of the ideal functionality.

1. Machine-Operable Transformation Rules: From the abstract concept of vintage transformation, GAuV derives two concrete, machine-operable transformation rules:

• Equivalent Rewriting: This rule allows substituting a sub-graph with an equivalent one. It's precisely defined by requiring both the original and transformed graphs to be acyclic and preserving the number of each type of random node, ensuring the possibilities of randomness assignments are unchanged.
• Tail Node Elimination: This rule permits the elimination of a node that has no outgoing edges, akin to dead code elimination in compilers. This is used to remove redundant computations that no longer affect the corrupted party's view after other transformations.

1. The Sound Theorem: The theoretical backbone of GAuV is its Sound Theorem. This theorem states that given a correct MPC protocol P, if for any possible set of corrupted parties, there exists a series of vintage transformations from P to a simulator, then P is secure. This theorem provides the formal guarantee that if GAuV successfully finds a simulator, the protocol is indeed secure.
2. Simulator Finding Algorithm: GAuV implements a searching algorithm that treats graphs as states and vintage transformations as transitions. Guided by a cost function, it employs a best-first search strategy to find a sequence of transformations that leads to a valid simulator. The soundness of this algorithm directly follows from the Sound Theorem.
3. Generalization via Hybrid Argument: The framework's methodology is tied to the hybrid argument, a common technique in cryptography for proving indistinguishability between two distributions. The step-by-step vintage transformations can be seen as a mechanized point in a hybrid argument, allowing GAuV to be generalized to more advanced perfectly secure protocols like DN (Damgård-Nielsen) and A (Asharov et al.) protocols.

These findings collectively present a robust, formal, and automated approach to a problem traditionally dominated by manual, expert-intensive methods, promising greater assurance and efficiency in MPC protocol design.

Technical Deep Dive

▶ Watch: Key transformation: Introducing ideal functionality for W (8:40)

The core technical innovation of GAuV lies in its structured approach to transforming an MPC protocol, represented as a data flow graph, into a simulator. This process is guided by the principles of vintage transformation, ensuring that the resulting simulator accurately reflects the corrupted party's view without revealing honest parties' private inputs.

Let's dissect the process using the example provided in the talk: a three-party addition protocol where Alice (X), Bob (Y), and Charlie (Z) want to compute W = X + Y + Z. Charlie is assumed to be the corrupted party. The simulator's goal is to produce Charlie's view (messages Charlie receives, B and R) using only Charlie's input Z and the final output W.

1. Initial Protocol Representation (Data Flow Graph):

The protocol begins with Alice generating a random mask R.

• Alice computes A = X + R.
• Alice sends A to Bob.
• Bob computes B = A + Y.
• Bob sends B to Charlie.
• Charlie computes C = B + Z.
• Alice sends R to Charlie.
• Charlie computes W = C - R.

In the data flow graph, nodes represent variables and operations, and edges represent data dependencies. The initial graph shows dependencies on X and Y (honest party inputs), which must be removed for the simulator. W (the protocol output) is also treated as an input for the simulator, as the simulator needs to know the final result to construct a consistent view. Nodes like X, Y, and W are initially marked as violating the technical goal if they represent honest party inputs or protocol outputs that the simulator needs to "invert" or derive.

1. Transformation Steps:

• Step 1: Reverse Alice's Computation to Remove Dependency on X

Original: A = X + R (Alice samples R, adds X to it).

Goal: Remove X.

Transformation: Instead of sampling R and adding X to it, the simulator can uniformly sample A and compute R = A - X. This seems counter-intuitive because X is still present. However, the crucial insight is that X is an honest party's input. The simulator needs to mimic the distribution of A and R as observed by Charlie. By sampling A and deriving R from X, the relationship between A and R is maintained, but the source of randomness is shifted. The actual removal of X comes later when R can be derived differently.

• Step 2: Reverse Bob's Computation to Remove Dependency on Y

Original: B = A + Y.

Goal: Remove Y.

Transformation: Similar to Step 1, the simulator can uniformly sample B and compute A = B - Y. Again, Y is an honest party's input. The goal is to shift the dependency.

• Step 3: Introduce Ideal Functionality and Compute W

This is the "magic" step. The ideal functionality directly computes W = X + Y + Z.

The simulator knows W (as its input) and Z (Charlie's input).

From W = X + Y + Z, we can derive X + Y = W - Z.

Recall W = C - R.

And C = B + Z.

So, W = (B + Z) - R.

Therefore, R = (B + Z) - W.

Now we have two ways to compute R: R = A - X (from Step 1, conceptually) and R = (B + Z) - W (from this step). The latter is crucial because it depends only on B, Z, and W – none of which are honest party inputs that need to be hidden. The consistency between these two derivations of R comes from the protocol's correctness.

• Step 4: Remove Redundant Computation (Tail Node Elimination)

After Step 3, the simulator can compute R using R = (B + Z) - W. This derivation no longer depends on X or Y. Consequently, the original computations involving X and Y (e.g., A = X + R and B = A + Y) become redundant from the perspective of constructing Charlie's view. The nodes representing X and Y, as well as the intermediate variable A, can be eliminated from the graph. The simulator now constructs Charlie's view (B and R) using only Z and W.

1. Formalizing Vintage Transformation:

A vintage transformation from G to H is formally an injection from the nodes of H to G. It must satisfy:

• Preservation of Corrupted Party Nodes: Nodes corresponding to corrupted parties and their inputs/outputs are preserved.
• View Distribution Preservation: The probability distribution of the corrupted parties' views in H must be identical to that in G. This is the essence of simulation-based security.
• Correctness Preservation: H must still correctly compute the function f with respect to the ideal functionality.

1. Machine-Operable Rules:

• Equivalent Rewriting: This rule allows replacing a sub-graph L with an equivalent sub-graph R within G to form H. This is only valid if both G and H are acyclic and, crucially, the number of random nodes of each type is preserved. This ensures that the overall randomness space and its distribution are maintained, which is vital for security proofs.
• Tail Node Elimination: This rule is straightforward: if a node has no outgoing edges (i.e., its value is not used by any subsequent computation relevant to the corrupted party's view), it can be removed. This is directly analogous to dead code elimination in compilers and is used to clean up the graph once dependencies on honest party inputs have been removed or circumvented.

1. The Sound Theorem and Algorithm:

The Sound Theorem provides the formal guarantee: if GAuV can find a sequence of vintage transformations from a correct protocol P to a simulator for any corrupted party set, then P is secure. The simulator-finding algorithm operates as a best-first search on the state space of graphs, where each state is a protocol graph and transitions are vintage transformations. A cost function guides the search towards graphs that are closer to a simulator (e.g., graphs with fewer dependencies on honest party inputs). The algorithm's soundness is a direct consequence of the Sound Theorem.

GAuV's trusted code base is self-contained, not relying on external SMT solvers like Z3 or proof assistants like Coq. This design choice aims to minimize the trusted computing base and simplify verification of the framework itself.

Demo / Proof of Concept

▶ Watch: Formalizing "good transformations": The Vintage Transformation (10:20)

While the talk did not feature a live, interactive demonstration of the GAuV tool, the speakers effectively illustrated its capabilities through a detailed worked example and presented evaluation results on established MPC protocols. These serve as the proof of concept for the framework's design and implementation.

The primary conceptual demonstration was the three-party addition protocol described in the "Technical Deep Dive" section. This example walked the audience step-by-step through how GAuV would transform an initial protocol description into a simulator. By showing how dependencies on honest party inputs (X and Y) are systematically removed through variable re-sampling, computation reversal, and the strategic introduction of the ideal functionality, the speakers concretely demonstrated the core mechanism of vintage transformations. This illustrated how the framework constructs a simulator that produces the corrupted party's view (B and R) solely from the corrupted party's input (Z) and the protocol's output (W).

Beyond this conceptual walkthrough, GAuV was evaluated as a prototype tool on two significant categories of MPC protocols:

1. BGW Protocols: The framework was tested on BGW (Ben-Or, Goldwasser, Wigderson) protocols, which are classical perfectly secure MPC protocols capable of computing any function composed of additions and multiplications. The evaluation showed that GAuV could successfully prove the security of BGW protocols for any set of corrupted parties. Crucially, it achieved this in polynomial time, given a suitable cost function to guide its search algorithm. This result is significant because BGW protocols are fundamental to MPC, and an automated, efficient verification for them demonstrates the scalability and practicality of GAuV.

1. Arithmetic Secret Sharing Conversion Protocols: GAuV was also applied to arithmetic secret sharing conversion protocols. These protocols are essential components in more complex MPC systems, enabling parties to switch between different secret-sharing schemes securely. The successful verification of these protocols further validates GAuV's ability to handle various cryptographic constructs commonly found in MPC.

Furthermore, the speakers discussed the generalizability of their method. They explained that GAuV's step-by-step vintage transformation process can be viewed as a mechanized form of the hybrid argument, a common proof technique for showing indistinguishability between two distributions. This insight suggests that GAuV could be adapted to verify the security of other advanced perfectly secure protocols, such as DN (Damgård-Nielsen) and A (Asharov et al.) protocols, by mechanizing the transformations between adjacent hybrids using equivalent rewriting or tail node elimination. This broader applicability, even if requiring "sufficient amount of time," indicates the foundational strength of the framework.

The existence of an open-source codebase (linked in the presentation) for the prototype tool further reinforces the demonstrative aspect, allowing other researchers and practitioners to inspect, reproduce, and build upon their work.

Defensive Implications

▶ Watch: GAuV prototype tool and evaluation results (15:00)

GAuV offers significant defensive implications for organizations and practitioners involved in designing, implementing, or deploying Multiparty Computation (MPC) protocols. Its primary benefit is providing a higher degree of security assurance by automating a process that is notoriously complex and error-prone when performed manually.

1. Enhanced Trustworthiness of MPC Deployments: For critical applications involving sensitive data (e.g., healthcare, finance, intelligence), the security of MPC protocols must be beyond doubt. GAuV provides a formal, machine-checked verification that a protocol adheres to its perfect semi-honest security guarantees. This means that if a protocol is verified by GAuV, defenders can be confident that even an adversary controlling a subset of parties (who follow the protocol but try to learn extra information) cannot glean any private inputs beyond what is revealed by their own input and the final output. This significantly boosts the trustworthiness of MPC systems.

1. Reduced Risk of Protocol Design Flaws: Manual security proofs for MPC protocols are known to contain subtle mistakes that can lead to exploitable vulnerabilities. By automating the verification process, GAuV acts as a robust check on protocol design. It can identify scenarios where a simulator cannot be constructed, indicating a potential security flaw that would likely be missed by human review alone. This allows designers to catch and rectify vulnerabilities early in the development lifecycle, preventing costly exploits down the line.

1. Faster and More Reliable Protocol Development: The traditional burden of writing and reviewing complex simulation-based proofs can slow down the development and deployment of new MPC protocols. GAuV streamlines this process, allowing researchers and developers to iterate on protocol designs more rapidly, with automated security checks providing immediate feedback. This accelerates innovation in privacy-preserving technologies without compromising security.

1. Clarity on Security Model: GAuV operates under a very specific and strong security model: perfect semi-honest security. For defenders, understanding this model is crucial.

• Perfect Security: Implies information-theoretic security, meaning it does not rely on any unproven cryptographic assumptions (e.g., the difficulty of factoring large numbers). This is a very strong guarantee, providing security even against adversaries with unlimited computational power.
• Semi-Honest Adversary: Assumes the corrupted parties will honestly follow the protocol instructions but will attempt to extract additional information from the messages they observe. This is distinct from a malicious adversary who might deviate from the protocol. Defenders must be aware that GAuV's current scope does not cover malicious adversaries, and protocols designed for semi-honest security might be vulnerable to malicious attacks. However, many protocols are first designed and proven secure in the semi-honest model before adding robustness against malicious behavior.

1. Support for Complex Protocols: The framework's ability to verify classical BGW protocols in polynomial time, and its potential to generalize to more advanced protocols like DN and A through mechanized hybrid arguments, indicates its capacity to handle the complexity inherent in real-world MPC systems. This means that even as MPC protocols become more sophisticated, GAuV can remain a relevant tool for ensuring their security.

In essence, GAuV empowers defenders by shifting the burden of security proof from human experts to an automated system. This leads to more secure, more efficiently developed, and more trustworthy MPC solutions, fostering greater confidence in privacy-preserving computations across various sensitive domains.

Key Takeaways

• Automated Verification for MPC Security: GAuV provides a novel, graph-based framework for automatically verifying the perfect semi-honest security of Multiparty Computation (MPC) protocols, addressing the complexity and error-proneness of manual proofs.
• Formal Foundation with Vintage Transformations: The framework's core is the concept of vintage transformations, a formalized set of graph manipulation rules (like equivalent rewriting and tail node elimination) that preserve the view distribution of corrupted parties and protocol correctness.
• Soundness Guarantee: The Sound Theorem formally proves that if GAuV can transform a protocol into a simulator through a series of vintage transformations, the protocol is indeed secure under the specified model.
• Practical Applicability: GAuV has been successfully evaluated on classical BGW protocols, demonstrating its ability to prove security for any corrupted party set in polynomial time, and also on arithmetic secret sharing conversion protocols.
• Generalizable Approach: The methodology is linked to the hybrid argument, suggesting its potential for verifying more advanced perfectly secure protocols (e.g., DN, A protocols) by mechanizing hybrid transitions.
• Specific Security Model: GAuV targets perfect security (information-theoretic, no cryptographic assumptions) against a semi-honest adversary (parties follow protocol but try to learn extra information), providing strong guarantees within this defined threat model.

About the Speaker(s)

The talk was presented by Xingyu Xie, representing Tsinghua University and Real AI, along with co-authors Yifei Li, Wei Zhang, Tuowei Wang, Shizhen Xu, and Jun Zhu. The primary speaker, Xingyu Xie, introduced himself as being from Tsinghua University and Real AI. While specific titles or detailed biographies were not provided in the transcript, their affiliation with a prominent academic institution like Tsinghua University and a research entity like Real AI indicates their expertise in cryptography, formal methods, and artificial intelligence, particularly in the domain of secure computation and automated verification. Their collaborative work on GAuV demonstrates a commitment to advancing the security and practicality of Multiparty Computation protocols.