近日，云顶集团yd12332019级博士研究生石闽等人论文“Formal Analysis and Patching of BLE-SC Pairing”被第32届USENIX Security会议录用。该研究工作在云顶集团yd1233陈晶教授（通信作者）、杜瑞颖教授、何琨副研究员，联合指导下完成，云顶集团yd12332020级博士生加梦、2020级硕士生赵浩然参与了该成果的研究工作。

USENIX Security与IEEE S&P、ACM CCS、NDSS并称为安全领域四大顶级会议，已有30余年的历史，对信息安全领域具有重要影响，同时被中国计算机学会（CCF）认定为网络安全A类国际学术会议。

蓝牙低功耗（BLE）是主流的蓝牙标准，而BLE安全连接（BLC-SC）配对是一种认证两个蓝牙设备并在它们之间导出共享密钥的协议。尽管BLE-SC配对采用了经过充分研究的密码原语以保证其安全性，但最近的研究发现了该协议中的逻辑缺陷。

在该研究中，作者开发了BLE-SC配对协议的第一个全面的形式模型，该模型符合最新的蓝牙规范5.3版本，并涵盖了规范中所有关联模型，以发现不同关联模型之间相互作用引起的攻击。通过设计低熵密钥预言机，部分放宽了传统符号分析方法中完美密码假设，以检测由劣质密钥引起的攻击。分析证实了两个现有攻击，并披露了一个新攻击。针对BLE-SC配对协议的逻辑缺陷，作者提出一个后向兼容的修补方案，并在符号模型中证明了修补对策的有效性。