近日，我院2019級博士研究生石閩等人論文“Formal Analysis and Patching of BLE-SC Pairing”被第32屆USENIX Security會議錄用。該研究工作在我院陳晶教授（通信作者）、杜瑞穎教授、何琨副研究員，聯合指導下完成，我院2020級博士生加夢、2020級碩士生趙浩然參與了該成果的研究工作。
USENIX Security與IEEE S&P、ACM CCS、NDSS并稱為安全領域四大頂級會議，已有30餘年的曆史，對信息安全領域具有重要影響，同時被中國計算機學會（CCF）認定為網絡安全A類國際學術會議。
藍牙低功耗（BLE）是主流的藍牙标準，而BLE安全連接（BLC-SC）配對是一種認證兩個藍牙設備并在它們之間導出共享密鑰的協議。盡管BLE-SC配對采用了經過充分研究的密碼原語以保證其安全性，但最近的研究發現了該協議中的邏輯缺陷。
在該研究中，作者開發了BLE-SC配對協議的第一個全面的形式模型，該模型符合最新的藍牙規範5.3版本，并涵蓋了規範中所有關聯模型，以發現不同關聯模型之間相互作用引起的攻擊。通過設計低熵密鑰預言機，部分放寬了傳統符号分析方法中完美密碼假設，以檢測由劣質密鑰引起的攻擊。分析證實了兩個現有攻擊，并披露了一個新攻擊。針對BLE-SC配對協議的邏輯缺陷，作者提出一個後向兼容的修補方案，并在符号模型中證明了修補對策的有效性。
