{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:40:12Z","timestamp":1750297212308,"version":"3.41.0"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,12,31]],"date-time":"2024-12-31T00:00:00Z","timestamp":1735603200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"crossref","award":["N00014-18-1-2620"],"award-info":[{"award-number":["N00014-18-1-2620"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"crossref"}]},{"name":"German Federal Ministry of Education and Research","award":["FKZ: 13N1S0762"],"award-info":[{"award-number":["FKZ: 13N1S0762"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2024,12,31]]},"abstract":"<jats:p>\n            This article discusses the relationship between two frameworks: universal composability (\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            ) and robust compilation (\n            <jats:italic>RC<\/jats:italic>\n            ). In cryptography,\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee:\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            protocols remain secure even when composed with other protocols. In programming language security,\n            <jats:italic>RC<\/jats:italic>\n            is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields.\n          <\/jats:p>\n          <jats:p>\n            This article formally proves the connection between\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            and\n            <jats:italic>RC<\/jats:italic>\n            and then it explores the benefits of this connection (focussing on perfect, rather than computational\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            ). For this, this article first identifies which conditions must programming languages fulfil in order to possibly attain\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            -like composition. Then, it proves\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            of both an existing and a new commitment protocol as a corollary of the related compilers attaining\n            <jats:italic>RC<\/jats:italic>\n            . Finally, it mechanises these proofs in DEEPSEC, obtaining symbolic guarantees that the protocol is indeed\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            .\n          <\/jats:p>\n          <jats:p>\n            Our connection lays the groundwork towards a better and deeper understanding of both\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            and\n            <jats:italic>RC<\/jats:italic>\n            , and the benefits we showcase from this connection provide evidence of scalable mechanised proofs for\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{UC}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            .\n          <\/jats:p>","DOI":"10.1145\/3698234","type":"journal-article","created":{"date-parts":[[2024,10,10]],"date-time":"2024-10-10T15:44:09Z","timestamp":1728575049000},"page":"1-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Universal Composability Is Robust Compilation"],"prefix":"10.1145","volume":"46","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3411-9678","authenticated-orcid":false,"given":"Marco","family":"Patrignani","sequence":"first","affiliation":[{"name":"DISI, University of Trento, Trento, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0822-9283","authenticated-orcid":false,"given":"Robert","family":"K\u00fcnnemann","sequence":"additional","affiliation":[{"name":"CISPA Helmholz Center for Information Security, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0224-1989","authenticated-orcid":false,"given":"Riad S.","family":"Wahby","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7900-8328","authenticated-orcid":false,"given":"Ethan","family":"Cecchetti","sequence":"additional","affiliation":[{"name":"University of Wisconsin\u2013Madison, Madison, WI, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,12,31]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/646252.686313"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90168-H"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360213"},{"key":"e_1_3_2_7_2","first-page":"105","volume-title":"Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS \u201998)","author":"Abadi Mart\u00edn","year":"1998","unstructured":"Mart\u00edn Abadi, C\u00e9dric Fournet, and Georges Gonthier. 1998. Secure Implementation of Channel Abstractions. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS \u201998), 105\u2013116."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325734"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3086"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2240276.2240279"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243745"},{"key":"e_1_3_2_13_2","first-page":"1","volume-title":"Proceedings of 29th European Symposium on Programming Languages and Systems (ESOP \u201920)","author":"Abate Carmine","year":"2020","unstructured":"Carmine Abate, Roberto Blanco, \u015etefan Ciob\u00e2c\u0103, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, \u00c9ric Tanter, and Jeremy J\u00e9r\u00e9my. 2020. Trace-Relating Compiler Correctness and Secure Compilation. In Proceedings of 29th European Symposium on Programming Languages and Systems (ESOP \u201920), 1\u201328. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-030-44914-8_1"},{"issue":"4","key":"e_1_3_2_14_2","first-page":"14","article-title":"An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation","volume":"43","author":"Abate Carmine","year":"2021","unstructured":"Carmine Abate, Roberto Blanco, \u015etefan Ciob\u00e2c\u0103, Adrien Durier, Deepak Garg, C\u0103t\u0103lin Hri\u0163cu, Marco Patrignani, \u00c9ric Tanter, and J\u00e9r\u00e9my Thibault. 2021. An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation. ACM Transactions on Programming Languages and Systems 43, 4, Article 14 (Nov. 2021), 48 pages. DOI: http:\/\/dx.doi.org\/10.1145\/3460860","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_15_2","volume-title":"Proceedings of 2019 IEEE 32nd Computer Security Foundations Symposium (CSF 2019)","author":"Abate Carmine","year":"2019","unstructured":"Carmine Abate, Roberto Blanco, Deepak Garg, C\u0103t\u0103lin Hri\u0163cu, Marco Patrignani, and J\u00e9r\u00e9my Thibault. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In Proceedings of 2019 IEEE 32nd Computer Security Foundations Symposium (CSF 2019)."},{"key":"e_1_3_2_16_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-030-89051-3_6","volume-title":"Proceedings of 19th Asian Symposium on Programming Languages and Systems (APLAS \u201921)","volume":"13008","author":"Abate Carmine","year":"2021","unstructured":"Carmine Abate, Matteo Busi, and Stelios Tsampas. 2021. Fully Abstract and Robust Compilation: And How to Reconcile the Two, Abstractly. In Proceedings of 19th Asian Symposium on Programming Languages and Systems (APLAS \u201921). Hakjoo Oh (Ed.), Lecture Notes in Computer Science, Vol. 13008, Springer, 83\u2013101. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-030-89051-3_6"},{"key":"e_1_3_2_17_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/978-3-030-56784-2_10","volume-title":"Proceedings of 40th Annual Cryptology Conference Advances in Cryptology (CRYPTO \u201920)","author":"Abdalla Michel","year":"2020","unstructured":"Michel Abdalla, Manuel Barbosa, Tatiana Bradley, Stanisaw Jarecki, Jonathan Katz, and Jiayu Xu. 2020. Universally Composable Relaxed Password Authenticated Key Exchange. In Proceedings of 40th Annual Cryptology Conference Advances in Cryptology (CRYPTO \u201920). Daniele Micciancio and Thomas Ristenpart (Eds.), Lecture Notes in Computer Science, Springer International Publishing, Cham, 278\u2013307. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-030-56784-2_10"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454074"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105"},{"key":"e_1_3_2_20_2","first-page":"157","volume-title":"Proceedings of International Conference on Functional Programming","author":"Ahmed Amal","year":"2008","unstructured":"Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In Proceedings of International Conference on Functional Programming. ACM, 157\u2013168."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046745"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978418"},{"key":"e_1_3_2_24_2","author":"Backes Michael","year":"2004","unstructured":"Michael Backes, Birgit Pfitzmann, and Michael Waidner. 2004. Secure Asynchronous Reactive Systems. Technical Report 082.","journal-title":"Secure Asynchronous Reactive Systems"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.002"},{"key":"e_1_3_2_26_2","volume-title":"In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S & P \u201921)","author":"Baelde David","year":"2021","unstructured":"David Baelde, St\u00e9phanie Delaune, Charlie Jacomme, Adrien Koutsos, and Sol\u00e8ne Moreau. 2021. An Interactive Prover for Protocol Verification in the Computational Model. In In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S & P \u201921)."},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1109\/SP40001.2021.00008","volume-title":"Proceedings of 2021 IEEE Symposium on Security and Privacy (SP)","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In Proceedings of 2021 IEEE Symposium on Security and Privacy (SP), 777\u2013795. DOI: http:\/\/dx.doi.org\/10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484548"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/2033036.2033043"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/CSF.2019.00017","volume-title":"Proceedings of 2019 IEEE 32nd Computer Security Foundations Symposium (CSF)","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, Charlie Jacomme, Steve Kremer, and Pierre-Yves Strub. 2019. Symbolic Methods in Computational Cryptography Proofs. In Proceedings of 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 136\u2013115. DOI: http:\/\/dx.doi.org\/10.1109\/CSF.2019.00017"},{"key":"e_1_3_2_31_2","first-page":"1","volume-title":"2021 IEEE 34th Computer Security Foundations Symposium (CSF)","author":"Basin David","year":"2021","unstructured":"David Basin, Andreas Lochbihler, Ueli Maurer, and S. Reza Sefidgar. 2021. Abstract Modeling of System Communication in Constructive Cryptography Using CryptHOL. In 2021 IEEE 34th Computer Security Foundations Symposium (CSF), 1\u201316. DOI: http:\/\/dx.doi.org\/10.1109\/CSF51468.2021.00047"},{"key":"e_1_3_2_32_2","author":"Bellare Mihir","year":"2004","unstructured":"Mihir Bellare and Phillip Rogaway. 2004. The Game-Playing Technique. Technical Report.","journal-title":"The Game-Playing Technique"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1109\/CSF.2013.24","volume-title":"Proceedings of 2013 IEEE 26th Computer Security Foundations Symposium","author":"B\u00f6hl Florian","year":"2013","unstructured":"Florian B\u00f6hl and Dominique Unruh. 2013. Symbolic Universal Composability. In Proceedings of 2013 IEEE 26th Computer Security Foundations Symposium, 257\u2013271. DOI: http:\/\/dx.doi.org\/10.1109\/CSF.2013.24"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784733"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477314.3507084"},{"key":"e_1_3_2_37_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-030-34618-8_7","volume-title":"Proceedings of 25th International Conference on the Theory and Application of Cryptology and Information Security, Advances in Cryptology (ASIACRYPT \u201919)","volume":"11923","author":"Camenisch Jan","year":"2019","unstructured":"Jan Camenisch, Stephan Krenn, Ralf K\u00fcsters, and Daniel Rausch. 2019. iUC: Flexible Universal Composability Made Simple. In Proceedings of 25th International Conference on the Theory and Application of Cryptology and Information Security, Advances in Cryptology (ASIACRYPT \u201919), Lecture Notes in Computer Science, Vol. 11923, Springer, 191\u2013221."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2001.959888"},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/SFCS.2001.959888","volume-title":"Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science (FOCS \u201901)","author":"Ran Canetti","year":"2001","unstructured":"Ran Canetti. 2001. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science (FOCS \u201901). IEEE Computer Society, 136. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=874063.875553"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3402457"},{"key":"e_1_3_2_41_2","unstructured":"Ran Canetti Asaf Cohen and Yehuda Lindell. 2014. A Simpler Variant of Universally Composable Security for Standard Multiparty Computation. Cryptology ePrint Archive Report 2014\/553. Retrieved from https:\/\/eprint.iacr.org\/2014\/553"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/646766.704151"},{"key":"e_1_3_2_43_2","first-page":"78","volume-title":"Proceedings of 42nd Annual International Cryptology Conference (CRYPTO\u201922)","author":"Canetti Ran","unstructured":"Ran Canetti, Palak Jain, Marika Swanberg, and Mayank Varia. Universally Composable End-to-End Secure Messaging: A Modular Analysis. In Proceedings of 42nd Annual International Cryptology Conference (CRYPTO\u201922), 78."},{"key":"e_1_3_2_44_2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1109\/CSF.2019.00019","volume-title":"Proceedings of 2019 IEEE 32nd Computer Security Foundations Symposium (CSF)","author":"Canetti Ran","year":"2019","unstructured":"Ran Canetti, Alley Stoughton, and Mayank Varia. 2019. EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. In Proceedings of 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 167\u2013716. DOI: http:\/\/dx.doi.org\/10.1109\/CSF.2019.00019"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1109\/SP.2018.00033","volume-title":"Proceedings of 2018 IEEE Symposium on Security and Privacy (SP)","author":"Cheval Vincent","year":"2018","unstructured":"Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice. In Proceedings of 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 529\u2013546. DOI: http:\/\/dx.doi.org\/10.1109\/SP.2018.00033"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_47_2","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1007\/978-3-540-30576-7_26","volume-title":"Proceedings of the 2nd International Conference on Theory of Cryptography (TCC\u201905)","author":"Datta Anupam","year":"2005","unstructured":"Anupam Datta, Ralf K\u00fcsters, John C. Mitchell, and Ajith Ramanathan. 2005. On the Relationships between Notions of Simulation-Based Security. In Proceedings of the 2nd International Conference on Theory of Cryptography (TCC\u201905). Springer-Verlag, 476\u2013494. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-540-30576-7_26"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.005"},{"key":"e_1_3_2_49_2","unstructured":"St\u00e9phanie Delaune Steve Kremer and Olivier Pereira. 2009. Simulation Based Security in the Applied Pi Calculus. Cryptology ePrint Archive (2009). Retrieved from https:\/\/eprint.iacr.org\/2009\/267"},{"issue":"4","key":"e_1_3_2_50_2","article-title":"Modular, Fully-Abstract Compilation by Approximate Back-translation","volume":"13","author":"Devriese Dominique","year":"2017","unstructured":"Dominique Devriese, Marco Patrignani, Frank Piessens, and Steven Keuchel. 2017. Modular, Fully-Abstract Compilation by Approximate Back-translation. Logical Methods in Computer Science 13, 4 (Oct. 2017). Retrieved from https:\/\/lmcs.episciences.org\/4011","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/CSF54842.2022.9919680","volume-title":"IEEE 35th Computer Security Foundations Symposium (CSF)","author":"El-Korashy Akram","year":"2022","unstructured":"Akram El-Korashy, Roberto Blanco, J\u00e9r\u00e9my Thibault, Adrien Durier, Deepak Garg, and Catalin Hritcu. 2022. SecurePtrs: Proving secure compilation with data-flow back-translation and turn-taking simulation. IEEE 35th Computer Security Foundations Symposium (CSF), 64\u201379. DOI: http:\/\/dx.doi.org\/10.1109\/CSF54842.2022.9919680"},{"key":"e_1_3_2_52_2","first-page":"1","volume-title":"34th IEEE Computer Security Foundations Symposium (CSF \u201921)","author":"El-Korashy Akram","year":"2021","unstructured":"Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, and Frank Piessens. 2021. CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle. In 34th IEEE Computer Security Foundations Symposium (CSF \u201921), 1\u201316. DOI: http:\/\/dx.doi.org\/10.1109\/CSF51468.2021.00036"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(90)90010-U"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1109\/CSF.2018.00016","volume-title":"Proceedings of 2018 IEEE 31st Computer Security Foundations Symposium (CSF)","author":"Haagh H.","year":"2018","unstructured":"H. Haagh, A. Karbyshev, S. Oechsner, B. Spitters, and P. Strub. 2018. Computer-Aided Proofs for Multiparty Computation with Active Security. In Proceedings of 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE Computer Society 119\u2013131. DOI: http:\/\/dx.doi.org\/10.1109\/CSF.2018.00016"},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","first-page":"1220","DOI":"10.1109\/SP.2019.00028","volume-title":"Proceedings of 2019 IEEE Symposium on Security and Privacy (SP)","author":"Hastings Marcella","year":"2019","unstructured":"Marcella Hastings, Brett Hemenway, Daniel Noble, and Steve Zdancewic. 2019. SoK: General Purpose Compilers for Secure Multi-Party Computation. In Proceedings of 2019 IEEE Symposium on Security and Privacy (SP), 1220\u20131237. DOI: http:\/\/dx.doi.org\/10.1109\/SP.2019.00028"},{"key":"e_1_3_2_58_2","unstructured":"Michael Hicks. 2014. Formal Reasoning in PL and Crypto. Retrieved from http:\/\/www.pl-enthusiast.net\/2014\/12\/23\/formal-reasoning-pl-crypto\/"},{"key":"e_1_3_2_59_2","article-title":"Adaptive Security of Multi-Party Protocols, Revisited","author":"Hirt Martin","year":"2021","unstructured":"Martin Hirt, Chen-Da Liu-Zhang, and Ueli Maurer. 2021. Adaptive Security of Multi-Party Protocols, Revisited. In Proceedings of 19th International Conference on Theory of Cryptography.","journal-title":"Proceedings of 19th International Conference on Theory of Cryptography"},{"key":"e_1_3_2_60_2","unstructured":"Dennis Hofheinz and Victor Shoup. 2011. GNUC: A New Universal Composability Framework. Cryptology ePrint Archive. Retrieved from http:\/\/eprint.iacr.org\/"},{"key":"e_1_3_2_61_2","volume-title":"Proceedings of IEEE Symposium on Security and Privacy","author":"Hofheinz Dennis","year":"2006","unstructured":"Dennis Hofheinz and Dominique Unruh. 2006. Simulatable Security and Polynomially Bounded Concurrent Composability. In Proceedings of IEEE Symposium on Security and Privacy."},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-012-9127-4"},{"key":"e_1_3_2_63_2","first-page":"133","article-title":"A Kripke Logical Relation between ML and Assembly","author":"Hur Chung-Kil","year":"2011","unstructured":"Chung-Kil Hur and Derek Dreyer. 2011. A Kripke Logical Relation between ML and Assembly. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 133\u2013146.","journal-title":"Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"},{"key":"e_1_3_2_64_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-540-31987-0_29","volume-title":"Proceedings of the 14th European Conference on Programming Languages and Systems (ESOP \u201905)","volume":"3444","author":"Jeffrey Alan","year":"2005","unstructured":"Alan Jeffrey and Julian Rathke. 2005. Java Jr.: Fully Abstract Trace Semantics for a Core Java Language. In Proceedings of the 14th European Conference on Programming Languages and Systems (ESOP \u201905), Lecture Notes in Computer Science, Vol. 3444. Springer, 423\u2013438."},{"key":"e_1_3_2_65_2","unstructured":"Matthis Kruse and Marco Patrignani. 2022. Composing Secure Compilers."},{"key":"e_1_3_2_66_2","author":"Kuesters Ralf","year":"2013","unstructured":"Ralf Kuesters, Max Tuengerthal, and Daniel Rausch. 2013. The IITM Model: A Simple and Expressive Model for Universal Composability. Technical Report 025.","journal-title":"The IITM Model: A Simple and Expressive Model for Universal Composability"},{"key":"e_1_3_2_67_2","volume-title":"IEEE 37th Computer Security Foundations Symposium (CSF)","author":"K\u00fcnnemann Robert","year":"2024","unstructured":"Robert K\u00fcnnemann, Marco Patrignani, and Ethan Cecchetti. Computationally Bounded Robust Compilation and Universally Composable SecurityProceedings of 2024 In IEEE 37th Computer Security Foundations Symposium (CSF)."},{"key":"e_1_3_2_68_2","first-page":"309","volume-title":"Proceedings of 19th IEEE Computer Security Foundations Workshop","author":"Ralf K\u00fcsters","year":"2006","unstructured":"Ralf K\u00fcsters. 2006. Simulation-Based Security with Inexhaustible Interactive Turing Machines. In Proceedings of 19th IEEE Computer Security Foundations Workshop. IEEE Computer Society, 309\u2013320."},{"key":"e_1_3_2_69_2","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1109\/CSF.2015.28","volume-title":"Proceedings of 2015 IEEE 28th Computer Security Foundations Symposium","author":"Kusters Ralf","year":"2015","unstructured":"Ralf Kusters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr. 2015. A Hybrid Approach for Proving Noninterference of Java Programs. In Proceedings of 2015 IEEE 28th Computer Security Foundations Symposium. IEEE, 305\u2013319. DOI: http:\/\/dx.doi.org\/10.1109\/CSF.2015.28"},{"key":"e_1_3_2_70_2","first-page":"203","article-title":"Formal Foundation for Specification and Verification","author":"Lamport Leslie","year":"1984","unstructured":"Leslie Lamport and Fred B. Schneider. 1984. Formal Foundation for Specification and Verification. In Distributed Systems: Methods and Tools for Specification, An Advanced Course, 203\u2013285. DOI: http:\/\/dx.doi.org\/10.5555\/647435.726394","journal-title":"Distributed Systems: Methods and Tools for Specification, An Advanced Course"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314607"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498930"},{"key":"e_1_3_2_74_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-642-27375-9_3","volume-title":"Proceedings of Joint Workshop on Theory of Security and Applications (TOSCA \u201911)","volume":"6993","author":"Maurer Ueli","year":"2011","unstructured":"Ueli Maurer. 2011. Constructive Cryptography-A New Paradigm for Security Definitions and Proofs. In Proceedings of Joint Workshop on Theory of Security and Applications (TOSCA \u201911), Revised Selected Papers. Sebastian M\u00f6dersheim and Catuscia Palamidessi (Eds.), Lecture Notes in Computer Science, Vol. 6993, Springer, 33\u201356. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-642-27375-9_3"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.30"},{"key":"e_1_3_2_76_2","unstructured":"Greg Morrisett Elaine Shi Kristina Sojakova Xiong Fan and Joshua Gancher. 2021. IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols. Cryptology ePrint Archive Paper 2021\/147. Retrieved from https:\/\/eprint.iacr.org\/2021\/147"},{"key":"e_1_3_2_77_2","unstructured":"Marco Patrignani. 2021. Why Should Anyone Use Colours? or Syntax Highlighting Beyond Code Snippets. arXiv:2001.11334. Retrieved from https:\/\/arxiv.org\/abs\/2001.11334"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.03.002"},{"key":"e_1_3_2_81_2","volume-title":"Proceedings of 2016 IEEE 29th Computer Security Foundations Symposium (CSF)","author":"Patrignani Marco","year":"2016","unstructured":"Marco Patrignani, Dominique Devriese, and Frank Piessens. 2016. On Modular and Fully Abstract Compilation. In Proceedings of 2016 IEEE 29th Computer Security Foundations Symposium (CSF)."},{"key":"e_1_3_2_82_2","volume-title":"Proceedings of 28th European Symposium on Programming Languages and Systems (ESOP \u201919)","author":"Patrignani Marco","year":"2019","unstructured":"Marco Patrignani and Deepak Garg. 2019. Robustly Safe Compilation. In Proceedings of 28th European Symposium on Programming Languages and Systems (ESOP \u201919)."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/3436809"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_85_2","unstructured":"Marco Patrignani Riad S. Wahby and Robert K\u00fcnnemann. 2022. Universal Composability Is Secure Compilation. (2022). arXiv:1910.08634. Retrieved from https:\/\/arxiv.org\/abs\/1910.08634"},{"key":"e_1_3_2_86_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-642-54833-8_8","volume-title":"Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP)","volume":"8410","author":"Perconti James T.","year":"2014","unstructured":"James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP). Shao, Zhong (Ed.), Lecture Notes in Computer Science, Vol. 8410, Springer Berlin, 128\u2013148."},{"key":"e_1_3_2_87_2","unstructured":"Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. Retrieved from http:\/\/www.kb.ecei.tohoku.ac.jp\/\u223csumii\/pub\/infohide.pdf"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_89_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-031-07085-3_9","volume-title":"Proceedings of 41st Annual International Conference on the Theory and Applications of Cryptographic Techniques, Advances in Cryptology (EUROCRYPT \u201922)","author":"Rausch Daniel","year":"2022","unstructured":"Daniel Rausch, Ralf K\u00fcsters, and C\u00e9line Chevalier. 2022. Embedding the UC Model into the IITM Model. In Proceedings of 41st Annual International Conference on the Theory and Applications of Cryptographic Techniques, Advances in Cryptology (EUROCRYPT \u201922). Orr Dunkelman and Stefan Dziembowski (Eds.), Lecture Notes in Computer Science, Springer International Publishing, Cham, 242\u2013272. DOI: http:\/\/dx.doi.org\/10.1007\/978-3-031-07085-3_9"},{"key":"e_1_3_2_90_2","volume-title":"PI-Calculus: A Theory of Mobile Processes","author":"Sangiorgi Davide","year":"2001","unstructured":"Davide Sangiorgi and David Walker. 2001. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, New York, NY."},{"key":"e_1_3_2_91_2","doi-asserted-by":"crossref","unstructured":"Fred B. Schneider. 2000. Enforceable Security Policies. ACM Transactions of Information Systems Security 3 1 (2000) 30\u201350. Retrieved from http:\/\/www.cs.cornell.edu\/fbs\/publications\/EnfSecPols.pdf","DOI":"10.1145\/353323.353382"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.5555\/959088.959091"},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_3_2_94_2","first-page":"256","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201916)","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, C\u0103t\u0103lin Hri\u0163cu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201916). ACM, New York, NY, 256\u2013270. DOI: http:\/\/dx.doi.org\/10.1145\/2837614.2837655"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3698234","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3698234","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3698234","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:18Z","timestamp":1750295838000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3698234"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,31]]},"references-count":93,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12,31]]}},"alternative-id":["10.1145\/3698234"],"URL":"https:\/\/doi.org\/10.1145\/3698234","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2024,12,31]]},"assertion":[{"value":"2022-12-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-25","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}