{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:17:03Z","timestamp":1748405823780,"version":"3.41.0"},"publisher-location":"Singapore","reference-count":52,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819789429"},{"type":"electronic","value":"9789819789436"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"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-981-97-8943-6_12","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"241-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On Computational Indistinguishability and\u00a0Logical Relations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo Dal","family":"Lago","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6402-3531","authenticated-orcid":false,"given":"Zeinab","family":"Galal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6533-8307","authenticated-orcid":false,"given":"Giulia","family":"Giusti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M.: Security protocols: principles and calculi. In: Aldini, A., Gorrieri, R. (eds.) Foundations of Security Analysis and Design IV, pp. 1\u201323 (2006). https:\/\/doi.org\/10.1007\/978-3-540-74810-6_1","DOI":"10.1007\/978-3-540-74810-6_1"},{"key":"12_CR2","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65-116. Addison-Wesley Longman Publishing Co., Inc. (1990)"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Dal\u00a0Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci. 12(1) (2016). https:\/\/doi.org\/10.2168\/LMCS-12(1:4)2016","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S.Y., Sato, T.: Higher-order probabilistic adversarial computations: categorical semantics and program logics. In: Proceedings of the ICFP 2021, pp. 1\u201330. ACM (2021). https:\/\/doi.org\/10.1145\/3473598","DOI":"10.1145\/3473598"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Birkedal, L.: Step-indexed logical relations for countable nondeterminism and probabilistic choice. In: Proceedings of POPL 2023, vol. 7, pp. 33\u201360. ACM (2023). https:\/\/doi.org\/10.1145\/3571195","DOI":"10.1145\/3571195"},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/3665453.3665461","volume":"11","author":"D Baelde","year":"2024","unstructured":"Baelde, D., Jacomme, C.: The squirrel prover and its logic. ACM SIGLOG News 11(2), 62\u201383 (2024). https:\/\/doi.org\/10.1145\/3665453.3665461","journal-title":"ACM SIGLOG News"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Balan, A., Kurz, A., Velebil, J.: Extending set functors to generalised metric spaces. Log. Methods Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:5)2019","DOI":"10.23638\/LMCS-15(1:5)2019"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Baldan, P., Bonchi, F., Kerstan, H., K\u00f6nig, B.: Coalgebraic behavioral metrics. Log. Methods Comput. Sci. 14(3) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(3:20)2018","DOI":"10.23638\/LMCS-14(3:20)2018"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: Proceedings of the CCS 2014, pp. 609\u2013620 (2014). https:\/\/doi.org\/10.1145\/2660267.2660276","DOI":"10.1145\/2660267.2660276"},{"issue":"4","key":"12_CR10","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s00145-002-0116-x","volume":"15","author":"M Bellare","year":"2002","unstructured":"Bellare, M.: A note on negligible functions. J. Cryptol. 15(4), 271\u2013284 (2002). https:\/\/doi.org\/10.1007\/s00145-002-0116-x","journal-title":"J. Cryptol."},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Proceedings of FoSSaCS 2015, pp. 279\u2013294. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"12_CR12","unstructured":"van Breugel, F.: The metric monad for probabilistic nondeterminism. Draft available at http:\/\/www.cse.yorku.ca\/franck\/research\/drafts\/monad.pdf (2005)"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Canetti, R., Stoughton, A., Varia, M.: EasyUC: using EasyCrypt to mechanize proofs of universally composable security. In: Proceedings of the CSF 2019, pp. 167\u2013183. IEEE (2019). https:\/\/doi.org\/10.1109\/CSF.2019.00019","DOI":"10.1109\/CSF.2019.00019"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Dal\u00a0Lago, U., Galal, Z., Giusti, G.: On Computational Indistinguishability and Logical Relations (2024). http:\/\/arxiv.org\/abs\/2408.17340","DOI":"10.1007\/978-981-97-8943-6_12"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Gavazzo, F.: A relational theory of effects and coeffects. In: Proceedings of the POPL 2022, vol.\u00a06, pp. 1\u201328. ACM (2022). https:\/\/doi.org\/10.1145\/3498692","DOI":"10.1145\/3498692"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Giusti, G.: On session typing, probabilistic polynomial time, and cryptographic experiments. In: Proceedings of the CONCUR 2022, vol.\u00a0243, pp. 37:1\u201337:18 (2022). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2022.37","DOI":"10.4230\/LIPICS.CONCUR.2022.37"},{"key":"12_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02930-1_14","author":"U Dal Lago","year":"2012","unstructured":"Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda calculus. Log. Methods Comput. Sci. (2012). https:\/\/doi.org\/10.1007\/978-3-642-02930-1_14","journal-title":"Log. Methods Comput. Sci."},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Petit, B.: Linear dependent types in a call-by-value scenario. In: Proceedings of the PPDP 2012, pp. 115\u2013126. ACM (2012). https:\/\/doi.org\/10.1145\/2370776.2370792","DOI":"10.1145\/2370776.2370792"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Zuppiroli, S., Gabbrielli, M.: Probabilistic recursion theory and implicit computational complexity. Sci. Ann. Comput. Sci. 177\u2013216 (2014). https:\/\/doi.org\/10.7561\/SACS.2014.2.177","DOI":"10.7561\/SACS.2014.2.177"},{"issue":"2","key":"12_CR20","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). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Ehrhard, T., Tasson, C.: Probabilistic call by push value. Log. Methods Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:3)2019","DOI":"10.23638\/LMCS-15(1:3)2019"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: Proceedings of the CSFW 2001, pp. 160\u2013173. IEEE (2001). https:\/\/doi.org\/10.1109\/CSFW.2001.930144","DOI":"10.1109\/CSFW.2001.930144"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful programs: applicative distances. In: Proceedings of the LICS 2018, pp. 452\u2013461. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209149","DOI":"10.1145\/3209108.3209149"},{"issue":"3","key":"12_CR24","doi-asserted-by":"publisher","first-page":"419","DOI":"10.2307\/1403865","volume":"70","author":"AL Gibbs","year":"2002","unstructured":"Gibbs, A.L., Su, F.E.: On choosing and bounding probability metrics. Int. Stat. Rev. 70(3), 419\u2013435 (2002). https:\/\/doi.org\/10.2307\/1403865","journal-title":"Int. Stat. Rev."},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: Proceedings of the 1986 ACM Conference on LISP and Functional Programming, pp. 28\u201338. ACM (1986). https:\/\/doi.org\/10.1145\/319838.319848","DOI":"10.1145\/319838.319848"},{"issue":"1","key":"12_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"JY Girard","year":"1992","unstructured":"Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theoret. Comput. Sci. 97(1), 1\u201366 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90386-T","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR27","unstructured":"Goldreich, O.: Foundations of Cryptography. Vol. 1: Basic Tools. Cambridge University Press, Cambridge (2007)"},{"issue":"2","key":"12_CR28","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270\u2013299 (1984). https:\/\/doi.org\/10.1016\/0022-0000(84)90070-9","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR29","unstructured":"Gordon, A.D.: Operational equivalences for untyped and polymorphic object calculi. In: Higher-Order Operational Techniques in Semantics, Publications of the Newton Institute, pp. 9\u201354. Cambridge University Press (1998)"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Goubault-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. Math. Struct. Comput. Sci. 1169\u20131217 (2008). https:\/\/doi.org\/10.1007\/3-540-45793-3_37","DOI":"10.1007\/3-540-45793-3_37"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Goubault-Larrecq, J., Lasota, S., Nowak, D., Zhang, Y.: Complete lax logical relations for cryptographic lambda-calculi. In: Proceedings of the CSL 2004, pp. 400\u2013414. Springer (2004).https:\/\/doi.org\/10.1007\/978-3-540-30124-0_31","DOI":"10.1007\/978-3-540-30124-0_31"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Hofmann, D., Seal, G.J., Tholen, W.: Monoidal Topology: A Categorical Approach to Order, Metric, and Topology. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107517288"},{"issue":"1","key":"12_CR33","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.03.013","volume":"357","author":"M Hyland","year":"2006","unstructured":"Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theoret. Comput. Sci. 357(1), 70\u201399 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.03.013","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"12_CR34","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1016\/j.jcss.2005.06.008","volume":"72","author":"R Impagliazzo","year":"2006","unstructured":"Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. J. Comput. Syst. Sci. 72(2), 286\u2013320 (2006). https:\/\/doi.org\/10.1016\/j.jcss.2005.06.008","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"12_CR35","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1007\/s10958-006-0049-2","volume":"133","author":"LV Kantorovich","year":"2006","unstructured":"Kantorovich, L.V.: On the translocation of masses. J. Math. Sci. 133(4), 1381\u20131382 (2006). https:\/\/doi.org\/10.1007\/s10958-006-0049-2","journal-title":"J. Math. Sci."},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Katz, J., Lindell, Y.: Introduction to Modern Cryptography. CRC Press (2020)","DOI":"10.1201\/9781351133036"},{"key":"12_CR37","unstructured":"Lassen, S.B.: Relational reasoning about contexts. In: Higher-Order Operational Techniques in Semantics, Publications of the Newton Institute, vol.\u00a091, pp. 91\u2013136. Cambridge University Press (1998)"},{"issue":"2","key":"12_CR38","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009). https:\/\/doi.org\/10.1016\/j.ic.2007.12.004","journal-title":"Inf. Comput."},{"key":"12_CR39","unstructured":"Levy, P.B.: Call-by-Push-Value: A Functional\/Imperative Synthesis, vol.\u00a02. Springer Science & Business Media (2012)"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Mardare, R., Panangaden, P., Plotkin, G.: Quantitative algebraic reasoning. In: Proceedings of the LICS 2016, pp. 700\u2013709. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934518","DOI":"10.1145\/2933575.2934518"},{"key":"12_CR41","doi-asserted-by":"publisher","unstructured":"Mitchell, J., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proceedings of the SFCS 1998, pp. 725\u2013733. IEEE (1998). https:\/\/doi.org\/10.1109\/SFCS.1998.743523","DOI":"10.1109\/SFCS.1998.743523"},{"key":"12_CR42","doi-asserted-by":"publisher","unstructured":"Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoret. Comput. Sci. 353(1\u20133) (2006). https:\/\/doi.org\/10.1016\/j.tcs.2005.10.044","DOI":"10.1016\/j.tcs.2005.10.044"},{"key":"12_CR43","doi-asserted-by":"publisher","unstructured":"Mitchell, J.C.: Multiset rewriting and security protocol analysis. In: Proceedings of the RTA 2002, pp. 19\u201322. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45610-4_2","DOI":"10.1007\/3-540-45610-4_2"},{"key":"12_CR44","doi-asserted-by":"publisher","unstructured":"Mitchell, J.C., Scedrov, A.: Notes on sconing and relators. In: Proceedings of the CSL 1992, pp. 352\u2013378. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-56992-8_21","DOI":"10.1007\/3-540-56992-8_21"},{"key":"12_CR45","doi-asserted-by":"publisher","unstructured":"Nowak, D., Zhang, Y.: A calculus for game-based security proofs. In: Proceedings of the ProvSec 2010. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-16280-0_3","DOI":"10.1007\/978-3-642-16280-0_3"},{"key":"12_CR46","doi-asserted-by":"publisher","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Proceedings of the ICFP 2010, pp. 157\u2013168. ACM (2010). https:\/\/doi.org\/10.1145\/1863543.1863568","DOI":"10.1145\/1863543.1863568"},{"key":"12_CR47","unstructured":"Rosenthal, K.I.: Quantales and Their Applications. Wiley (1990)"},{"key":"12_CR48","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Rutten, J.: Advanced Topics in Bisimulation and Coinduction. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511792588"},{"key":"12_CR49","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch., p. 332 (2004). http:\/\/eprint.iacr.org\/2004\/332"},{"key":"12_CR50","doi-asserted-by":"publisher","unstructured":"Statman, R.: Logical relations and the typed $$\\lambda $$-calculus. Inf. Control 65(2\u20133), 85\u201397 (1985). https:\/\/doi.org\/10.1016\/S0019-9958(85)80001-2","DOI":"10.1016\/S0019-9958(85)80001-2"},{"issue":"2","key":"12_CR51","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"WW Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symbol. Log. 32(2), 198\u2013212 (1967). https:\/\/doi.org\/10.2307\/2271658","journal-title":"J. Symbol. Log."},{"key":"12_CR52","doi-asserted-by":"publisher","unstructured":"Wild, P., Schr\u00f6der, L.: Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci. (2022). https:\/\/doi.org\/10.46298\/lmcs-18(2:19)2022","DOI":"10.46298\/lmcs-18(2:19)2022"}],"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-981-97-8943-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:40Z","timestamp":1748364760000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}