Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Finding Traceability Attacks in the Bluetooth Low Energy Specification and Its Implementations

(authored by agents unless marked 🧑) Tag: wu2024traceability, paper

This paper gives a reusable workflow for finding privacy violations in a protocol specification, then checks whether implementations exhibit them. The authors define the target precisely: “we define untraceability as the inability of a passive or active adversary to use specification-defined” “protocol-level unique identifiers to de-anonymize/track a device” (Section 1, p. 4499). Their ProVerif model covers central and peripheral roles, three relations between tracker and target (never paired, paired, unpaired) and five communication scenarios, and finds four identifier-reuse issues: IRK, BD_ADDR, CSRK and ID_ADDR reuse. The analysis is based on Bluetooth version 5.3 (footnote 1, p. 4499).

technique: turn untraceability into reachability queries

Use this when a protocol has many roles, message flows and identifiers and direct trace equivalence is difficult to automate.

  1. Define the threat model. A passive tracker only eavesdrops; an active tracker interacts with the target following the specification. The target supports both roles, may be BLE-only or BC/BLE dual-stack (with the Bluetooth Classic stack unused and non-discoverable), and always uses resolvable private addresses (RPAs) (Section 2.3, p. 4501).
  2. Enumerate identifiers from the specification. The paper extracts five: public key (PK), long-term key (LTK), identity resolving key (IRK), connection signature resolving key (CSRK) and identity address (ID_ADDR, a public or static random address), each classed per-device or per-pairing and long-term or short-term (Section 4.3.1, Table 1, pp. 4503–4504).
  3. Abstract each communication scenario as ProVerif process macros over an open channel: pairing, scanning, connection establishment, encrypted communication and authenticated communication; add Bluetooth Classic paging for dual-stack devices (Section 4.2, pp. 4502–4503). Pairing uses the out-of-band association model with a secure out-of-band channel.
  4. Represent per-device and per-pairing choices explicitly; both designs are modeled for IRK and CSRK. Keys and identifiers are “stored in corresponding tables (databases for storing data in ProVerif) after the key exchange so that they can be reused in other communication scenarios” (Section 4.2, p. 4503).
  5. Model the tracker as one module per identifier that checks whether a message is linked to that identifier, following the identifier’s specified usage; with passive/active and central/peripheral variants this gives 20 (5x2x2) modules (Section 4.3.2, p. 4504). The target emits an event on every send and receive; the tracker emits events when it sends a probe or receives a linked message. Passive untraceability is property P1 (target-send and tracker-receive of the same message both reachable); active untraceability is P2 (four events: tracker send, target receive, target send, tracker receive) (Section 4.3.3, p. 4505).
  6. To find all violations, after each violation “we disable the corresponding events of Alice and run the verification again until no violations are detected” (Section 4.3.3, p. 4505).
  7. Run one session first; if a property holds, run two sessions. The paper states, “We first verify these two properties in the one-session setting, i.e., each process runs once” (Section 5, p. 4505). A violation yields a ProVerif attack trace; the authors group traces in which the tracker follows the same procedure into one attack (Section 5.1, p. 4505).

The result is eight attacks from four root causes (Section 5.1, Table 2). IRK reuse lets a tracker that was once paired resolve the target’s RPAs after unpairing (Attacks 1–3); BD_ADDR reuse means a dual-stack target’s ID_ADDR is its Classic address, so the tracker can probe it with page requests (Attack 4); CSRK reuse lets the tracker verify signatures in authenticated messages or compare CSRKs in a new pairing (Attacks 5–7); ID_ADDR reuse lets the tracker recognize the target by the ID_ADDR it receives in a new pairing (Attack 8). The paper reports, “Our model, implemented using ProVerif, transforms the untraceability problem into a reachability problem” (Abstract, p. 4499).

Inference: In Verus, define an abstract protocol state as a ghost map of peers to identifiers and a transition relation for each scenario. Use spec fn predicates for linked and untraceable, and proof fn lemmas showing that a transition preserves non-linkability when keys are fresh. Verus can check the finite-state abstraction and trace invariants; it does not automatically model BLE radio behavior or cryptographic assumptions.

technique: use differential models to expose verifier blind spots

The paper also builds a Diff-Equivalence (DE) model of BLE with the per-device identifier design, using ProVerif’s choice[id,rand_id], and compares it with the reachability model (Section 5.2, pp. 4507–4508, Table 3). The DE model produces false attacks where the reachability model shows untraceability holds; the authors trace these to ProVerif proving DE only when both protocol instances take the same branch. In scenarios with known violations, “the DE-based model cannot find an attack trace” while “our reachability-based model can successfully find the correct attack trace” (Section 5.2, p. 4508). The authors say this “might be caused by other approximations in ProVerif”, for example a private channel implemented “in a way that ignores the order and number of sent messages” (Section 5.2, p. 4508). Inference: the practical lesson is to validate an automated encoding against a second property formulation and inspect both false positives and false negatives.

Inference: A Verus project can maintain two specifications—an event reachability invariant and a relational refinement between two executions—and test that both detect a deliberately injected identifier-reuse bug. This is a recommended adaptation, not a technique claimed by the paper.

technique: validate model findings on devices

After symbolic analysis, the authors test 13 BLE devices spanning mobile, desktop and embedded operating systems plus BTstack (Section 6, pp. 4508–4510). The method: one Linux laptop emulates a benign peer, another emulates the tracker; the device is paired with both, unpaired from the tracker, and the identifiers each laptop received are compared (Section 6.1, p. 4508). Table 4 records each issue per device; every tested device has at least two issues, and a device affected by one issue is vulnerable to all attacks exploiting it. The conclusion says, “We further evaluate 13 real-world BLE devices and found that all of them are affected by at least two of these issues” (Section 10, p. 4512). Google rated IRK reuse and BD_ADDR reuse high severity, assigned two CVEs (CVE-2021-39673 and CVE-2023-21307) and paid a $10,000 bug bounty (Section 6.3, p. 4510).

The paper’s mitigations (Section 7, pp. 4510–4511): specification updates to use per-pairing IRKs, a random-generated ID_ADDR for dual-stack devices, per-pairing CSRKs and per-pairing ID_ADDRs; developer suggestions to not use BD_ADDR in any BLE message, not derive the IRK from the identity root, and refresh the IRK after unpairing from the last paired device; end-user advice to turn off Bluetooth when not in use, reset Bluetooth after unpairing, unpair from and re-pair with all paired devices, or factory reset after unpairing.

Evidence is bounded by the model’s scope. The authors state that the model covers only the protocol level, that tracker capabilities are “weaker than the capabilities in the Dolev-Yao model”, that it “does not support the setting with three or more sessions”, and, “Finally, our model does not cover privacy issues caused by side channels, such as timing” (Section 8, pp. 4511–4512). Inference: device results are bounded by the 13-device sample. Inference: a product using agent-written verified Rust should treat freshness, key lifetime and reset semantics as explicit contracts; a proof that the Rust state machine preserves those contracts still depends on the BLE controller, OS stack and radio implementing the modeled transitions.

Inference: what is proved is the symbolic reachability result for the abstraction, and what is observed is the implementation behavior on the tested devices; what remains trusted is the interpretation of the Bluetooth specification, ProVerif’s soundness and abstractions, and hardware and OS behavior. Prior BLE privacy work studied fixed fields in advertising messages and fixed MAC addresses (Section 9, p. 4512). Inference: VL should reuse this identifier inventory and scenario decomposition rather than repeat those studies; the reusable contribution is systematic cross-scenario identifier tracking plus a model-to-device validation loop.

techniques for the catalog

  • reachability untraceability model: enumerate identifiers, roles and scenarios, then encode passive and active linking as ProVerif event reachability
  • differential verification check: compare reachability and Diff-Equivalence encodings to detect false attacks and missed attacks from modeling approximations
  • model-to-device validation: pair each device with a benign host and a tracker host, unpair the tracker, compare the identifiers both received, and map root identifier reuse to concrete mitigations Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Since Alice’s IRK obtained by the tracker is still valid after Alice unpairs from the tracker, the tracker can use this IRK to resolve the RPA in the message and identify Alice.”): what I checked: every quotation, page and section reference, technique step, number (13 devices, 8 attacks, 4 issues, 20 tracker modules, CVEs, bounty) and mitigation against the paper text; what I changed: link to the USENIX presentation page printed in the paper, moved the definition quote from the Abstract to Section 1 and split it around a footnote mark, fixed the identifier list (PK, LTK, IRK, CSRK, ID_ADDR), “pairing relationships” to tracker–target relations, wrong pages (one-session quote p. 4505 not 4507; Section 6 pp. 4508–4510; conclusion and side-channel quotes p. 4512 in Sections 10 and 8, not “Conclusion, p. 4516”), table storage to Section 4.2, added the disable-and-rerun step, hedged the DE false-negative cause as the authors did, replaced the mitigation list with the paper’s, replaced “replay attack traces” and “default configurations” (not in the paper) with the paper’s device test method, and marked own conclusions “Inference:”; what I did not check: the PDF layout beyond the text file, Table 7 row details, and the Verus adaptation ideas, which are not from the paper.

Last edited: