{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T02:33:02Z","timestamp":1755225182965,"version":"3.43.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["SEVERITAS (ANR-20-CE39-0009), PRIVA-SIQ (ANR-23-CE39-0008)"],"award-info":[{"award-number":["SEVERITAS (ANR-20-CE39-0009), PRIVA-SIQ (ANR-23-CE39-0008)"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["INDID, C-ROADS, SCALE"],"award-info":[{"award-number":["INDID, C-ROADS, SCALE"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["SEVERITAS (ANR-20-CE39-0009), PRIVA-SIQ (ANR-23-CE39-0008)"],"award-info":[{"award-number":["SEVERITAS (ANR-20-CE39-0009), PRIVA-SIQ (ANR-23-CE39-0008)"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["INDID, C-ROADS, SCALE"],"award-info":[{"award-number":["INDID, C-ROADS, SCALE"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,8,25]]},"DOI":"10.1145\/3708821.3710828","type":"proceedings-article","created":{"date-parts":[[2025,8,13]],"date-time":"2025-08-13T06:30:56Z","timestamp":1755066656000},"page":"1476-1489","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Analysis of SDNsec: Attacks and Corrections for Payload, Route Integrity and Accountability"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-6485-2782","authenticated-orcid":false,"given":"Ayoub","family":"Ben Hassen","sequence":"first","affiliation":[{"name":"\u00c9cole Sup\u00e9rieure des Communications, Tunis, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4459-511X","authenticated-orcid":false,"given":"Pascal","family":"Lafourcade","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Clermont Auvergne, CNRS, Clermont Auvergne INP, Mines Saint-Etienne, LIMOS, 63000 Clermont-Ferrand, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0555-0581","authenticated-orcid":false,"given":"Dhekra","family":"Mahmoud","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Clermont Auvergne, CNRS, Clermont Auvergne INP, Mines Saint-Etienne, LIMOS, 63000 Clermont-Ferrand, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6127-9816","authenticated-orcid":false,"given":"Maxime","family":"Puys","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Clermont Auvergne, CNRS, Clermont Auvergne INP, Mines Saint-Etienne, LIMOS, 63000 Clermont-Ferrand, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,8,24]]},"reference":[{"key":"e_1_3_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Mart\u00edn Abadi Bruno Blanchet and C\u00e9dric Fournet. 2017. The Applied Pi Calculus: Mobile Values New Names and Secure Communication. J. ACM 65 1 Article 1 (oct 2017) 41\u00a0pages. 10.1145\/3127586","DOI":"10.1145\/3127586"},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Mathilde Arnaud V\u00e9ronique Cortier and St\u00e9phanie Delaune. 2014. Modeling and verifying ad hoc routing protocols. Inf. Comput. 238 (2014) 30\u201367. 10.1016\/J.IC.2014.07.004","DOI":"10.1016\/J.IC.2014.07.004"},{"key":"e_1_3_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14629053"},{"key":"e_1_3_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Conor Black and Sandra Scott-Hayward. 2021. A Survey on the Verification of Adversarial Data Planes in Software-Defined Networks. Proceedings of the ACM International Workshop on Software Defined Networks & Network Function Virtualization Security SDN-NFV Sec 2021. 10.1145\/3445968.3452092","DOI":"10.1145\/3445968.3452092"},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_3_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Alessandro Bruni Rosario Giustolisi and Carsten Schuermann. 2017. Automated Analysis of Accountability. 417\u2013434. 10.1007\/978-3-319-69659-123","DOI":"10.1007\/978-3-319-69659-123"},{"key":"e_1_3_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1029102.1029119"},{"key":"e_1_3_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_50"},{"key":"e_1_3_3_2_12_2","volume-title":"31st USENIX Security Symposium (USENIX Security 22)","author":"Cheval Vincent","year":"2022","unstructured":"Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert K\u00fcnnemann. 2022. SAPIC+: protocol verifiers of the world, unite!. In 31st USENIX Security Symposium (USENIX Security 22). USENIX Association, Boston, MA. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/cheval"},{"key":"e_1_3_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00033"},{"key":"e_1_3_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.15"},{"key":"e_1_3_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-70890-9_21"},{"key":"e_1_3_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_3"},{"key":"e_1_3_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243762"},{"key":"e_1_3_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"e_1_3_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02002-5_5"},{"key":"e_1_3_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/INM.2015.7140289"},{"key":"e_1_3_3_2_21_2","doi-asserted-by":"publisher","unstructured":"St\u00e9phanie Delaune Steve Kremer and Mark Ryan. 2009. Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17 4 (2009) 435\u2013487. 10.3233\/JCS-2009-0340","DOI":"10.3233\/JCS-2009-0340"},{"key":"e_1_3_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Mohan Dhawan Rishabh Poddar Kshiteej Mahajan and Vijay Mann. 2015. SPHINX: Detecting Security Attacks in Software-Defined Networks.","DOI":"10.14722\/ndss.2015.23064"},{"key":"e_1_3_3_2_23_2","doi-asserted-by":"publisher","unstructured":"D. Dolev and A. Yao. 1983. On the security of public key protocols. IEEE Transactions on Information Theory 29 2 (1983) 198\u2013208. 10.1109\/TIT.1983.1056650","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-71"},{"key":"e_1_3_3_2_25_2","doi-asserted-by":"crossref","unstructured":"Marco\u00a0Longhi Gelati Giovanni Neri Pierantonio Natali Richard C.\u00a0S. Morling Gerald\u00a0D. Cain and Eugenio Faldella. 1984. MININET: A Local Area Network for Real-Time Instrumentation Applications. Comput. Networks 8 (1984) 107\u2013131.","DOI":"10.1016\/0376-5075(84)90039-4"},{"key":"e_1_3_3_2_26_2","doi-asserted-by":"publisher","unstructured":"H. Hu W. Han G.-J. Ahn and Z. Zhao. 2014. FLOWGUARD: Building Robust Firewalls for Software-Defined Networks. Proceedings of the Third Workshop on Hot Topics in Software Defined Networking HotSDN\u201914 97\u2013102. 10.1145\/2620728.2620749","DOI":"10.1145\/2620728.2620749"},{"key":"e_1_3_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342467"},{"key":"e_1_3_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2809826.2809833"},{"key":"e_1_3_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/WoWMoM.2014.6918979"},{"key":"e_1_3_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Ahmed Khurshid Xuan Zou Wenxuan Zhou Matthew Caesar and P.\u00a0Brighten Godfrey. 2012. Veriflow: Verifying Network-wide Invariants in Real Time. ACM SIGCOMM Computer Communication Review 42 (2012) 467\u2013472.","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_3_3_2_31_2","unstructured":"Nadim Kobeissi Georgio Nicolas and Mukesh Tiwari. 2019. Verifpal: Cryptographic Protocol Analysis for the Real World. Cryptology ePrint Archive Paper 2019\/971. https:\/\/eprint.iacr.org\/2019\/971"},{"key":"e_1_3_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00034"},{"key":"e_1_3_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866366"},{"key":"e_1_3_3_2_34_2","first-page":"137","volume-title":"International Symposium on Foundations and Practice of Security","author":"Lafourcade Pascal","year":"2015","unstructured":"Pascal Lafourcade and Maxime Puys. 2015. Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In International Symposium on Foundations and Practice of Security. Springer, 137\u2013155."},{"key":"e_1_3_3_2_35_2","doi-asserted-by":"crossref","unstructured":"Gavin Lowe. 1995. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Inform. Process. Lett. 56 3 (1995) 131\u2013133.","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"e_1_3_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1997.596782"},{"key":"e_1_3_3_2_37_2","doi-asserted-by":"crossref","unstructured":"Nick McKeown Tom Anderson Hari Balakrishnan Guru Parulkar Larry Peterson Jennifer Rexford Scott Shenker and Jonathan Turner. 2008. OpenFlow: Enabling Innovation in Campus Networks. ACM CCR (2008).","DOI":"10.1145\/1355734.1355746"},{"key":"e_1_3_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00032"},{"key":"e_1_3_3_2_40_2","unstructured":"Mahamat\u00a0Charfadine Salim. 2019. Gestion dynamique et \u00e9volutive de r\u00e8gles de s\u00e9curit\u00e9 pour l\u2019Internet des Objets. Ph.\u00a0D. Dissertation. Universit\u00e9 de Reims Champagne-Ardenne. Th\u00e8se de doctorat."},{"key":"e_1_3_3_2_41_2","doi-asserted-by":"crossref","unstructured":"Takayuki Sasaki Christos Pappas Taeho Lee Torsten Hoefler and Adrian Perrig. 2016. SDNsec: Forwarding Accountability for the SDN Data Plane. NEC Corporation Japan and ETH Zurich Switzerland (2016). Available: NEC Corporation and ETH Zurich.","DOI":"10.1109\/ICCCN.2016.7568569"},{"key":"e_1_3_3_2_42_2","volume-title":"Proc. of Workshop on Hot Topics in Software Defined Networking","author":"Schlesinger Cole","year":"2012","unstructured":"Cole Schlesinger, Alec Story, Stephen Gutz, Nate Foster, and David Walker. 2012. Splendid isolation: Language-based security for software-defined networks. In Proc. of Workshop on Hot Topics in Software Defined Networking."},{"key":"e_1_3_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3052973.3053039"},{"key":"e_1_3_3_2_44_2","unstructured":"Rob Sherwood Glen Gibb Kok-Kiong Yap Guido Appenzeller Martin Casado Nick McKeown and Guru Parulkar. 2009. Flowvisor: A network virtualization layer. OpenFlow Switch Consortium Tech. Rep 1 (2009) 132."},{"key":"e_1_3_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Takahiro Shimizu Naoya Kitagawa Kohta Ohshima and Nariyoshi Yamai. 2019. WhiteRabbit: Scalable Software-Defined Network Data-Plane Verification Method Through Time Scheduling. (2019). 10.1109\/ACCESS.2019.2929958","DOI":"10.1109\/ACCESS.2019.2929958"},{"key":"e_1_3_3_2_46_2","doi-asserted-by":"crossref","unstructured":"P.\u00a0P.\u00a0S. Shin V. Yegneswaran and G. Gu. 2013. Avant-Guard: Scalable and Vigilant Switch Flow Management in Software-Defined Networks. CProceedings of the 2013 ACM SIGSAC conference on Computer & communications security (2013) 413\u2013424.","DOI":"10.1145\/2508859.2516684"},{"key":"e_1_3_3_2_47_2","volume-title":"RYU SDN Framework - English Edition","author":"team RYU","year":"2014","unstructured":"RYU team. 2014. RYU SDN Framework - English Edition. RYU project team. https:\/\/books.google.fr\/books?id=JC3rAgAAQBAJ"},{"key":"e_1_3_3_2_48_2","doi-asserted-by":"publisher","unstructured":"T. Xing D. Huang C.-J.\u00a0Chung L.\u00a0Xu and P. Khatkar. 2013. SnortFlow: an OpenFlow-based intrusion prevention system in cloud environment. Second GENI Research and Educational Experiment Workshop (GREE) 89\u201392. 10.1109\/GREE.2013.25","DOI":"10.1109\/GREE.2013.25"},{"key":"e_1_3_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47717-6_20"},{"key":"e_1_3_3_2_50_2","unstructured":"V. Yegneswaran M. Fong M. Thottan P. Porras S. Shin and G. Gu. 2012. A security enforcement kernel for OpenFlow networks. ACM."},{"key":"e_1_3_3_2_51_2","doi-asserted-by":"crossref","unstructured":"Peng Zhang Hui Wu Dan Zhang and Qi Li. 2020. Verifying Rule Enforcement in Software Defined Networks With REV. IEEE\/ACM Transactions on Networking (2020).","DOI":"10.1109\/TNET.2020.2977006"},{"key":"e_1_3_3_2_52_2","unstructured":"Peng Zhang Shimin Xu Zuoru Yang Hao Li Qi Li Huanzhao Wang and Chengchen Hu. 2020. FOCES: Detecting Forwarding Anomalies in Software Defined Networks. (2020)."}],"event":{"name":"ASIA CCS '25: 20th ACM Asia Conference on Computer and Communications Security","location":"Hanoi Vietnam","acronym":"ASIA CCS '25","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 20th ACM Asia Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3708821.3710828","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,13]],"date-time":"2025-08-13T07:32:52Z","timestamp":1755070372000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708821.3710828"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,24]]},"references-count":51,"alternative-id":["10.1145\/3708821.3710828","10.1145\/3708821"],"URL":"https:\/\/doi.org\/10.1145\/3708821.3710828","relation":{},"subject":[],"published":{"date-parts":[[2025,8,24]]},"assertion":[{"value":"2025-08-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}