{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:31:58Z","timestamp":1757626318419,"version":"3.44.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031954962"},{"type":"electronic","value":"9783031954979"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-95497-9_11","type":"book-chapter","created":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T13:15:37Z","timestamp":1749906937000},"page":"182-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Approach to\u00a0Formalize Information-Theoretic Security of\u00a0Multiparty Computation Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-2752-1490","authenticated-orcid":false,"given":"Cheng-Hui","family":"Weng","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2327-953X","authenticated-orcid":false,"given":"Reynald","family":"Affeldt","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8056-5519","authenticated-orcid":false,"given":"Jacques","family":"Garrigue","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4492-745X","authenticated-orcid":false,"given":"Takafumi","family":"Saikawa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,11]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Reasoning with conditional probabilities and joint distributions in Coq. Comput. Softw. 37(3), 79\u201395 (2020). https:\/\/doi.org\/10.11309\/jssst.37.3_79","DOI":"10.11309\/jssst.37.3_79"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: A practical formalization of monadic equational reasoning in dependent-type theory. J. Funct. Program. 35 (2025). https:\/\/doi.org\/10.1017\/S0956796824000157","DOI":"10.1017\/S0956796824000157"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-04444-1_26","volume-title":"Computer Security \u2013 ESORICS 2009","author":"M Barni","year":"2009","unstructured":"Barni, M., Failla, P., Kolesnikov, V., Lazzeretti, R., Sadeghi, A.-R., Schneider, T.: Secure evaluation of private linear branching programs with medical applications. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 424\u2013439. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04444-1_26"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Lochbihler, A., Sefidgar, S.R.: CryptHOL: game-based proofs in higher-order logic. J. Cryptol. 33(2), 494\u2013566 (2020). https:\/\/doi.org\/10.1007\/S00145-019-09341-Z","DOI":"10.1007\/S00145-019-09341-Z"},{"issue":"2","key":"11_CR5","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/s000370050025","volume":"8","author":"C Blundo","year":"1999","unstructured":"Blundo, C., De Santis, A., Persiano, G., Vaccaro, U.: Randomness complexity of private computation. Comput. Complex. 8(2), 145\u2013168 (1999). https:\/\/doi.org\/10.1007\/s000370050025","journal-title":"Comput. Complex."},{"key":"11_CR6","unstructured":"Boutillier, P., et al.: Rocq 9.0 reference manual - the ring and field tactic families (2025). https:\/\/rocq-prover.org\/doc\/v9.0\/refman\/addendum\/ring.html"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-66107-0_8","volume-title":"Interactive Theorem Proving","author":"D Butler","year":"2017","unstructured":"Butler, D., Aspinall, D., Gasc\u00f3n, A.: How to simulate it in Isabelle: towards formal proof for secure multi-party computation. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 114\u2013130. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_8"},{"key":"11_CR8","unstructured":"Chen, K., Hsu, T.S., Huang, W.K., Liau, C.J., Wang, D.W.: Towards a scripting language for automating secure multiparty computation. In: First Asia-Pacific Programming Languages and Compilers Workshop (APPLC 2012), Beijing, China, 14 June 2012 (2012)"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Du, W., Zhan, J.Z.: A practical approach to solve secure multi-party computation problems. In: Workshop on New Security Paradigms (NSPW 2002), Virginia Beach, VA, USA, 23\u201326 September 2002, pp. 127\u2013135. ACM (2002). https:\/\/doi.org\/10.1145\/844102.844125","DOI":"10.1145\/844102.844125"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/J.COSE.2017.04.013","volume":"71","author":"J Dumas","year":"2017","unstructured":"Dumas, J., Lafourcade, P., Orfila, J., Puys, M.: Dual protocols for private multi-party matrix multiplication and trust computations. Comput. Secur. 71, 51\u201370 (2017). https:\/\/doi.org\/10.1016\/J.COSE.2017.04.013","journal-title":"Comput. Secur."},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Helminger, L., Rechberger, C.: Multi-party computation in the GDPR. In: Privacy Symposium 2022\u2014Data Protection Law International Convergence and Compliance with Innovative Technologies, pp. 21\u201339. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-09901-4_2","DOI":"10.1007\/978-3-031-09901-4_2"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Iwamoto, M.: Information-theoretic perspectives for simulation-based security in multi-party computation. IEICE Trans. Fund. E107-A(3), 360\u2013372 (2024). https:\/\/doi.org\/10.1587\/transfun.2023TAI0001","DOI":"10.1587\/transfun.2023TAI0001"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Lindell, Y.: Secure computation for privacy preserving data mining. In: Wang, J. (ed.) Encyclopedia of Data Warehousing and Mining, 2nd edn, vol. 4, pp. 1747\u20131752. IGI Global (2009). http:\/\/www.igi-global.com\/Bookstore\/Chapter.aspx?TitleId=11054","DOI":"10.4018\/978-1-60566-010-3.ch266"},{"key":"11_CR14","volume-title":"Communicating and Mobile Systems: The $$\\pi $$-Calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: The $$\\pi $$-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Naor, M., Pinkas, B., Sumner, R.: Privacy preserving auctions and mechanism design. In: First ACM Conference on Electronic Commerce (EC-99), Denver, CO, USA, 3\u20135 November 1999, pp. 129\u2013139. ACM (1999). https:\/\/doi.org\/10.1145\/336992.337028","DOI":"10.1145\/336992.337028"},{"key":"11_CR16","unstructured":"Pearl, J., Paz, A.: GRAPHOIDS: a graph-based logic for reasoning about relevance relations. Technical Report. R-53 CSD-850038, UCLA Computer Science Department (1985)"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Rogers, J., et\u00a0al.: VaultDB: a real-world pilot of secure multi-party computation within a clinical research network. arXiv preprint arXiv:2203.00146 (2022). https:\/\/doi.org\/10.48550\/arXiv.2203.00146","DOI":"10.48550\/arXiv.2203.00146"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-14423-3_16","volume-title":"Information, Security and Cryptology \u2013 ICISC 2009","author":"A-R Sadeghi","year":"2010","unstructured":"Sadeghi, A.-R., Schneider, T., Wehrenberg, I.: Efficient privacy-preserving face recognition. In: Lee, D., Hong, S. (eds.) ICISC 2009. LNCS, vol. 5984, pp. 229\u2013244. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14423-3_16"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Shen, C.H., Zhan, J., Hsu, T.S., Liau, C.J., Wang, D.W.: Scalar-product based secure two-party computation. In: 2008 IEEE International Conference on Granular Computing, pp. 556\u2013561 (2008). https:\/\/doi.org\/10.1109\/GRC.2008.4664775","DOI":"10.1109\/GRC.2008.4664775"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Shen, C.H., Zhan, J., Wang, D.W., Hsu, T.S., Liau, C.J.: Information-theoretically secure number-product protocol. In: 2007 International Conference on Machine Learning and Cybernetics, vol.\u00a05, pp. 3006\u20133011 (2007). https:\/\/doi.org\/10.1109\/ICMLC.2007.4370663","DOI":"10.1109\/ICMLC.2007.4370663"},{"key":"11_CR21","unstructured":"Tassi, E.: Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi $$\\lambda $$Prolog dialect). In: The Fourth International Workshop on Coq for Programming Languages (2018)"},{"key":"11_CR22","unstructured":"The Rocq Development Team: The Rocq Proof Assistant Reference Manual. Inria (2024). https:\/\/coq.inria.fr. Version 8.20.0"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Wang, H., Li, Z., Ge, C., Susilo, W.: ABG: a multi-party mixed protocol framework for privacy-preserving cooperative learning. arXiv preprint arXiv:2202.02928 (2022). https:\/\/doi.org\/10.48550\/arXiv.2202.02928","DOI":"10.48550\/arXiv.2202.02928"},{"key":"11_CR24","unstructured":"Weng, C.H., Affeldt, R., Garrigue, J., Saikawa, T.: Formalization for the SMC scalar product protocol (2024). https:\/\/github.com\/affeldt-aist\/infotheo\/pull\/138"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Yao, A.C.: Protocols for secure computations (extended abstract). In: 23rd Annual Symposium on Foundations of Computer Science, Chicago, Illinois, USA, 3\u20135 November 1982, pp. 160\u2013164. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SFCS.1982.38","DOI":"10.1109\/SFCS.1982.38"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Yao, A.C.: How to generate and exchange secrets (extended abstract). In: 27th Annual Symposium on Foundations of Computer Science, Toronto, Canada, 27\u201329 October 1986, pp. 162\u2013167. IEEE Computer Society (1986). https:\/\/doi.org\/10.1109\/SFCS.1986.25","DOI":"10.1109\/SFCS.1986.25"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-030-36987-3_5","volume-title":"Distributed Computing and Internet Technology","author":"N Yoshida","year":"2020","unstructured":"Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: Hung, D.V., D\u2019Souza, M. (eds.) ICDCIT 2020. LNCS, vol. 11969, pp. 73\u201393. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-36987-3_5"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-95497-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T21:43:53Z","timestamp":1757454233000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-95497-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031954962","9783031954979"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-95497-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"11 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"45","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}