  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.
