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

David Butler, David Aspinall, Adria Gascón

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 aw 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 simulation approach, in which security is established by showing indistinguishability between execution traces in the actual protocol executionand an ideal world where security is guaranteed by definition. We show that existing machinery for reasoning about probabilistic programs can be 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.
Original languageEnglish
Title of host publicationInteractive Theorem Proving
Subtitle of host publicationITP 2017
Place of Publication978-3-319-66106-3
PublisherSpringer, Cham
Pages114-130
Number of pages17
ISBN (Electronic)978-3-319-66107-0
DOIs
Publication statusPublished - 21 Aug 2017
Event8th International Conference on Interactive Theorem Proving 2017 - Brasilia, Brazil
Duration: 26 Sep 201729 Sep 2017
http://itp2017.cic.unb.br/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume10499
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Conference on Interactive Theorem Proving 2017
Abbreviated titleITP 2017
Country/TerritoryBrazil
CityBrasilia
Period26/09/1729/09/17
Internet address

Fingerprint

Dive into the research topics of 'How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation'. Together they form a unique fingerprint.

Cite this