Conditional Min-Entropy Loss and Transcript Binding in Bluetooth Low Energy Pairing

Bluetooth Low Energy (BLE) Secure Connections pairing begins with an unauthenticated exchange of Security Manager Protocol features that influence the subsequent association procedure and security policy, while the complete ordered feature-exchange transcript is not included as a unified context in the standard Passkey Entry confirmation computation. This missing cross-phase binding allows an active adversary to present different negotiation contexts to two honest endpoints. We analyse this problem through four distinct evidential layers: information-theoretic uncertainty loss, symbolic reachability, a conditional computational argument for transcript binding, and a prototype experiment on a controlled testbed. First, conditional min-entropy is used to quantify the security loss caused by accepting an effective key length ℓ<L: under a uniform-key and no-additional-leakage model, the loss is L−ℓ bits and the optimal one-shot guessing probability increases by 2L−ℓ. Second, a Tamarin-style symbolic abstraction represents transcript tampering, user-interface confusion, and the symbolic recovery of keys classified as low entropy under the stated rewriting rules. Third, we propose a context-bound Passkey Entry confirmation variant in which both endpoints include the canonical Pairing Request/Pairing Response transcript in the Passkey Entry confirmation computation. The variant adds no radio message or user interaction, but requires bilateral deployment. In the controlled HCI-injection evaluation, the two selected fault conditions were exercised for 1000 runs each. The prototype recorded 981/1000 and 978/1000 protocol-level blocks, corresponding to 98.1% and 97.8%. Operational timeouts were recorded separately. The setup was not a transparent over-the-air man-in-the-middle between two independent commercial endpoints. Because original per-run packet captures and HCI traces were not retained, the aggregate blocking outcomes cannot be independently verified at packet level. The BLE transcript requires 14 octets of additional cached protocol-payload state, while complete memory, latency, and energy overheads remain implementation-dependent. Transcript binding therefore preserves negotiation consistency but neither creates key entropy nor prevents endpoints from jointly selecting a weak policy.