Wireless communications integrated in connected devices can expose their users to tracking via the exposure of link layer identifiers (e.g. MAC addresses). To counter this threat, it has been proposed to replace those permanent identifiers with periodically changing random pseudonyms [17]. This practice, called address randomization has been progressively adopted by vendors [28, 36] and has even made its way to wireless standards [1, 35]. However, an effective implementation of address randomization requires more than periodically rotating the link layer identifier. Indeed, several works [8, 11, 12, 16, 27, 28, 36] identified issues with address randomization implementation, where in-frames counters and identifiers can undermine the anti-tracking measure.

In this paper, we address the problem of verifying the correctness of an address randomization implementation. To this end, we introduce an approach to identify issues based on a capture of the traffic generated by a device. This approach relies on rules specifying requirements for a correct implementation of address randomization. Then, we prototype Valkyrie (Verification of Addresses LinKabilitY in address Randomization ImplemEntations), a software tool that, based on a set of rules, verifies that a given sequence of frames generated by a device does not compromise the address randomization scheme. Finally, we evaluate this tool on a corpus of frame captures corresponding to 60 devices implementing address randomization for Wi-Fi and Bluetooth Low Energy (BLE).