Concrete Security Bounds for Simulation-Based Proofs of Multi-Party Computation Protocols

TL;DR

This paper introduces a new method for automatically computing precise concrete security bounds for multi-party computation protocols, supported by formal verification and implemented in Maude, significantly simplifying and reducing proof complexity.

Contribution

It presents a foundational approach inspired by IPDL for deriving concrete security bounds in MPC, including the first formal verification of GMW protocol security in this style.

Findings

First formal verification of GMW protocol security bounds

Automated computation of concrete security bounds for MPC

Proof size reduced by 72% compared to prior methods

Abstract

The concrete security paradigm aims to give precise bounds on the probability that an adversary can subvert a cryptographic mechanism. This is in contrast to asymptotic security, where the probability of subversion may be eventually small, but large enough in practice to be insecure. Fully satisfactory concrete security bounds for Multi-Party Computation (MPC) protocols are difficult to attain, as they require reasoning about the running time of cryptographic adversaries and reductions. In this paper we close this gap by introducing a new foundational approach that allows us to automatically compute concrete security bounds for MPC protocols. We take inspiration from the meta-theory of IPDL, a prior approach for formally verified distributed cryptography, to support reasoning about the runtime of protocols and adversarial advantage. For practical proof developments, we implement our approach in Maude, an extensible logic for equational rewriting. We carry out four case studies of concrete security for simulation-based proofs. Most notably, we deliver the first formal verification of the GMW MPC protocol over N parties. To our knowledge, this is the first time that formally verified concrete security bounds are computed for a proof of an MPC protocol in the style of Universal Composability. Our tool provides a layer of abstraction that allows the user to write proofs at a high level, which drastically simplifies the proof size. For comparison, a case study that in prior works required 2019 LoC only takes 567 LoC, thus reducing proof size by 72%