{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T16:03:37Z","timestamp":1780589017128,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"French Government (France 2030, ANR \u2013 PEPR Networks of the Future)","award":["ANR-22-PEFT-0009"],"award-info":[{"award-number":["ANR-22-PEFT-0009"]}]},{"name":"Agence Nationale de la Recherche (ANR) \u2013 PRIVA-SIQ","award":["ANR-23-CE39-0008"],"award-info":[{"award-number":["ANR-23-CE39-0008"]}]},{"name":"European Union's Horizon Europe Framework Programme","award":["101093046"],"award-info":[{"award-number":["101093046"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1145\/3779208.3805979","type":"proceedings-article","created":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T15:21:58Z","timestamp":1780586518000},"page":"1584-1597","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of EDHOC-PSK: A Symbolic Approach with SAPIC+"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-2498-4397","authenticated-orcid":false,"given":"Elsa","family":"L\u00f3pez P\u00e9rez","sequence":"first","affiliation":[{"name":"Inria Paris, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3695-9315","authenticated-orcid":false,"given":"Thomas","family":"Watteyne","sequence":"additional","affiliation":[{"name":"Unaffiliated, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4638-0639","authenticated-orcid":false,"given":"Cristina","family":"Onete","sequence":"additional","affiliation":[{"name":"University of Limoges, XLIM, CNRS UMR 7252, Limoges, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0555-0581","authenticated-orcid":false,"given":"Dhekra","family":"Mahmoud","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Clermont Auvergne, Clermont-Ferrand, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4459-511X","authenticated-orcid":false,"given":"Pascal","family":"Lafourcade","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Clermont Auvergne, Clermont-Ferrand, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5945-5208","authenticated-orcid":false,"given":"Vaishnavi","family":"Sundararajan","sequence":"additional","affiliation":[{"name":"IIT Delhi, Delhi, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7700-9121","authenticated-orcid":false,"given":"Mali\u0161a","family":"Vu\u010dini\u0107","sequence":"additional","affiliation":[{"name":"Inria Paris, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,4]]},"reference":[{"key":"e_1_3_2_1_1_1","article-title":"The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication","volume":"65","author":"Abadi Martin","year":"2017","unstructured":"Martin Abadi, Bruno Blanchet, and C\u00e9dric Fournet. 2017. The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. J. ACM 65, 1 (2017), 41 pages.","journal-title":"J. ACM"},{"key":"e_1_3_2_1_2_1","volume-title":"Analysing Unlinkability and Anonymity Using the Applied Pi Calculus. In IEEE Computer Security Foundations Symposium. 107\u2013121","author":"Arapinis Myrto","year":"2010","unstructured":"Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. 2010. Analysing Unlinkability and Anonymity Using the Applied Pi Calculus. In IEEE Computer Security Foundations Symposium. 107\u2013121."},{"key":"e_1_3_2_1_3_1","volume-title":"Pierre-Cyrille H\u00e9am, Olga Kouchnarenko, Jacopo Mantovani, Sebastian M\u00f6dersheim, David von Oheimb, Micha\u00ebl Rusinowitch, Judson Santos Santiago, Luca Vigano, Mathieu Turuani, and Laurent Vigneron.","author":"Armando Alessandro","year":"2005","unstructured":"Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille H\u00e9am, Olga Kouchnarenko, Jacopo Mantovani, Sebastian M\u00f6dersheim, David von Oheimb, Micha\u00ebl Rusinowitch, Judson Santos Santiago, Luca Vigano, Mathieu Turuani, and Laurent Vigneron. 2005. The AVISPA Tool for the automated validation of internet security protocols and applications. In Lecture Notes in Computer Science (Lecture Notes in Computer Science, Vol. 3576). Springer, Edinburgh, Scotland\/UK, France, 281\u2013285."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3559360"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Bruno Blanchet. 2016. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. In Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Number 1-2 in Foundations and Trends\u00ae in Privacy and Security. 1\u2013135. doi:10.1561\/3300000004","DOI":"10.1561\/3300000004"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.29"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00032"},{"key":"e_1_3_2_1_10_1","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Cheval Vincent","year":"2023","unstructured":"Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, and Steve Kremer. 2023. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses. In 32nd USENIX Security Symposium (USENIX Security 23). USENIX Association, Anaheim, CA, 5899\u20135916."},{"key":"e_1_3_2_1_11_1","volume-title":"31st USENIX Security Symposium (USENIX Security 22)","author":"Cheval Vincent","year":"2022","unstructured":"Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Kimnemann. 2022. SAPIC+: protocol verifiers of the world, unite!. In 31st USENIX Security Symposium (USENIX Security 22). USENIX Association, Boston, MA, 3935\u20133952."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.46298\/theoretics.24.4"},{"key":"e_1_3_2_1_13_1","unstructured":"Cisco Systems. 2020. 8.5 Identity PSK Feature Deployment Guide. https:\/\/www.dsco.com\/c\/en\/us\/td\/docs\/wireless\/controller\/technotes\/8-5\/b_Identity_PSK_Feature_Deployment_Guide.html Describes the configuration and deployment of Identity PSK (iPSK) for device-specific or group-specific pre-shared keys in enterprise and IoT environments."},{"key":"e_1_3_2_1_14_1","volume-title":"Relating two standard notions of secrecy. CoRR abs\/0706.0502","author":"Cortier V\u00e9ronique","year":"2007","unstructured":"V\u00e9ronique Cortier, Micha\u00ebl Rusinowitch, and Eugen Zalinescu. 2007. Relating two standard notions of secrecy. CoRR abs\/0706.0502 (2007)."},{"key":"e_1_3_2_1_15_1","volume-title":"Security Analysis of Improved EDHOC Protocol. In Foundations and Practice of Security: 15th International Symposium, FPS 2022","author":"Cottier Baptiste","year":"2022","unstructured":"Baptiste Cottier and David Pointcheval. 2022. Security Analysis of Improved EDHOC Protocol. In Foundations and Practice of Security: 15th International Symposium, FPS 2022, Ottawa, ON, Canada, December 12-14, 2022, Revised Selected Papers. Springer-Verlag, Berlin, Heidelberg, 3\u201318."},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17)","author":"Cremers Cas","unstructured":"Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A Comprehensive Symbolic Analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17). Association for Computing Machinery, New York, NY, USA, 1773\u20131788."},{"key":"e_1_3_2_1_17_1","volume-title":"Relations and Composition. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). 288\u2013303","author":"de Saint Guilhem Cyprien Delpech","year":"2020","unstructured":"Cyprien Delpech de Saint Guilhem, Marc Fischlin, and Bogdan Warinschi. 2020. Authentication in Key-Exchange: Definitions, Relations and Composition. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). 288\u2013303."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Jan-Erik Ekberg Alexandra Afanasyeva and N. Asokan. 2012. Authenticated Encryption Primitives for Size-Constrained Trusted Computing. In Trust and Trustworthy Computing Stefan Katzenbeisser Edgar Weippl L. Jean Camp Melanie Volkamer Mike Reiter and Xinwen Zhang (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 1\u201318.","DOI":"10.1007\/978-3-642-30921-2_1"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-58868-6_2"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/276698.276712"},{"key":"e_1_3_2_1_22_1","volume-title":"Careful with MAc-then-SIGn: A Computational Analysis of the EDHOC Lightweight Authenticated Key Exchange Protocol. In 2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P). IEEE, 773\u2013796","author":"G\u00fcnther Felix","year":"2023","unstructured":"Felix G\u00fcnther and Marc Ilunga Tshibumbu Mukendi. 2023. Careful with MAc-then-SIGn: A Computational Analysis of the EDHOC Lightweight Authenticated Key Exchange Protocol. In 2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P). IEEE, 773\u2013796."},{"key":"e_1_3_2_1_23_1","unstructured":"Internet Assigned Numbers Authority (LANA) [n. d.]. IANA EDHOC Parameters Registry. Accessed: 2025-02-10."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/3620237.3620566"},{"key":"e_1_3_2_1_25_1","volume-title":"Sangmin Lee, Bonam Kim, JaeDeok Lim, and Ilsun You.","author":"Kim Jiyoon","year":"2021","unstructured":"Jiyoon Kim, Daniel Gerbi Duguma, Sangmin Lee, Bonam Kim, JaeDeok Lim, and Ilsun You. 2021. Scrutinizing the Vulnerability of Ephemeral Diffie-Hellman over COSE (EDHOC) for IoT Environment Using Formal Approaches. Mobile Information Systems (2021), 1\u201318."},{"key":"e_1_3_2_1_26_1","unstructured":"J. Koo. 2021. Internet of Things Security Case Studies and Solutions. Ph.D. Dissertation. California State University San Bernardino. https:\/\/scholarworks.lib.csusb.edu\/cgi\/viewcontent.cgi?article=2455&context=etd Contains case studies of IoT products (e.g. smart meters EV chargers IP cameras) using PSK or password authentication and discusses their vulnerabilities."},{"key":"e_1_3_2_1_27_1","volume-title":"SIGMA: The \u2018SIGn-and-MAc","author":"Krawczyk Hugo","year":"2003","unstructured":"Hugo Krawczyk. 2003. SIGMA: The \u2018SIGn-and-MAc\u2019 Approach to Authenticated Diffie-Hellman and Its Use in the IKE Protocols. In Advances in Cryptology -CRYPTO 2003. Springer Berlin Heidelberg, Berlin, Heidelberg, 400\u2013425."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2006.52"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54631-0_38"},{"key":"e_1_3_2_1_30_1","volume-title":"Rafael Marin-Lopez, and Francisco Lopez-Gomez.","author":"Lopez-Perez Elsa","year":"2025","unstructured":"Elsa Lopez-Perez, G\u00f6ran Selander, John Preu\u00df Mattsson, Rafael Marin-Lopez, and Francisco Lopez-Gomez. 2025. EDHOC Authenticated with Pre-Shared Keys (PSK). Work in Progress."},{"key":"e_1_3_2_1_31_1","volume-title":"Cristina Onete, Clement Papon, and Mali\u0161a Vu\u010dini\u00e9.","author":"Perez Elsa Lopez","year":"2025","unstructured":"Elsa Lopez Perez, Thomas Watteyne, Rafael Marin Lopez, Cristina Onete, Clement Papon, and Mali\u0161a Vu\u010dini\u00e9. 2025. Pre-Shared Key Authentication with EDHOC: the Security-Performance Tradeoff. IEEE Access (2025)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795075"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_1_34_1","unstructured":"NIST. 2016. Report on Post-Quantum Cryptography. Technical Report NISTLR 8105. National Institute of Standards and Technology."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Karl Norrman Vaishnavi Sundararajan and Alessandro Bruni. 2020. Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. CoRR abs\/2007.11427(2020).","DOI":"10.5220\/0010554000002998"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2024.3415908"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.23919\/PEMWN50727.2020.9293085"},{"key":"e_1_3_2_1_38_1","volume-title":"John Preu\u00df Mattsson, and Francesca Palombini","author":"Seiander G\u00f6ran","year":"2024","unstructured":"G\u00f6ran Seiander, John Preu\u00df Mattsson, and Francesca Palombini. 2024. Ephemeral Diffie-Hellman Over COSE (EDHOC)."},{"key":"e_1_3_2_1_39_1","volume-title":"A Survey of Chosen-Prefix Collision Attacks. Computational Cryptography","author":"Stevens M.M.J.","year":"2021","unstructured":"M.M.J. Stevens. 2021. A Survey of Chosen-Prefix Collision Attacks. Computational Cryptography (2021). https:\/\/api.semanticscholar.org\/CorpusID:236467675"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2022.3144764"},{"key":"e_1_3_2_1_41_1","volume-title":"Technical Overview of SmartMesh LP. In 2013 Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing. 547\u2013551","author":"Watteyne Thomas","year":"2013","unstructured":"Thomas Watteyne, Lance Doherty, Jonathan Simon, and Kris Pister. 2013. Technical Overview of SmartMesh LP. In 2013 Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing. 547\u2013551."}],"event":{"name":"ASIA CCS '26: ACM Asia Conference on Computer and Communications Security","location":"Bangalore India","acronym":"ASIA CCS '26","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the ACM Asia Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779208.3805979","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T15:40:10Z","timestamp":1780587610000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779208.3805979"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":41,"alternative-id":["10.1145\/3779208.3805979","10.1145\/3779208"],"URL":"https:\/\/doi.org\/10.1145\/3779208.3805979","relation":{},"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"2026-06-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}