{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T16:50:41Z","timestamp":1781974241295,"version":"3.54.5"},"reference-count":52,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T00:00:00Z","timestamp":1651363200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1109\/sp46214.2022.9833777","type":"proceedings-article","created":{"date-parts":[[2022,7,27]],"date-time":"2022-07-27T19:28:05Z","timestamp":1658950085000},"page":"2285-2303","source":"Crossref","is-referenced-by-count":30,"title":["Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities"],"prefix":"10.1109","author":[{"given":"Jianliang","family":"Wu","sequence":"first","affiliation":[{"name":"Purdue University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ruoyu","family":"Wu","sequence":"additional","affiliation":[{"name":"Purdue University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dongyan","family":"Xu","sequence":"additional","affiliation":[{"name":"Purdue University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dave Jing","family":"Tian","sequence":"additional","affiliation":[{"name":"Purdue University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antonio","family":"Bianchi","sequence":"additional","affiliation":[{"name":"Purdue University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref13","year":"2020","journal-title":"CVE-2020-26560"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"ref15","year":"2020","journal-title":"Bluetooth SIG Statement Regarding the Exploiting Cross-Transport Key Derivation in Bluetooth Classic and Bluetooth Low Energy (BLURtooth) and the Security implications of key conversion between BR\/EDR and BLE Vulnerabilities"},{"key":"ref14","year":"2021","journal-title":"Bluetooth SIG Statement Regarding the ‘Impersonation Attack in Bluetooth Mesh Provisioning’ Vulnerability"},{"key":"ref52","author":"perrin","year":"2021","journal-title":"The noise protocol framework"},{"key":"ref11","article-title":"A Study of the Feasibility of Co-located App Attacks against BLE and a Large-Scale Analysis of the Current Application-Layer Security Landscape","author":"sivakumaran","year":"2019","journal-title":"Proceedings of the USENIX Security Symposium (USENIX Security)"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23097"},{"key":"ref17","year":"2019","journal-title":"Mesh Profile Specifications 1 0"},{"key":"ref16","year":"0","journal-title":"Model Implementation and Attack Trace Explanation"},{"key":"ref19","article-title":"The KNOB is Broken: Exploiting Low Entropy in the Encryption Key Negotiation Of Bluetooth BR\/EDR","author":"antonioli","year":"2019","journal-title":"Proceedings of the USENIX Security Symposium (USENIX Security)"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00093"},{"key":"ref51","article-title":"A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols","author":"girol","year":"2020","journal-title":"Proceedings of the USENIX Security Symposium (USENIX Security)"},{"key":"ref50","doi-asserted-by":"crossref","DOI":"10.1109\/EuroSP.2017.38","article-title":"Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach","author":"kobeissi","year":"2017","journal-title":"Proceedings of the IEEE European Symposium on Security and Privacy (EuroS&P)"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/11535218_7"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28628-8_25"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2133375.2133378"},{"key":"ref47","author":"marlinspike","year":"2016","journal-title":"Signal on the outside Signal on the inside"},{"key":"ref42","article-title":"BLURtooth: Exploiting Cross-Transport Key Derivation in Bluetooth Classic and Bluetooth Low Energy","author":"antonioli","year":"2020","journal-title":"ArXiv"},{"key":"ref41","article-title":"The TAMARIN Prover for the Symbolic Analysis of Security Protocols","author":"meier","year":"2013","journal-title":"Computer Aided Verification (CAV)"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50011-9_31"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/TrustCom.2012.182"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23482"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00013"},{"key":"ref9","year":"2019","journal-title":"Bluetooth Core Specification"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3321705.3329813"},{"key":"ref3","article-title":"Formal Verification of Improved Numeric Comparison Protocol for Secure Simple Pairing in Bluetooth Using ProVerif","author":"arai","year":"2014","journal-title":"Proceedings of the International Conference on Security and Management (SAM)"},{"key":"ref6","article-title":"BLESA: Spoofing Attacks against Reconnections in Bluetooth Low Energy","author":"wu","year":"2020","journal-title":"Proceedings of the USENIX Workshop on Offensive Technologies (WOOT)"},{"key":"ref5","article-title":"Prime, Order Please! revisiting Small Subgroup and Invalid CurveAttacks on ProtocolsUsingDiffie-Hellman","author":"cremers","year":"2019","journal-title":"Proceedings of the IEEE Computer Security Foundations Symposium (CSF)"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"ref35","year":"2020","journal-title":"Human Interface Device (HID) Profile"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/SPW53761.2021.00054"},{"key":"ref37","year":"2020","journal-title":"CVE-2020-15802"},{"key":"ref36","year":"2020","journal-title":"Save reversed BR\/EDR link key derived from LE LTK"},{"key":"ref31","year":"2020","journal-title":"Bluetooth mesh SDK 2 0 0 0 GA"},{"key":"ref30","year":"2019","journal-title":"BlueZ"},{"key":"ref33","year":"2020","journal-title":"Apache NimBLE"},{"key":"ref32","year":"2020","journal-title":"Zephyr Bluetooth"},{"key":"ref2","article-title":"Formal Analysis of Authentication in Bluetooth Device Pairing","author":"chang","year":"2007","journal-title":"Proceedings of the LICS\/ICALP Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA)"},{"key":"ref1","year":"2019","journal-title":"Bluetooth market update 2019"},{"key":"ref39","article-title":"Bluetooth:With Low Energy Comes Low Security","author":"ryan","year":"2013","journal-title":"Proceedings of the USENIX Workshop on Offensive Technologies (WOOT)"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3448609"},{"key":"ref24","article-title":"Inaudible Voice Commands: The Long-Range Attack and Defense","author":"roy","year":"2018","journal-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)"},{"key":"ref23","article-title":"Breaking the Bluetooth Pairing–The Fixed Coordinate Invalid Curve Attack","author":"biham","year":"2019","journal-title":"Proceedings of the International Conference on Selected Areas in Cryptography (SAC)"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.29"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00016"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3394497"},{"key":"ref22","article-title":"Securing Bluetooth Communications","volume":"14","author":"yeh","year":"2012","journal-title":"IJ Network Security"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref28","year":"2020","journal-title":"nRF Mesh"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2004.1301317"},{"key":"ref29","year":"2020","journal-title":"ST BLE Mesh"}],"event":{"name":"2022 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA, USA","start":{"date-parts":[[2022,5,22]]},"end":{"date-parts":[[2022,5,26]]}},"container-title":["2022 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9833550\/9833558\/09833777.pdf?arnumber=9833777","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T23:06:13Z","timestamp":1699484773000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9833777\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5]]},"references-count":52,"URL":"https:\/\/doi.org\/10.1109\/sp46214.2022.9833777","relation":{},"subject":[],"published":{"date-parts":[[2022,5]]}}}