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.
This work was supported by The Alan Turing Institute under the EPSRC grant EP/N510129/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A negligible function is a function \(\epsilon \; {:}{:} \; \mathbb {N} \rightarrow \mathbb {R}\) such that for all \(c \in \mathbb {N}\) there exists \(N_c \in \mathbb {N}\) such that for all \(x > N_c\) we have \(|\epsilon (x)| < \frac{1}{x^c}\).
References
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 20(3), 395 (2007)
Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90–101. ACM (2009)
Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22792-9_5
Barthe, G., Grégoire, B., Schmidt, B.: Automated proofs of pairing-based cryptography. In: ACM Conference on Computer and Communications Security, pp. 1156–1168. ACM (2015)
Beaver, D.: Efficient multiparty protocols using circuit randomization. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 420–432. Springer, Heidelberg (1992). doi:10.1007/3-540-46766-1_34
Bennett, C.H., Brassard, G., Crépeau, C., Skubiszewska, M.-H.: Practical quantum oblivious transfer. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 351–366. Springer, Heidelberg (1992). doi:10.1007/3-540-46766-1_29
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secur. Comput. 5(4), 193–207 (2008)
Bogdanov, D., Laur, S., Willemson, J.: Sharemind: a framework for fast privacy-preserving computations. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 192–206. Springer, Heidelberg (2008). doi:10.1007/978-3-540-88313-5_13
Demmler, D., Schneider, T., Zohner, M.: ABY - a framework for efficient mixed-protocol secure two-party computation. In: NDSS. The Internet Society (2015)
Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644–654 (1976)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)
Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game or a completeness theorem for protocols with honest majority. In: STOC, pp. 218–229. ACM (1987)
Keller, M., Orsini, E., Scholl, P.: MASCOT: faster malicious arithmetic secure computation with oblivious transfer. In: ACM Conference on Computer and Communications Security, pp. 830–842. ACM (2016)
Lindell, Y.: How to simulate it - a tutorial on the simulation proof technique. IACR Cryptology ePrint Archive 2016:46 (2016)
Lindell, Y., Pinkas, B.: A proof of security of Yao’s protocol for two-party computation. J. Cryptol. 22(2), 161–188 (2009)
Lindell, Y., Pinkas, B., Smart, N.P., Yanai, A.: Efficient constant round multi-party computation combining BMR and SPDZ. In: Gennaro, R., Robshaw, M. (eds.) CRYPTO 2015. LNCS, vol. 9216, pp. 319–338. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48000-7_16
Liu, C., Wang, X.S., Nayak, K., Huang, Y., Shi, E.: ObliVM: a programming framework for secure computation. In: IEEE Symposium on Security and Privacy, pp. 359–376. IEEE Computer Society (2015)
Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503–531. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1_20
Naor, M., Pinkas, B.: Efficient oblivious transfer protocols. In: SODA, pp. 448–457. ACM/SIAM (2001)
Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53–72. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46666-7_4
Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004:332 (2004)
Yao, A.: How to generate and exchange secrets (extended abstract). In: FOCS, pp. 162–167. IEEE Computer Society (1986)
Zahur, S., Evans, D.: Obliv-C: a language for extensible data-oblivious computation. IACR Cryptology ePrint Archive 2015:1153 (2015)
Acknowledgements
We are deeply grateful to Andreas Lochbihler for providing and continuing to develop CryptHOL and for his kind help given with using it. Also we are thankful to the reviewers for their comments regarding the presentation of our work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Butler, D., Aspinall, D., Gascón, A. (2017). How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-66107-0_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66106-3
Online ISBN: 978-3-319-66107-0
eBook Packages: Computer ScienceComputer Science (R0)