Formal Analysis and Patching of BLE-SC Pairing

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

scope and result

Shi et al. model Bluetooth Low Energy Secure Connections (BLE-SC) pairing in Tamarin Prover, covering every phase and all association models in Bluetooth 5.3. The paper’s abstract says, “In this paper, we develop the first comprehensive formal model of the BLE-SC pairing protocol.” The model finds method-confusion, key-negotiation-downgrade, and keysize-confusion attacks, then analyzes a backward-compatible patch with residual vulnerabilities in the input-input Passkey Entry case (§6.3, p. 47). The analysis is symbolic trace verification under an extended Dolev–Yao attacker (§3.2, p. 41). Inference: these proofs establish properties of the model, not of device code or cryptographic implementations.

technique 1: multiset-rewriting protocol model

What it is: Tamarin represents concurrent protocol executions as transitions over multisets of facts. The paper explains: “Tamarin Prover uses multiset rewriting rules to specify the concurrent execution of the protocol and the adversary as a transition system, where the state of the transition system is a multiset of facts and the initial state is an empty multiset” (§3.1, p. 40). Rules have a left-hand side of required facts, observable actions, and a right-hand side of produced facts. Linear facts are consumed once; persistent facts can be reused.

How to apply it: (1) model each device phase and message as facts; (2) use Fr for fresh values, Out for public sends, and In for attacker-constructed receives; (3) write one rule per protocol transition, requiring its pre-state facts and emitting its post-state facts; (4) let the adversary obtain every Out message and construct In messages from known terms. The paper’s encryption example generates fresh key and message, emits senc(m,k), then records attacker knowledge with a persistent fact (§3.1, Example 1, pp. 40–41).

Verus form: Inference: represent a protocol state as an enum or struct and define a pure transition relation over states and attacker actions. Use requires to constrain honest-device state and ensures to preserve phase and key invariants. A Tamarin multiset has no direct Verus equivalent; encode facts as a finite map or sequence with lemmas for linear consumption and persistent lookup. Keep cryptographic primitives abstract with spec fn axioms only when their assumptions are explicit.

Evidence and limits: The model includes all phases and association models, including user interactions and OOB. It assumes a secure OOB channel, honest devices, and a user with specified compare/input behavior (§3.2, p. 41). It abstracts key size to “low entropy” and “high entropy,” giving the attacker a brute-force oracle only for low entropy (§3.2, p. 41). Inference: those assumptions are trusted boundaries; a Verus proof of a Rust implementation would still need a specification for the Bluetooth radio and cryptographic library.

technique 2: parameterized model generation

A single model must cover 29 pairing situations arising from IO capabilities, OOB capabilities, and MITM requirements. Both honest devices advertise high-entropy maximum key sizes; low-entropy negotiation is an attacker action (§3.3.1, p. 43). Rather than hand-write all rules, the authors use the M4 macro processor. They state, “The scale of the general model is huge, which makes the modeling task time-consuming and error-prone” (§3.3.1, p. 41). A macro parameterizes initiator and responder capabilities, expands to rules for each branch, and generates 29 concrete models (§3.3.2, p. 43; Table 3).

How to apply it: (1) define a general transition schema with symbolic configuration parameters; (2) map each capability pair to its expected association model; (3) expand the schema into a concrete model; (4) check executability and security properties for every generated instance. The authors report that each specific model contains 112 rules (§3.3.2, p. 43).

Verus form: Inference: use Rust const generics or an enum configuration and prove a generic transition lemma, then instantiate it for every configuration. Configuration enumeration can check coverage, but execution tests alone do not prove trace properties.

Evidence and limits: The authors state, “These specific models cover all pairing situations in the specification” (§3.3.2, p. 43). Inference: this coverage claim is limited by their modeling assumptions; a counterexample is a symbolic trace and does not by itself demonstrate an exploit on deployed devices.

technique 3: trace properties and attack discovery

The authors express secrecy, authentication, MITM protection, and LTK-confusion protection as guarded first-order trace formulas. Their secrecy example says, “The definition of secrecy requires that there is no trace where an adversary could know the secret message m” (§3.1, Example 2, p. 41). Agreement lemmas relate a device’s commit event to a peer’s corresponding state and key. The tool automatically searches for a violating trace; the trace identifies which fields the attacker changes.

How to apply it: (1) mark protocol events with action facts; (2) define a property as a quantified relation between events; (3) run Tamarin over unbounded interleavings and attacker actions; (4) classify any counterexample by the modified field and association-model mismatch; (5) fix the protocol and rerun the same lemmas. This process discovers method confusion by changing IOCap fields, key-negotiation downgrade by changing KeySize, and keysize confusion by causing peers to derive keys of different lengths (§5, p. 45).

Verus form: Inference: record events in ghost state and express secrecy as exclusion of attacker-knowledge events, and authentication as a relation between commit and peer-running events. Proving these properties inductively would require an explicit transition relation and attacker model; this is a proposed adaptation, not a technique evaluated in the paper.

Evidence and limits: The full-scale study analyzes 29 models on Ubuntu 18.04 (§5, p. 45). All non-JW situations violate LTK-confusion protection, all situations violate secrecy of authenticated LTK, and seven pairing situations exhibit method confusion (§5, p. 45; Table 4, p. 46). These results concern the 29 generated models. The model retains the perfect-cryptography abstraction for high-entropy keys, assumes honest devices, and excludes an untrusted environment for passkey entry (§3.2, p. 41).

technique 4: patch then reverify

The patch authenticates values that were previously attacker-modifiable. In patched Numeric Comparison (NC), the devices first complete standard NC with user confirmation. They then display HI = g3(VI || req || rsp) and HR = g3(VR || req || rsp) for a second user comparison and confirmation. Here req and rsp are the pairing request and response, || denotes concatenation, and g3 outputs a six-digit number (§6.2.1, p. 47). In patched Passkey Entry (PE), the display-input case first completes standard PE. The display device then shows DR = g3(passkey || req || rsp); the input device computes the same expression as H, asks the user to enter DR, and checks equality. The input-input case performs standard PE without this additional check (§6.2.2, p. 47). The authors then model the patch with the same assumptions and rerun Tamarin: “We formally model our patched BLE-SC pairing protocol and verify the model using Tamarin Prover” (§6.3, p. 47).

How to apply it: (1) identify the message field enabling the attack; (2) include the pairing request and response in the additional six-digit computation; (3) add the comparison or input check; (4) analyze compatibility with unpatched devices (§6.4, pp. 48–49); (5) rerun executability and security lemmas for the patched NC and PE configurations. Table 6 verifies MITM protection, LTK-confusion protection, and authenticated-LTK secrecy for patched NC and display-input PE, but KeyboardOnly–KeyboardOnly still violates LTK-confusion protection and authenticated-LTK secrecy (§6.3, p. 47; Table 6, p. 48). Some authentication lemmas still fail, which the authors attribute to one-side pairing (§6.3, p. 47). Compatibility with an unpatched device preserves connectivity with the security of the standard association model (§6.4, pp. 48–49).

Verus form: Inference: model the added computation and confirmation as explicit transitions, then attempt to prove the corresponding trace properties. A six-digit output cannot uniquely identify every possible transcript; any proof using equality of displayed values must state how it treats collisions. The paper specifies g3 only as a function that outputs a six-digit number (§6.2.1, p. 47).

what is proved, measured, and trusted

Reported: verified and falsified symbolic trace properties for the original and patched models (Tables 4 and 6, pp. 46 and 48), with 29 original BLE-SC configurations and 112 rules per specific model (§3.3.2, p. 43). Assumptions: secure OOB, honest devices supporting high-entropy maximum key sizes, specified user behavior, and a low-entropy key oracle (§3.2, p. 41). Inference: a Rust verification effort could reuse this configuration coverage and event-property structure, but would need to justify the mapping from implementation behavior to the symbolic model.

Inference: VL could reuse the paper’s all-association-model decomposition, attacker oracle for low entropy, event-property style, 29-instance coverage plan, and patch/reverification workflow as specification patterns, while retaining the unresolved KeyboardOnly–KeyboardOnly cases as residual vulnerabilities.

techniques for the catalog

• multiset-rewriting model: encode concurrent protocol and attacker steps as linear and persistent facts
• parameterized expansion: generate every configuration from one protocol schema
• trace-property checking: state secrecy and agreement as quantified event formulas and inspect counterexample traces
• patch-and-reverify: bind mutable fields to the transcript, then rerun all properties Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “The security mechanism in the BLE-SC pairing protocol cannot detect the disparity of the key sizes.”): checked all paper text, study quotations, numbers, section and printed-page references, model assumptions, attack descriptions, and patch steps; corrected quotations, page references, configuration parameters, patch scope, and unsupported Verus claims, and replaced the link with the publisher page printed in the paper; did not run Tamarin, inspect the model repository, validate Bluetooth implementations, or verify the proposed Verus adaptations.

Last edited: 2026-10-16