How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation

TL;DR

This paper formalizes security proofs for cryptographic multi-party computation protocols within Isabelle/HOL, using simulation-based reasoning to ensure privacy and correctness guarantees.

Contribution

It presents the first formalization of MPC security proofs in Isabelle/HOL, adapting probabilistic reasoning tools for cryptographic simulation arguments.

Findings

First formalization of MPC security proofs in Isabelle/HOL

Adaptation of probabilistic program reasoning for cryptography

Enables precise verification of MPC protocols' security guarantees

Abstract

In cryptography, secure Multi-Party Computation (MPC) protocols allow participants to compute a function jointly while keeping their inputs private. Recent breakthroughs are bringing MPC into practice, solving fundamental challenges for secure distributed computation. Just as with classic protocols for encryption and key exchange, precise guarantees are needed for MPC designs and implementations; any flaw will give attackers a chance to break privacy or correctness. In this paper we present the first (as far as we know) formalisation of some MPC security proofs. These proofs provide probabilistic guarantees in the computational model of security, but have a different character to machine proofs and proof tools implemented so far --- MPC proofs use a \emph{simulation} approach, in which security is established by showing indistinguishability between execution traces in the actual protocol execution and an ideal world where security is guaranteed by definition. We show that existing machinery for reasoning about probabilistic programs adapted to this setting, paving the way to precisely check a new class of cryptography arguments. We implement our proofs using the CryptHOL framework inside Isabelle/HOL.