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

David Butler, David Aspinall, Adria Gascon

In cryptography, secure Multi-Party Computation (MPC) protocols allow participants to compute a function jointly while keeping their inputs private. Recent breakthroughs are bringi…