{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:25:18Z","timestamp":1750220718551,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:00:00Z","timestamp":1604016000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["ANR-17-CE39-0004-01"],"award-info":[{"award-number":["ANR-17-CE39-0004-01"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,30]]},"DOI":"10.1145\/3372297.3417229","type":"proceedings-article","created":{"date-parts":[[2021,3,4]],"date-time":"2021-03-04T16:21:21Z","timestamp":1614874881000},"page":"1427-1444","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets"],"prefix":"10.1145","author":[{"given":"Hubert","family":"Comon","sequence":"first","affiliation":[{"name":"LSV, CNRS & ENS Paris-Saclay & Inria & Universit\u00e9 Paris-Saclay, Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charlie","family":"Jacomme","sequence":"additional","affiliation":[{"name":"LSV, CNRS & ENS Paris-Saclay & Inria & Universit\u00e9 Paris-Saclay, Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Scerri","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Versailles Saint-Quentin & Inria, Versailles, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,2]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"[n. d.]. ISO\/IEC 9798-3:2019 IT Security techniques - Entity authentication ?Part 3: Mechanisms using digital signature techniques. https:\/\/www.iso.org\/standard\/67115.html  [n. d.]. ISO\/IEC 9798-3:2019 IT Security techniques - Entity authentication ?Part 3: Mechanisms using digital signature techniques. https:\/\/www.iso.org\/standard\/67115.html"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.16"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0046-6"},{"key":"e_1_3_2_2_4_1","first-page":"12","article-title":"The Reactive Simulatability (RSIM) Framework for Asynchronous","volume":"205","author":"Backes Michael","year":"2007","unstructured":"Michael Backes , Birgit Pfitzmann , and Michael Waidner . 2007 . The Reactive Simulatability (RSIM) Framework for Asynchronous Systems. Inf. Comput. , Vol. 205 , 12 (Dec. 2007), 1685--1720. https:\/\/doi.org\/10.1016\/j.ic.2007.05.002 10.1016\/j.ic.2007.05.002 Michael Backes, Birgit Pfitzmann, and Michael Waidner. 2007. The Reactive Simulatability (RSIM) Framework for Asynchronous Systems. Inf. Comput., Vol. 205, 12 (Dec. 2007), 1685--1720. https:\/\/doi.org\/10.1016\/j.ic.2007.05.002","journal-title":"Systems. Inf. Comput."},{"key":"e_1_3_2_2_5_1","volume-title":"ESORICS 2018, Barcelona, Spain, September 3--7, 2018, Proceedings, Part II. 350--372","author":"Bana Gergei","year":"2018","unstructured":"Gergei Bana , Rohit Chadha , and Ajay Kumar Eeralla . 2018 . Formal Analysis of Vote Privacy Using Computationally Complete Symbolic Attacker. In Computer Security - 23rd European Symposium on Research in Computer Security , ESORICS 2018, Barcelona, Spain, September 3--7, 2018, Proceedings, Part II. 350--372 . https:\/\/doi.org\/10.1007\/978--3--319--98989--1_18 10.1007\/978--3--319--98989--1_18 Gergei Bana, Rohit Chadha, and Ajay Kumar Eeralla. 2018. Formal Analysis of Vote Privacy Using Computationally Complete Symbolic Attacker. In Computer Security - 23rd European Symposium on Research in Computer Security, ESORICS 2018, Barcelona, Spain, September 3--7, 2018, Proceedings, Part II. 350--372. https:\/\/doi.org\/10.1007\/978--3--319--98989--1_18"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660276"},{"volume-title":"Advances in Cryptology -- CRYPTO 2011 (Lecture Notes in Computer Science)","author":"Barthe Gilles","key":"e_1_3_2_2_7_1","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , Sylvain Heraud , and Santiago Zanella-B\u00e9guelin . 2011. Computer-Aided Security Proofs for the Working Cryptographer . In Advances in Cryptology -- CRYPTO 2011 (Lecture Notes in Computer Science) , Vol. 6841 . Springer , Heidelberg , 71--90. Gilles Barthe, Benjamin Gr\u00e9goire, Sylvain Heraud, and Santiago Zanella-B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology -- CRYPTO 2011 (Lecture Notes in Computer Science), Vol. 6841. Springer, Heidelberg, 71--90."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Bruno Blanchet. 2007. CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. In Dagstuhl seminar \"Formal Protocol Verification Applied\" .  Bruno Blanchet. 2007. CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. In Dagstuhl seminar \"Formal Protocol Verification Applied\" .","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00009"},{"key":"e_1_3_2_2_10_1","volume-title":"Konrad Kohbrok, and Markulf Kohlweiss.","author":"Brzuska Chris","year":"2018","unstructured":"Chris Brzuska , Antoine Delignat-Lavaud , C\u00e9 dric Fournet , Konrad Kohbrok, and Markulf Kohlweiss. 2018 . State Separation for Code-Based Game-Playing Proofs. In ASIACRYPT (3) (Lecture Notes in Computer Science), Vol. 11274 . Springer , 222--249. Chris Brzuska, Antoine Delignat-Lavaud, C\u00e9 dric Fournet, Konrad Kohbrok, and Markulf Kohlweiss. 2018. State Separation for Code-Based Game-Playing Proofs. In ASIACRYPT (3) (Lecture Notes in Computer Science), Vol. 11274. Springer, 222--249."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-013-0192-y"},{"key":"e_1_3_2_2_12_1","volume-title":"Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS '11)","author":"Brzuska Christina","year":"2046","unstructured":"Christina Brzuska , Marc Fischlin , Bogdan Warinschi , and Stephen C. Williams . 2011. Composability of Bellare-rogaway Key Exchange Protocols . In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS '11) . ACM, New York, NY, USA, 51--62. https:\/\/doi.org\/10.1145\/ 2046 707.2046716 10.1145\/2046707.2046716 Christina Brzuska, Marc Fischlin, Bogdan Warinschi, and Stephen C. Williams. 2011. Composability of Bellare-rogaway Key Exchange Protocols. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS '11). ACM, New York, NY, USA, 51--62. https:\/\/doi.org\/10.1145\/2046707.2046716"},{"key":"e_1_3_2_2_13_1","first-page":"1","article-title":"From Computationally-Proved Protocol Specifications to Implementations and Application to SSH","volume":"4","author":"Cad\u00e9 David","year":"2013","unstructured":"David Cad\u00e9 and Bruno Blanchet . 2013 . From Computationally-Proved Protocol Specifications to Implementations and Application to SSH . Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA) , Vol. 4 , 1 (March 2013), 4--31. David Cad\u00e9 and Bruno Blanchet. 2013. From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), Vol. 4, 1 (March 2013), 4--31.","journal-title":"Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Ran Canetti. 2000. Universally Composable Security: A New Paradigm for Cryptographic Protocols. http:\/\/eprint.iacr.org\/2000\/067  Ran Canetti. 2000. Universally Composable Security: A New Paradigm for Cryptographic Protocols. http:\/\/eprint.iacr.org\/2000\/067","DOI":"10.1109\/SFCS.2001.959888"},{"volume-title":"Advances in Cryptology - CRYPTO 2003 (Lecture Notes in Computer Science )","author":"Canetti Ran","key":"e_1_3_2_2_16_1","unstructured":"Ran Canetti and Tal Rabin . 2003. Universal Composition with Joint State . In Advances in Cryptology - CRYPTO 2003 (Lecture Notes in Computer Science ) , Dan Boneh (Ed.). Springer Berlin Heidelberg , 265--281. Ran Canetti and Tal Rabin. 2003. Universal Composition with Joint State. In Advances in Cryptology - CRYPTO 2003 (Lecture Notes in Computer Science ), Dan Boneh (Ed.). Springer Berlin Heidelberg, 265--281."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Hubert Comon Charlie Jacomme and Guillaume Scerri. 2020. Oracle Simulation: a Technique for Protocol Composition with Long Term Shared Secrets - long version. https:\/\/hal.inria.fr\/hal-02913866  Hubert Comon Charlie Jacomme and Guillaume Scerri. 2020. Oracle Simulation: a Technique for Protocol Composition with Long Term Shared Secrets - long version. https:\/\/hal.inria.fr\/hal-02913866","DOI":"10.1145\/3372297.3417229"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.9"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.9"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368324"},{"volume-title":"Automata, Languages and Programming (Lecture Notes in Computer Science ), Lu\u00eds Caires, Giuseppe F","author":"Datta Anupam","key":"e_1_3_2_2_21_1","unstructured":"Anupam Datta , Ante Derek , John C. Mitchell , Vitaly Shmatikov , and Mathieu Turuani . 2005. Probabilistic Polynomial-Time Semantics for a Protocol Security Logic . In Automata, Languages and Programming (Lecture Notes in Computer Science ), Lu\u00eds Caires, Giuseppe F . Italiano, Lu\u00eds Monteiro, Catuscia Palamidessi, and Moti Yung (Eds.). Springer Berlin Heidelberg , 16--29. Anupam Datta, Ante Derek, John C. Mitchell, Vitaly Shmatikov, and Mathieu Turuani. 2005. Probabilistic Polynomial-Time Semantics for a Protocol Security Logic. In Automata, Languages and Programming (Lecture Notes in Computer Science ), Lu\u00eds Caires, Giuseppe F. Italiano, Lu\u00eds Monteiro, Catuscia Palamidessi, and Moti Yung (Eds.). Springer Berlin Heidelberg, 16--29."},{"key":"e_1_3_2_2_22_1","first-page":"4","article-title":"A Compositional Logic for Proving Security Properties of Protocols","volume":"11","author":"Durgin Nancy","year":"2003","unstructured":"Nancy Durgin , John Mitchell , and Dusko Pavlovic . 2003 . A Compositional Logic for Proving Security Properties of Protocols . J. Comput. Secur. , Vol. 11 , 4 (July 2003), 677--721. http:\/\/dl.acm.org\/citation.cfm?id=959088.959095 Nancy Durgin, John Mitchell, and Dusko Pavlovic. 2003. A Compositional Logic for Proving Security Properties of Protocols. J. Comput. Secur., Vol. 11, 4 (July 2003), 677--721. http:\/\/dl.acm.org\/citation.cfm?id=959088.959095","journal-title":"J. Comput. Secur."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660308"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/0217017"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-013-9160-y"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.63"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046715"},{"volume-title":"TOSCA (Lecture Notes in Computer Science)","author":"Maurer Ueli","key":"e_1_3_2_2_28_1","unstructured":"Ueli Maurer . 2011. Constructive Cryptography - A New Paradigm for Security Definitions and Proofs . In TOSCA (Lecture Notes in Computer Science) , Vol. 6993 . Springer , 33--56. Ueli Maurer. 2011. Constructive Cryptography - A New Paradigm for Security Definitions and Proofs. In TOSCA (Lecture Notes in Computer Science), Vol. 6993. Springer, 33--56."},{"volume-title":"Revisited. In Advances in Cryptology -- ASIACRYPT 2011 (Lecture Notes in Computer Science)","author":"Paterson Kenneth G.","key":"e_1_3_2_2_29_1","unstructured":"Kenneth G. Paterson , Jacob C. N. Schuldt , Martijn Stam , and Susan Thomson . 2011. On the Joint Security of Encryption and Signature , Revisited. In Advances in Cryptology -- ASIACRYPT 2011 (Lecture Notes in Computer Science) , Dong Hoon Lee and Xiaoyun Wang (Eds.). Springer Berlin Heidelberg , 161--178. Kenneth G. Paterson, Jacob C. N. Schuldt, Martijn Stam, and Susan Thomson. 2011. On the Joint Security of Encryption and Signature, Revisited. In Advances in Cryptology -- ASIACRYPT 2011 (Lecture Notes in Computer Science), Dong Hoon Lee and Xiaoyun Wang (Eds.). Springer Berlin Heidelberg, 161--178."},{"key":"e_1_3_2_2_30_1","volume-title":"Computational Security","author":"Scerri Guillaume","year":"2016","unstructured":"Guillaume Scerri and Stanley-Oakes Ryan . 2016. Analysis of Key Wrapping APIs: Generic Policies , Computational Security . IEEE Computer Society , 281--295. https:\/\/doi.org\/10.1109\/CSF. 2016 .27 10.1109\/CSF.2016.27 Guillaume Scerri and Stanley-Oakes Ryan. 2016. Analysis of Key Wrapping APIs: Generic Policies, Computational Security. IEEE Computer Society, 281--295. https:\/\/doi.org\/10.1109\/CSF.2016.27"},{"volume-title":"Cryptography and Coding (Lecture Notes in Computer Science )","author":"Williams Stephen C.","key":"e_1_3_2_2_31_1","unstructured":"Stephen C. Williams . 2011. Analysis of the SSH Key Exchange Protocol . In Cryptography and Coding (Lecture Notes in Computer Science ) , Liqun Chen (Ed.). Springer Berlin Heidelberg , 356--374. Stephen C. Williams. 2011. Analysis of the SSH Key Exchange Protocol. In Cryptography and Coding (Lecture Notes in Computer Science ), Liqun Chen (Ed.). Springer Berlin Heidelberg, 356--374."},{"key":"e_1_3_2_2_32_1","unstructured":"Tatu Ylonen and Chris Lonvick. [n. d.]. The Secure Shell (SSH) Transport Layer Protocol. https:\/\/tools.ietf.org\/html\/rfc4253  Tatu Ylonen and Chris Lonvick. [n. d.]. The Secure Shell (SSH) Transport Layer Protocol. https:\/\/tools.ietf.org\/html\/rfc4253"}],"event":{"name":"CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Virtual Event USA","acronym":"CCS '20"},"container-title":["Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3417229","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372297.3417229","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:33:25Z","timestamp":1750199605000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3417229"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,30]]},"references-count":31,"alternative-id":["10.1145\/3372297.3417229","10.1145\/3372297"],"URL":"https:\/\/doi.org\/10.1145\/3372297.3417229","relation":{},"subject":[],"published":{"date-parts":[[2020,10,30]]},"assertion":[{"value":"2020-11-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}