How to simulate it in Isabelle: towards formal proof for secure multi-party computation

DOI10.1007/978-3-319-66107-0_8zbMATH Open1483.68486arXiv1805.12482OpenAlexW2748077663MaRDI QIDQ1687724FDOQ1687724

Authors: Peng Zhang 

Publication date: 4 January 2018

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.

Full work available at URL: https://arxiv.org/abs/1805.12482

Recommendations

• Computationally sound abstraction and verification of secure multi-party computations
• From secrecy to soundness: efficient verification via secure computation (extended abstract)
• An equational approach to secure multi-party computation
• Verifying Secure Speculation in Isabelle/HOL
• scientific article; zbMATH DE number 2090144
• General composition and universal composability in secure multiparty computation
• Secure two-party computation in applied pi-calculus: models and verification
• Formalizing provable anonymity in Isabelle/HOL
• scientific article; zbMATH DE number 2086504

zbMATH Keywords

cryptographyoblivious transferformal verificationsimulation-based proof

Mathematics Subject Classification ID

Cryptography (94A60) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Formal certification of code-based cryptographic proofs
• New directions in cryptography
• A proof of security of Yao's protocol for two-party computation
• Efficient oblivious transfer protocols
• Computer-Aided Security Proofs for the Working Cryptographer
• On the security of public key protocols
• Title not available (Why is that?)
• Efficient constant round multi-party computation combining BMR and SPDZ
• Probabilistic functions and cryptographic oracles in higher order logic
• How to simulate it -- a tutorial on the simulation proof technique

Cited In (3)

• Computationally sound abstraction and verification of secure multi-party computations
• Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
• CryptHOL: game-based proofs in higher-order logic

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Sharemind
• CryptHOL
• ObliVM
• ABY

This page was built for publication: How to simulate it in Isabelle: towards formal proof for secure multi-party computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687724)