{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:00:22Z","timestamp":1750309222506,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7]]},"DOI":"10.1145\/3634737.3637667","type":"proceedings-article","created":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T11:51:38Z","timestamp":1719575498000},"page":"753-768","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Segment-Based Formal Verification of WiFi Fragmentation and Power Save Mode"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5342-0998","authenticated-orcid":false,"given":"Zilin","family":"Shen","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8680-9932","authenticated-orcid":false,"given":"Imtiaz","family":"Karim","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4029-7051","authenticated-orcid":false,"given":"Elisa","family":"Bertino","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Android Developers. 2023. Android Debug Bridge (adb). (2023). https:\/\/developer.android.com\/tools\/adb."},{"volume-title":"Studies in Logic and the Foundations of Mathematics.","author":"Barwise Jon","key":"e_1_3_2_1_2_1","unstructured":"Jon Barwise. 1977. An introduction to first-order logic. In Studies in Logic and the Foundations of Mathematics. Vol. 90. Elsevier, 5--46."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1997.646128"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2021.103058"},{"key":"e_1_3_2_1_6_1","volume-title":"USENIX Association","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, (Aug. 2022), 3935--3952. isbn: 978-1-939133-31-1. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/cheval."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2016.2548426"},{"key":"e_1_3_2_1_8_1","volume-title":"Network and Distributed System Security Symposium (NDSS). Internet Society.","author":"Cremers Cas","year":"2019","unstructured":"Cas Cremers and Martin Dehnel-Wild. 2019. Component-based formal analysis of 5g-aka: channel assumptions and session confusion. In Network and Distributed System Security Symposium (NDSS). Internet Society."},{"key":"e_1_3_2_1_9_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Cremers Cas","year":"2020","unstructured":"Cas Cremers, Benjamin Kiesl, and Niklas Medinger. 2020. A formal analysis of IEEE 802.11's WPA2: countering the kracks caused by cracking the counters. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, (Aug. 2020), 1--17. isbn: 978-1-939133-17-5. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/cremers."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","first-page":"247","DOI":"10.3233\/JCS-2004-12203","article-title":"Multiset rewriting and the complexity of bounded security protocols","volume":"12","author":"Durgin Nancy","year":"2004","unstructured":"Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov. 2004. Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security, 12, 2, 247--311.","journal-title":"Journal of Computer Security"},{"key":"e_1_3_2_1_12_1","unstructured":"2023. Formal model implementation and attack testing. (2023). https:\/\/github.com\/Zilinlin\/FunctionalWifiModelTesting."},{"volume-title":"Lte-advanced: next-generation wireless broadband technology","author":"Ghosh Amitava","key":"e_1_3_2_1_13_1","unstructured":"Amitava Ghosh, Rapeepat Ratasuk, Bishwarup Mondal, Nitin Mangalvedhe, and Tim Thomas. 2010. Lte-advanced: next-generation wireless broadband technology. IEEE wireless communications, 17, 3, 10--22."},{"key":"e_1_3_2_1_14_1","volume-title":"Recent Advances in Intrusion Detection: 8th International Symposium, RAID 2005","author":"Guo Fanglu","year":"2006","unstructured":"Fanglu Guo and Tzi-cker Chiueh. 2006. Sequence number-based mac address spoof detection. In Recent Advances in Intrusion Detection: 8th International Symposium, RAID 2005, Seattle, WA, USA, September 7--9, 2005. Revised Papers 8. Springer, 309--329."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2015.2461602"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/98.824570"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23313"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354263"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2021.9363693"},{"key":"e_1_3_2_1_20_1","unstructured":"Charlie Jacomme Elise Klein Steve Kremer and Ma\u00efwenn Racouchot. 2023. A comprehensive formal and automated analysis of the edhoc protocol. In USENIX Security'23-32nd USENIX Security Symposium."},{"key":"e_1_3_2_1_21_1","unstructured":"Brian W Kernighan and Dennis M Ritchie. 1977. The M4 macro processor. Bell Laboratories Murray Hill NJ."},{"key":"e_1_3_2_1_22_1","first-page":"11","article-title":"A comprehensive attack flow model and security analysis for wi-fi and wpa3","volume":"7","author":"Kohlios Christopher P","year":"2018","unstructured":"Christopher P Kohlios and Thaier Hayajneh. 2018. A comprehensive attack flow model and security analysis for wi-fi and wpa3. Electronics, 7, 11, 284.","journal-title":"Electronics"},{"key":"e_1_3_2_1_23_1","unstructured":"2020. Kr00k: a serious vulnerability deep inside wi-fi encryption. (2020). https:\/\/www.eset.com\/int\/kr00k\/."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3488932.3517425"},{"key":"e_1_3_2_1_26_1","volume-title":"2019 IEEE International Conference on Computational Electromagnetics (ICCEM). IEEE, 1--3.","author":"Liu Songyi","year":"2019","unstructured":"Songyi Liu. 2019. Mac spoofing attack detection based on physical layer characteristics in wireless networks. In 2019 IEEE International Conference on Computational Electromagnetics (ICCEM). IEEE, 1--3."},{"key":"e_1_3_2_1_27_1","volume-title":"Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25","author":"Meier Simon","year":"2013","unstructured":"Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The tamarin prover for the symbolic analysis of security protocols. In Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. Springer, 696--701."},{"key":"e_1_3_2_1_28_1","volume-title":"Kamlesh Kumar, Shibin David, and Munwar Ali.","author":"Nazir Rashid","year":"2021","unstructured":"Rashid Nazir, Asif Ali Laghari, Kamlesh Kumar, Shibin David, and Munwar Ali. 2021. Survey on wireless network security. Archives of Computational Methods in Engineering, 1--20."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1216370.1216373"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the 8th international conference on Mobile systems, applications, and services, 91--106","author":"Rozner Eric","year":"2010","unstructured":"Eric Rozner, Vishnu Navda, Ramachandran Ramjee, and Shravan Rayanchu. 2010. Napman: network-assisted power management for wifi devices. In Proceedings of the 8th international conference on Mobile systems, applications, and services, 91--106."},{"key":"e_1_3_2_1_31_1","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Schepers Domien","year":"2023","unstructured":"Domien Schepers, Aanjhan Ranganathan, and Mathy Vanhoef. 2023. Framing frames: bypassing wi-fi encryption by manipulating transmit queues. In 32nd USENIX Security Symposium (USENIX Security 23)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3448300.3468261"},{"key":"e_1_3_2_1_33_1","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Shi Min","year":"2023","unstructured":"Min Shi, Jing Chen, Kun He, Haoran Zhao, Meng Jia, and Ruiying Du. 2023. Formal analysis and patching of BLE-SC pairing. In 32nd USENIX Security Symposium (USENIX Security 23). USENIX Association, Anaheim, CA, (Aug. 2023), 37--52. isbn: 978-1-939133-37-3. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/shi-min."},{"key":"e_1_3_2_1_34_1","unstructured":"Tcpdump Group. 1999-2023. TCPDUMP. (1999-2023). https:\/\/www.tcpdump.org\/."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514274.1514286"},{"key":"e_1_3_2_1_36_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Vanhoef Mathy","year":"2021","unstructured":"Mathy Vanhoef. 2021. Fragment and forge: breaking Wi-Fi through frame aggregation and fragmentation. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, (Aug. 2021), 161--178. isbn: 978-1-939133-24-3. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/vanhoef."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2664243.2664260"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134027"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243807"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00031"},{"key":"e_1_3_2_1_41_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Qinying","year":"2021","unstructured":"Qinying Wang et al. 2021. MPInspector: a systematic and automatic approach for evaluating the security of IoT messaging protocols. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, (Aug. 2021), 4205--4222. isbn: 978-1-939133-24-3. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/wang-qinying."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833777"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00052"}],"event":{"name":"ASIA CCS '24: 19th ACM Asia Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Singapore Singapore","acronym":"ASIA CCS '24"},"container-title":["Proceedings of the 19th ACM Asia Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3634737.3637667","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:06Z","timestamp":1750290246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3634737.3637667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7]]},"references-count":43,"alternative-id":["10.1145\/3634737.3637667","10.1145\/3634737"],"URL":"https:\/\/doi.org\/10.1145\/3634737.3637667","relation":{},"subject":[],"published":{"date-parts":[[2024,7]]},"assertion":[{"value":"2024-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}