{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T17:21:48Z","timestamp":1749921708308,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_8","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"114-130","source":"Crossref","is-referenced-by-count":9,"title":["How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation"],"prefix":"10.1007","author":[{"given":"David","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adri\u00e0","family":"Gasc\u00f3n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s00145-007-0203-0","volume":"20","author":"M Abadi","year":"2007","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 20(3), 395 (2007)","journal-title":"J. Cryptol."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101. ACM (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22792-9_5"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Schmidt, B.: Automated proofs of pairing-based cryptography. In: ACM Conference on Computer and Communications Security, pp. 1156\u20131168. ACM (2015)","DOI":"10.1145\/2810103.2813697"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-46766-1_34","volume-title":"Advances in Cryptology \u2014 CRYPTO \u201991","author":"D Beaver","year":"1992","unstructured":"Beaver, D.: Efficient multiparty protocols using circuit randomization. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 420\u2013432. Springer, Heidelberg (1992). doi:10.1007\/3-540-46766-1_34"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-46766-1_29","volume-title":"Advances in Cryptology \u2014 CRYPTO \u201991","author":"CH Bennett","year":"1992","unstructured":"Bennett, C.H., Brassard, G., Cr\u00e9peau, C., Skubiszewska, M.-H.: Practical quantum oblivious transfer. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 351\u2013366. Springer, Heidelberg (1992). doi:10.1007\/3-540-46766-1_29"},{"issue":"4","key":"8_CR7","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TDSC.2007.1005","volume":"5","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secur. Comput. 5(4), 193\u2013207 (2008)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-540-88313-5_13","volume-title":"Computer Security - ESORICS 2008","author":"D Bogdanov","year":"2008","unstructured":"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\u2013206. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-88313-5_13"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Demmler, D., Schneider, T., Zohner, M.: ABY - a framework for efficient mixed-protocol secure two-party computation. In: NDSS. The Internet Society (2015)","DOI":"10.14722\/ndss.2015.23113"},{"issue":"6","key":"8_CR10","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013207 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013229. ACM (1987)","DOI":"10.1145\/28395.28420"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013842. ACM (2016)","DOI":"10.1145\/2976749.2978357"},{"key":"8_CR14","unstructured":"Lindell, Y.: How to simulate it - a tutorial on the simulation proof technique. IACR Cryptology ePrint Archive 2016:46 (2016)"},{"issue":"2","key":"8_CR15","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s00145-008-9036-8","volume":"22","author":"Y Lindell","year":"2009","unstructured":"Lindell, Y., Pinkas, B.: A proof of security of Yao\u2019s protocol for two-party computation. J. Cryptol. 22(2), 161\u2013188 (2009)","journal-title":"J. Cryptol."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-48000-7_16","volume-title":"Advances in Cryptology \u2013 CRYPTO 2015","author":"Y Lindell","year":"2015","unstructured":"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\u2013338. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48000-7_16"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013376. IEEE Computer Society (2015)","DOI":"10.1109\/SP.2015.29"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-662-49498-1_20","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2016","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503\u2013531. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49498-1_20"},{"key":"8_CR19","unstructured":"Naor, M., Pinkas, B.: Efficient oblivious transfer protocols. In: SODA, pp. 448\u2013457. ACM\/SIAM (2001)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-662-46666-7_4","volume-title":"Principles of Security and Trust","author":"A Petcher","year":"2015","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53\u201372. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46666-7_4"},{"key":"8_CR21","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004:332 (2004)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Yao, A.: How to generate and exchange secrets (extended abstract). In: FOCS, pp. 162\u2013167. IEEE Computer Society (1986)","DOI":"10.1109\/SFCS.1986.25"},{"key":"8_CR23","unstructured":"Zahur, S., Evans, D.: Obliv-C: a language for extensible data-oblivious computation. IACR Cryptology ePrint Archive 2015:1153 (2015)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:05:48Z","timestamp":1664431548000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}