The Library
How to simulate it in Isabelle : towards formal proof for secure multi-party computation
Tools
Tools
Tools
Butler, David, Aspinall, David and Gascon, Adrià (2017) How to simulate it in Isabelle : towards formal proof for secure multi-party computation. In: Ayala-Rincón, M. and Muñoz, C., (eds.) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science, 10499 . Cham: Springer, pp. 114-130. ISBN 9783319661063
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: https://doi.org/10.1007/978-3-319-66107-0
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 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 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.
| Item Type: | Book Item | ||||||
|---|---|---|---|---|---|---|---|
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
| Series Name: | Lecture Notes in Computer Science | ||||||
| Publisher: | Springer | ||||||
| Place of Publication: | Cham | ||||||
| ISBN: | 9783319661063 | ||||||
| Book Title: | Interactive Theorem Proving. ITP 2017 | ||||||
| Editor: | Ayala-Rincón, M. and Muñoz, C. | ||||||
| Official Date: | 21 August 2017 | ||||||
| Dates: |
|
||||||
| Volume: | 10499 | ||||||
| Page Range: | pp. 114-130 | ||||||
| DOI: | 10.1007/978-3-319-66107-0 | ||||||
| Status: | Peer Reviewed | ||||||
| Publication Status: | Published | ||||||
| Conference Paper Type: | Paper | ||||||
| Title of Event: | Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings | ||||||
| Type of Event: | Conference |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
