{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T09:10:10Z","timestamp":1746522610875,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911200"},{"type":"electronic","value":"9783031911217"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications.\u00a0We develop a new type theory to automatically enforce correctness, confidentiality, and integrity properties of protocols written\u00a0in the <jats:italic>Prelude\/Overture<\/jats:italic> language framework. Judgements in\u00a0the type theory are predicated on SMT verifications in a theory\u00a0of finite fields, which supports precise and efficient analysis.\u00a0Our approach is automated, compositional, scalable, and generalizes to arbitrary prime fields for data and key sizes.<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_11","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:51:29Z","timestamp":1746190289000},"page":"258-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SMT-Boosted Security Types for Low-Level MPC"],"prefix":"10.1007","author":[{"given":"Christian","family":"Skalka","sequence":"first","affiliation":[]},{"given":"Joseph P.","family":"Near","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"A probabilistic separation logic. Proc. ACM Program. Lang. 4(POPL) (dec 2019). https:\/\/doi.org\/10.1145\/3371123","DOI":"10.1145\/3371123"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Acay, C., Gancher, J., Recto, R., Myers, A.: Secure synthesis of distributed cryptographic applications. In: 2024 IEEE 37th Computer Security Foundations Symposium (CSF). pp. 315\u2013330. IEEE Computer Society, Los Alamitos, CA, USA (jul 2024). https:\/\/doi.org\/10.1109\/CSF61375.2024.00021, https:\/\/doi.ieeecomputersociety.org\/10.1109\/CSF61375.2024.00021","DOI":"10.1109\/CSF61375.2024.00021"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Acay, C., Recto, R., Gancher, J., Myers, A.C., Shi, E.: Viaduct: An extensible, optimizing compiler for secure distributed programs. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 740\u2013755. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021https:\/\/doi.org\/10.1145\/3453483.3454074","DOI":"10.1145\/3453483.3454074"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Pacheco, H., Pereira, V., Portela, B.: Enforcing ideal-world leakage bounds in real-world secret sharing mpc frameworks. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). pp. 132\u2013146. IEEE (2018)","DOI":"10.1109\/CSF.2018.00017"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Bendlin, R., Damg\u00e5rd, I., Orlandi, C., Zakarias, S.: Semi-homomorphic encryption and multiparty computation. In: Paterson, K.G. (ed.) Advances in Cryptology \u2013 EUROCRYPT 2011. pp. 169\u2013188. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-20465-4_11"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Bogdanov, D., Laud, P., Randmets, J.: Domain-polymorphic programming of privacy-preserving applications. In: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security. pp. 53\u201365. PLAS\u201914, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2637113.2637119","DOI":"10.1145\/2637113.2637119"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Damg\u00e5rd, I., Orlandi, C.: Multiparty computation for dishonest majority: From passive to active security at low cost. In: Rabin, T. (ed.) Advances in Cryptology \u2013 CRYPTO 2010. pp. 558\u2013576. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14623-7_30"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Damg\u00e5rd, I., Pastro, V., Smart, N., Zakarias, S.: Multiparty computation from somewhat homomorphic encryption. In: Safavi-Naini, R., Canetti, R. (eds.) Advances in Cryptology \u2013 CRYPTO 2012. pp. 643\u2013662. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-32009-5_38"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Darais, D., Sweet, I., Liu, C., Hicks, M.: A language for probabilistically oblivious computation. Proceedings of the ACM on Programming Languages 4(POPL), 1\u201331 (2019)","DOI":"10.1145\/3371118"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing semantic models of programs with the software analysis workbench. In: Blazy, S., Chechik, M. (eds.) Verified Software. Theories, Tools, and Experiments. pp. 56\u201372. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-48869-1_5"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Evans, D., Kolesnikov, V., Rosulek, M., et\u00a0al.: A pragmatic introduction to secure multi-party computation. Foundations and Trends\u00ae in Privacy and Security 2(2-3), 70\u2013246 (2018)","DOI":"10.1561\/3300000019"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Gao, S., Peng, Z., Tan, F., Zheng, Y., Xiao, B.: Symmeproof: Compact zero-knowledge argument for blockchain confidential transactions. IEEE Transactions on Dependable and Secure Computing (2022)","DOI":"10.1109\/TDSC.2022.3179913"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., Strub, P.: Computer-aided proofs for multiparty computation with active security. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). pp. 119\u2013131. IEEE Computer Society, Los Alamitos, CA, USA (jul 2018). https:\/\/doi.org\/10.1109\/CSF.2018.00016, https:\/\/doi.ieeecomputersociety.org\/10.1109\/CSF.2018.00016","DOI":"10.1109\/CSF.2018.00016"},{"issue":"3","key":"11_CR14","doi-asserted-by":"publisher","first-page":"1121","DOI":"10.1137\/080725398","volume":"39","author":"Y Ishai","year":"2009","unstructured":"Ishai, Y., Kushilevitz, E., Ostrovsky, R., Sahai, A.: Zero-knowledge proofs from secure multiparty computation. SIAM Journal on Computing 39(3), 1121\u20131152 (2009)","journal-title":"SIAM Journal on Computing"},{"key":"11_CR15","unstructured":"Knott, B., Venkataraman, S., Hannun, A., Sengupta, S., Ibrahim, M., van\u00a0der Maaten, L.: Crypten: Secure multi-party computation meets machine learning. Advances in Neural Information Processing Systems 34, 4961\u20134973 (2021)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Koch, K., Krenn, S., Pellegrino, D., Ramacher, S.: Privacy-preserving analytics for data markets using mpc. In: IFIP International Summer School on Privacy and Identity Management, pp. 226\u2013246. Springer (2020)","DOI":"10.1007\/978-3-030-72465-8_13"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Li, J.M., Ahmed, A., Holtzen, S.: Lilac: a modal separation logic for conditional probability. Proceedings of the ACM on Programming Languages 7(PLDI), 148\u2013171 (2023)","DOI":"10.1145\/3591226"},{"key":"11_CR18","unstructured":"Li, X., Dowsley, R., De\u00a0Cock, M.: Privacy-preserving feature selection with secure multiparty computation. In: International Conference on Machine Learning. pp. 6326\u20136336. PMLR (2021)"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Lindell, Y.: How to Simulate It \u2013 A Tutorial on the Simulation Proof Technique, pp. 277\u2013346. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57048-8_6, https:\/\/doi.org\/10.1007\/978-3-319-57048-8_6","DOI":"10.1007\/978-3-319-57048-8_6"},{"key":"11_CR20","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1016\/j.comcom.2020.02.014","volume":"153","author":"J Liu","year":"2020","unstructured":"Liu, J., Tian, Y., Zhou, Y., Xiao, Y., Ansari, N.: Privacy preserving distributed data mining based on secure multi-party computation. Computer Communications 153, 208\u2013216 (2020)","journal-title":"Computer Communications"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Lu, D., Yurek, T., Kulshreshtha, S., Govind, R., Kate, A., Miller, A.: Honeybadgermpc and asynchromix: Practical asynchronous mpc and its application to anonymous communication. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. pp. 887\u2013903 (2019)","DOI":"10.1145\/3319535.3354238"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Mitchell, J.C., Sharma, R., Stefan, D., Zimmerman, J.: Information-flow control for programming on encrypted data. In: 2012 IEEE 25th Computer Security Foundations Symposium. pp. 45\u201360 (2012). https:\/\/doi.org\/10.1109\/CSF.2012.30","DOI":"10.1109\/CSF.2012.30"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Orsini, E.: Efficient, actively secure MPC with a dishonest majority: A survey. In: Bajard, J.C., Topuzo\u011flu, A. (eds.) Arithmetic of Finite Fields. pp. 42\u201371. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-68869-1_3"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C.: Satisfiability modulo finite fields. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 163\u2013186. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_8"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Rastogi, A., Hammer, M.A., Hicks, M.: Wysteria: A programming language for generic, mixed-mode multiparty computations. In: 2014 IEEE Symposium on Security and Privacy. pp. 655\u2013670. IEEE (2014)","DOI":"10.1109\/SP.2014.48"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Rastogi, A., Swamy, N., Hicks, M.: Wys*: A DSL for verified secure multi-party computations. In: Nielson, F., Sands, D. (eds.) 8th International Conference on Principles of Security and Trust (POST). Lecture Notes in Computer Science, vol. 11426, pp. 99\u2013122. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17138-4_5","DOI":"10.1007\/978-3-030-17138-4_5"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. J. Comput. Secur. 17(5), 517\u2013548 (oct 2009)","DOI":"10.3233\/JCS-2009-0352"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Skalka, C., Near, J.P.: Language-based security for low-level MPC. In: Proceedings of the ACM Conference on Principles and Practice of Declarative Programming (2024)","DOI":"10.1145\/3678232.3678246"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Skalka, C., Near, J.P.: Smt-boosted security types for low-level mpc (2025). https:\/\/arxiv.org\/abs\/2501.17824","DOI":"10.1007\/978-3-031-91121-7_11"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Tomaz, A.E.B., Do\u00a0Nascimento, J.C., Hafid, A.S., De\u00a0Souza, J.N.: Preserving privacy in mobile health systems using non-interactive zero-knowledge proof and blockchain. IEEE access 8, 204441\u2013204458 (2020)","DOI":"10.1109\/ACCESS.2020.3036811"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Ye, Q., Delaware, B.: Oblivious algebraic data types. Proc. ACM Program. Lang. 6(POPL) (jan 2022). https:\/\/doi.org\/10.1145\/3498713","DOI":"10.1145\/3498713"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:35:26Z","timestamp":1746520526000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_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":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}