BLE Privacy Model

This repo is used to reproduce the result in Tables 6 and 7 of our paper: Finding Traceability Attacks in the Bluetooth Low Energy Specification and Its Implementations.

Bibtex:

@inproceedings {294502,
  author = {Jianliang Wu and Patrick Traynor and Dongyan Xu and Dave (Jing) Tian and Antonio Bianchi},
  title = {Finding Traceability Attacks in the Bluetooth Low Energy Specification and Its Implementations},
  booktitle = {33rd USENIX Security Symposium (USENIX Security 24)},
  year = {2024},
  address = {Philadelphia, PA},
  url = {https://www.usenix.org/conference/usenixsecurity24/presentation/wu-jianliang},
  publisher = {USENIX Association},
  month = aug
}

Execute scripts/run_all_reachability.sh to run the verification automatically using the reachability-based privacy model. It may take up to 2 hours.

Execute scripts/run_all_oe.sh to run the verification automatically using the OE-based privacy model.

These two scripts call other scripts (the script's name starts with per-device or per-pairing) to verify the privacy of BLE. You can also execute these scripts separately.

Dependence

M4 and ProVerif (tested with ProVerif version 2.04).

File explanation

• The name of the *.sh script files explains which scenario this script verifies. For example, the per-device_central_active_tracker.sh verifies the scenario where the target device adopts the per-device design, the target device is the central role, and the tracker is an active tracker. In each script, all three relations (i.e., never, paired, and unpaired) and all five identifiers (i.e., PK, LTK, IRK, CSRK, and ID_ADDR) are covered.

• The model folder contains the formal model of BLE privacy. The script utilizes the models in this folder to verify BLE privacy.

• The results.zip contains the verification result. You can also generate this by yourself using our scripts. In the reachability-results folder, there are eight sub-folders. Each of the sub-folders is generated by one of the eight scripts under the scripts/reachability folder (the per-device and per-pairing scripts). In each of the sub-folders, there are several sub-sub-folders containing the verification result. For example, the folder reachability-results/per-device-central-active-tracker/Never-1-P2 contains the verification result of the 1 row, P2 column, of the per-device design in Table 6. You can open the index.html file in the folder to check the result. If the property can be violated, there is also a trace*.pdf file in the folder showing the trace that can violate this property.

• In the observational_equivalence-results folder, there are four sub-folders. Each of the sub-folder is generated by one of the four scripts under the scripts/observational_equivalence folder (the per-device scripts). In each of the sub-folders, there are several sub-sub-folders containing the verification result. For example, the folder observational_equivalence-results/per-device-central-active-tracker/Never-1-PK contains the verification result of the 1 row, Active Tracker/Result column in Table 7. You can open the index.html file in the folder to check the result. If the property can be violated, there is also a trace*.pdf file in the folder showing the trace that can violate this property.

Attack demo videos

Attack 1

Attack 4