Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation Mohit Kumar Jangid

Indian Institute of Technology Jodhpur Jodhpur, Rajasthan, India mjangid@iitj.ac.in

Felix Engelmann

Ohio State University Columbus, Ohio, USA fe-research@nlogn.org

arXiv:2608.11337v1 [cs.CR] 11 Aug 2026

Abstract With the surge in privacy-sensitive data from sources such as social media and IoT devices, there is a pressing need for formal, automated methods to assess privacy risks within these intricate systems. This paper formally investigates root sources of pairing-based privacy threats exploited using replay/relay techniques in wireless communication. Our research harnesses condition-oblivious responses, replay-resistance, and distance bounding measures vital for protocols utilizing shared keys in allowlists for authenticated reconnections. Particularly, the paper uses formal modeling of notable wireless networks, like the Wi-Fi P2P persistent group formation and the Bluetooth Low Energy reconnection procedure, to illustrate the root causes and countermeasures. Our model rigorously validates the proposed solution against association inference attacks, along with existing formalizations of well-authentication, frame opacity, and no-desynchronization. The ensuing analysis reveals not only uncharted privacy realms in wireless communication but also identifies old and new vulnerabilities. Our proposed design changes are acknowledged by Wi-Fi Alliance and Bluetooth SIG, paving the way for future advancements in resilient, privacy-preserving wireless protocols.

Keywords User privacy, exclusive-use, network protocols, IoT, deanonymization, user profiling, tracking, formalization, privacy risks

1

Introduction

In the digital era, individuals and organizations rely heavily on technologies for instantaneous data exchange. Notably, businesses amass and analyze vast volumes of user data, leveraging its insights to refine their services and maintain a competitive edge in the market [44]. However, this continuous flow of information underscores the paramount importance of privacy, particularly in sectors such as the Internet of Things (IoT), healthcare [33, 62], and intelligence/government agencies. Furthermore, breaches of privacy for public figures can have a profound impact on their reputation and professional life [61]. Given these stakes, ensuring privacy has become an urgent imperative, necessitating robust mechanisms to guarantee the safety and security of sensitive information. As privacy is recognized as granting consent and control over various aspects of one’s life, including communication, intellectual pursuits, physical presence, and well-being, the privacy property unlinkability has been studied extensively in the domain of digital communication [10, 14, 48, 53, 58, 63]. Unlinkability is achieved when an external observer monitoring multiple users’ actions (such as communication via their devices) cannot correlate two distinct

Zhiqiang Lin

Ohio State University Columbus, Ohio, USA zlin@cse.ohio-state.edu

communications to a single user. If an adversary succeeds to link both, they could deduce intimate details about an individual’s interests, location, and health status, among other things, compromising the user’s anonymity. Notably, unlinkability has been studied in a range of protocols: e-voting [17, 29], TLS [21], backhaul network [19], 5G [10, 19], e-passports [1, 10, 38], Wi-Fi [24, 37], etc. In the domain of wireless communication, especially IoT applications, various unlinkability threats have emerged in the past. These smart devices employ a peculiar feature known as Preferred Network List (PNL) to connect frequently connecting devices efficiently. Trading off usability for security, this feature has been exploited to de-anonymize large crowds based on preferred Wi-Fi SSIDs list [24, 31, 37]. Advancing the impact further, the Bluetooth MAC Address Tracking Attack (BAT Attack) [65] deanonymizes users at an individual level. In this attack, the attacker leverages allowlists (the PNL for Bluetooth devices) and replay/relay techniques to track Bluetooth user locations. These threats reveal that wireless protocols may harbor subtle vulnerabilities leading to privacy breaches. The nature of these privacy threats is further complicated by the fact that different contexts of communication mediums, authentication mechanisms, and data share architectures impact unlinkability differently. Given these challenges, we notice a lack of foundational root causes of PNL-based attacks. Therefore, we undertake a formal investigation of privacy attacks exposing the association of users. In doing so, we ask the following questions: How can we systematically investigate the fundamental causes of these breaches? What countermeasures are effective at neutralizing these threats, both theoretically and in practice? To address these questions, this paper conducts a comprehensive, formal investigation of the mechanisms underlying allowlistbased attacks. To tackle the challenges of formal modeling and reasoning about unlinkability, we expand existing formal building blocks: Hirschi et al. [48] and Baelde et al. [10] use a combination of trace properties and diff-equivalence to reason about unlinkability based on three sufficient conditions (§2): Well-Authentication (WA), Frame Opacity (FO), and No-Desynchronisation (ND). We instrument privacy using the state-of-the-art symbolic verification tool Tamarin [56], preferring it over DeepSec [26], APTE [25] or AKISS [22] because Tamarin can reason about unbounded processes, sessions and messages providing stronger and generic guarantees. In this research, we find that the presence of allowlists in wireless protocols and conditional checks over this data are the root causes enabling an adversary to deduce user association in privacysensitive groups. For example, BAT attacks capitalize on locally shared data such as allowlists, commonly set up among IoT devices

Jangid et al.

within organizational or personal frameworks for swift reconnections [65]. This means that an adversary with the ability to relay or replay packets between a distant device associated with a targeted user’s privacy-sensitive group, whether it be a household or paired phone, can disclose the user’s association and even pinpoint their location. It is worth noting that in wireless communications, relay or replay can be easily and cost-effectively achieved due to the ubiquity of smartphones and programmable software-defined radios, as opposed to wired communications, as shown in various digital contact tracing works [8, 20, 40]. Modeling allowlists in a process calculus reveals attacks that were not captured in previous work. By using Tamarin [56], we formally model Bluetooth reconnection procedures and Wi-Fi P2P persistent group formation. Through detailed analysis, we highlight design flaws in the protocols leading to Association Inference (AInf ) and propose corrective countermeasures. We employ a combination of condition oblivious responses, replay-resistant techniques, and distance bounding checks to propose design changes mitigating AInf attacks. Our Tamarin models confirm the WA, FO, and ND privacy properties, in addition to the Replay-Resistant (RR) measures and Distance Bounding (DiB)[27]). Additionally, to demonstrate the preliminary performance overhead of our proposed design, we develop C++ protocol codes for Wi-Fi and Bluetooth reconnection procedures. The evaluation indicates that the proposed protocol design achieves reconnection within 80-125 milliseconds as long as distance bounding checks can be optimized within reasonable bounds. Encouragingly, both Wi-Fi Alliance and Bluetooth SIG have acknowledged our findings and agreed with our proposed solutions. Furthermore, both interest groups plan to publish our reports to stakeholders. We make the following contributions: Novel Privacy Characterization (§4). We systematically characterize AInf privacy attack, expanding our understanding beyond existing privacy formulations. Revised Protocols Design(§4). Our recommendations for protocol design modifications specifically target the prevention of AInf, concurred by both Bluetooth SIG and Wi-Fi Alliance. Our proposed design strategically combines distance bounding checks and condition oblivious responses to deterministically detect relay and replays while keeping the faster reconnection feature intact. Formally and Practically Validated Case Studies (§8). By formally verifying the proposed protocols for two prevalent real-world wireless protocols—Bluetooth and Wi-Fi P2P—we have demonstrated the generality and robustness of our privacy formalization approach. Additionally, we developed a C++ protocol code providing preliminary performance overhead of the proposed techniques.

2

Background & Related Works

Bluetooth Pairing. Bluetooth is a short-range wireless technology that transitioned from simple device pairing to facilitating mesh networks for streamlined IoT operations. During the initial connection, devices pair using a comprehensive authentication procedure [60], which consists of two distinct authentication phases and human interaction, resulting in the sharing of a Long-Term Key (LTK), such as the Identity Resolution Key (IRK). Thereafter, the reconnection process begins by discovering devices using advertisements of Random Private Addresses (RPA) [65]. These addresses are composed

of randomized hashed values of IRK shared at the end of the firsttime pairing protocol. A receiving device then searches its local storage for registered IRKs to identify the sender. Upon mutual RPA recognition, an ephemeral session key is derived for subsequent encrypted data exchanges [11]. Wi-Fi P2P or Wi-Fi Direct [64]. WiFi P2P/Direct facilitates peerto-peer communication, enhancing IoT device interaction by bypassing Access Points (AP). This direct approach saves energy and boosts network adaptability and robustness. In this setup, devices dynamically assume access point or client roles and utilize the Wi-Fi Protected Setup (WPS) [4] for security. It supports group formations for various applications, such as home automation and vehicle-to-vehicle communication. The Wi-Fi P2P specification categorizes devices as either Supplicants: requesting authentication, or Authenticators: granting access. Group connections can be initiated internally or externally and form in three ways: standard, autonomous, and persistent. While standard and autonomous connections dynamically designate device roles and fully authenticate new members, persistent groups utilize stored network IDs and associated Pre-Shared Keys (PSK) for faster reconnections. BAT Attack [65]. BAT attack exploits Bluetooth’s MAC addresses to track users. Even with MAC address randomization, BLE devices periodically broadcast their MAC address advertisements, allowing attackers to correlate devices. The vulnerability becomes more pronouncd when BLE devices enable the allowlist, responding only to a authorized preferred devices. Attackers can track these devices by analyzing MAC addresses and responses. An active form of this attack can be carried out by replaying a sniffed MAC address, probing whether a peripheral or central device responds. This exploitation is facilitated by a flaw in the current MAC address randomization algorithm of the Bluetooth specification, which does not specify a method for random number selection and lacks safeguards against the reuse of randomness. As a result, attackers can track devices across the randomization time interval by replaying MAC addresses and assessing whether they are in the allowlist. The BAT attack, therefore, leverages both replay and relay attack vectors to exploit user privacy and track locations, with the relay attack being independent of the replay attack. Related Works. Previous research has explored the use of humanreadable SSIDs in Wi-Fi and Bluetooth for deanonymizing locations and interests of individuals [65] and groups [24, 31, 37]. Unlike these studies, our work goes beyond the advertisement/probe phase and comprehensively characterizes the allowlist privacy attack. Prior formal research on privacy [10, 48] focuses on defining building block privacy properties with case studies on RFID and 5G networks. In contrast, our work leverages these building block properties and expands the attack scope to cover relay attacks over uncovered case studies for Wi-Fi and Bluetooth with mitigations. The closest work to ours is IDBleed [41], which adopts a measurement approach to explain the widespread occurrence of exclusiveuse attacks without formalization. It offers a defense using channel broadcasting and requiring synchronization. Instead, our focus lies on a formal approach to precisely specify Bluetooth and Wi-Fi protocol sections vulnerable to WA, ND, and FO privacy properties. Moreover, our defense does not require synchronization, and we propose a concrete protocol design that defends against both replay and relay attacks.

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation

Prover P

Verifier V

𝑘

𝑘 𝑛𝑉 ←$ N

𝑛𝑃 ←$ N 𝑛𝑃 , 𝑛𝑉 𝑃0 ||𝑃1 ← PRF(𝑛𝑉 , 𝑛𝑃 , 𝑘)

𝑉0 ||𝑉1 ← PRF(𝑛𝑉 , 𝑛𝑃 , 𝑘)

loop 𝑖 ∈ 1 . . . 𝑁 𝑐𝑖 𝑃𝑐𝑖 𝑖 (𝑖 th bit)

𝑐𝑖 ←$ {0, 1} Δ𝑡 𝑃𝑐𝑖 𝑖 = 𝑉𝑐𝑖𝑖 ∧ Δ𝑡 < 𝑡 thr

Figure 1: Distance bounding by Hancke and Kuhn [46].

Distance Bounding Protocol [16]. Distance Bounding Protocol was first introduced by Brands and Chaum in 1994 to protect against relay attacks that can compromise a wide range of systems, including touchless payment card transactions, wireless automobile keys, and RFID access controls [7, 9, 13, 27]. Relay attacks occur when an adversary acts as a man-in-the-middle, relaying authenticated connection packets from the source to the target device. Since relaying bypasses cryptographic protections, detecting the proximity of peer devices through distance bounding is critical. Distance Bounding Protocols establish the average response time and ensure it remains within an application-specific threshold through a series of timed challenge-responses. The verifying device uses the speed of the electromagnetic wave (speed of light), as well as the response time from the peer device, to calculate proximity. Given that this is a timesensitive calculation, multiple challenge responses are exchanged to verify that the average response time falls within the threshold limit based on various application cases. One of the canonical Distance Bounding Protocols, based on a shared symmetric key, was proposed by Hancke and Kuhn [46] (see Figure 1). The protocol begins with a session setup phase where the verifier and prover, which share a secret key 𝑘, exchange nonces 𝑛𝑉 and 𝑛𝑃 from a nonce space N . The subsequent phase is the rapid exchange of bits for 𝑁 rounds which are timed by the verifier. The responses consist of the bits generated by a pseudo-random function outputting 2𝑁 bits using the nonces and the shared key to authenticate the prover. Let 𝑐 be the speed of light, 𝑡 max the time to process and release the response for a given challenge at the prover, and 𝑑 max the maximum approved distance between the prover and verifier for a specific application. The calculated round-trip response time at the verifier must be less than the approved threshold time: 𝑡 thr = 2 ∗ 𝑑max 𝑐 +𝑡𝑚𝑎𝑥 . If all the responses are received within the threshold time and match with the local PRF calculation, the verifier approves the close proximity of the prover.

3

aims to violate. The owner of the target device will be referred to as the target user. To break unlinkability, the adversary attempts to link the user of an arbitrary device, referred to as a prospective device, to a user of the target devices. This set of target devices will be referred to as the target devices. The owner of a prospective device will be referred to as prospective user. An adversary will test numerous prospective devices to find one that connects to the target device, thereby identifying the target user. Motivating Example. We demonstrate two wireless protocol case scenarios with identical protocol designs, yet having different privacy impacts. Consider a database of passports that is queried at international airports. This database contains passport details of all countries (worldwide scope). On the other hand, consider two household Bluetooth devices: a cellphone and a speaker. Given their frequent connection, the cell phone has an allowlist (PNL) containing an entry for the speaker to facilitate faster reconnection. Unlike the worldwide scope of passport details, the scope of the Bluetooth allowlist database is limited to a household. Both cases employ the Basic Hash protocol [18]. In this protocol, the shared secret 𝑘 is hashed using a cryptographic hash function h with a nonce 𝑛 as the tuple ⟨𝑛, h(𝑛, 𝑘)⟩. In, Bluetooth’s case the secret is sender device’s IRK, while the E-Passport reader uses pre-shared secrets over RFID communication. In the attack, the adversary collects the message at time 𝑡 1 and attempts to replay it at time 𝑡 2 > 𝑡 1 , either to the EPassport reader at the airport or to an prospective user’s cellphone in various locations. At time 𝑡 2 , a response of OK or ERROR from the passport reader only discloses that the target user information is present in a worldwide database. In contrast, for paired devices, an OK response provides more specific and sensitive information: the prospective user is part of the target user’s household, violating location privacy by confirming the presence of the target user at the prospective device location. Problem Statement. Considering the above observation, this paper seeks to answer the following research questions (RQ): RQ1. What causes PNL privacy attacks to work differently in differnt contexts? RQ2. How can these attacks be prevented formally and in practice? Overview. To address RQ1, we observe that the various allowlist network expose privacy-sensitive data differently. In §4, we systematically describe the allowlist network, protocol checks, and adversary knowledge required for the PNL attack in terms of six necessary conditions. These conditions reveal unexplored privacy violations in protocols that use allowlists for peer agreements and authentication. To answer RQ2, we perform a formal security assessment of Bluetooth and Wi-Fi P2P (§8), leading to the identification of numerous old and new attacks. Utilizing sufficient conditions from prior research and employing condition oblivious responses in conjunction with RR and DiB)properties, we counter relay/replay attacks to prevent user location tracking (§6).

Motivation and Problem Statement

User/Device Roles in Unlinkability. Throughout the paper, we will be using some of the key terms to describe our research work. In this paper, the attacker’s objective is to link two seemingly unrelated actions of the same user. The following are the user/device roles: A target device belongs to the user whose privacy the adversary

4

Characterizing Association Inference Attack

In this section, we characterize the attack into its building blocks. We discuss the shared data network, scope sensitivity, peristence and the protocol structure that enable the PNL attack. We also clarify the attacker resources and context accessible to the adversary.

Jangid et al.

1 1

4

2

A

B

3 B

C

C

D

2 B

(a) local

D 4

E 5

3 1 2

5 (b) company

5

F

E 3

4

(c) global

Figure 2: Different data share network. Nodes represent devices; edges indicate shared key data according to their letter.

4.1

Infrastructure Requirements

In Figure 2 the sub-figures (a), (b), and (c) show an example of different shared data network among five devices {1...5}. In case (a), the devices {1, 2} and {3, 4, 5} form separate connected components (local groups) and they share data 𝐴 and 𝐵, respectively. Examples of data in this network are allowlist in Bluetooth pairing and group-network- configuration in Wi-Fi P2P persistent group formation protocol. Here, the devices {3, 4, 5} could be IoT devices of a house, with group network configuration files as data 𝐵 for fast reconnection. In case (b) A few devices {2, 4} contain data for all the other devices {1, 3, 5}. Devices {2, 4} could be considered as global server hosting details for clients {1, 3, 5}. For example, {2, 4} could be DNS servers holding host domains to IP mappings data 𝐶, 𝐷, and 𝐹 for devices {1, 3, 5}, respectively. Another example could be global passport records servers {1, 2, 3} holding bio information for users holding passports {1, 3, 5}. In case (c) a global data is shared among all devices. For example, data 𝐹 as root digital certificates of global certificate authorities for transport layer security protocol authentication shared among all Internet-connected devices {1...5}. Our first observervation is that the network shown in Figure 2(a) is vulnerable to PNL attacks while the other aren’t. Assume a connected component in the network as the target group. In this case, if a PNL is shared within the target group, it allows the adversary to distinctly compare the communication pattern of a prospective device with the target group. More details will be explained in §4.4. Second, the scope of the shared data must be privacy sensitive. In Figure 2(a), the target group could belong to various sizes of scope: a house, a university, small businesses such as restaurants and coffee shops, a city, countries, large corporate offices such as Google and Facebook, etc. The local scope is considered privacy sensitive if the information about the association of an individual to the group can be reduced to a target user. The group of IoT devices in a house or in an office can be owned by an individual user, whereas a device group in a university cannot be necessarily owned by an individual. In this case, the former group is considered privacy-sensitive, and the latter is not. Third the shared data should not change across multiple sessions. A persistently shared data across multiple sessions is usually desired to authenticate the devices on a reconnection or to establish new secrets if needed. Lastly, the protocol for communication among the target group should emit responses dependent on the shared data. An example of such responses could be result of message integrity check (MIC) verification with a preshared key. Other example could be

decryption and confirmation of a nonce sent recently in a protocol with using preshared key. The immediate response from the protocol agent executing the condition or any later responses at the agent can serve as the point for PNL attack. We will refer to such a condition as privacy-critical condition in the rest of the paper.

4.2

Attacker’s Resources

Replay and Relay. The adversary requires knowledge of one or more static locations for the target device. For a replay attack, this location enables the adversary to collect messages for future replay. For a relay attack, the adversary utilizes the static location of the target device to establish a relay connection with an arbitrary prospective device located at any location. For instance, numerous users may be targeted by locating their houses or offices, as most IoT devices within a house are paired. Observable Context. In terms of the context available to the adversary, note that the communication behavior between devices in the target devices deviates from that among unrelated devices. Specifically, responses at the privacy-critical conditions should be distinguishable when reconnecting to a target device versus an unrealed one. The differences may include response size, response time, message counts, encoding formats, or state transitions.

4.3

Threat Model and Scope

Threat Model. We adopt the standard Dolev-Yao adversary model [39] where the adversary can observe, modify, block, and replay communication messages. The adversary is capable of relaying wireless packets by deploying multiple relay devices between two remote user devices. Additionally, the adversary can initiate a connection without involving device owner interaction. We exclude the leakage of protocol secrets (e.g., preshared keys) or any compromise of the user devices in our model. In terms of timing side channels to breach privacy, we do not consider the adversary’s ability to assess time differences to deduce unlinkability. In the context of distance bounding protocols, various attacks have been classified based on compromised prover, compromised verifier, and secret key leakage. These include Mafia Fraud [35], Lone Distance Fraud [30, 35], Distance Hijacking [30], Terrorist Fraud [35], and Assisted Distance Fraud [30]. Since we do not consider compromised devices or secret key leakage, none of these attacks are relevant to our paper. Our case study uses the Bluetooth Specification V5.2 [60], Wi-Fi Protected Setup V2.0.8 [4], and Wi-Fi P2P Specification V1.9 [64]. Practicality of Threat Model. Many wireless devices have designed reconnection procedures for frequently connecting devices, often based on pre-shared keys, which facilitate automatic and quickconnections. Relay attacks have been part of security research for the past 20 years, resulting in numerous practical attacks such as car theft featuring “keyless” entry [2, 43] and remote pickpocketing through user’s contactless payment cards [28] , as well as mafia fraud attacks over RFID [47]. The relay capability is a standard threat model in various prior research on distance bounding protocols [30, 34–36, 55, 59] and wireless relay/replay based attacks [49, 51, 57, 65]. Practicality of Secure Proximity Precision. Verifying physical proximity is critical in domains such as industrial RFID/NFC manufacturing

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation

and asset tracking, wireless payments, and autonomous vehicles. This necessity has prompted active research in this area, with distance bounding check implementations facing challenges such as precise time measurements and noise considerations. However, the need to prevent relay attacks has become vital in the era of wireless communication [7, 13]. This is reflected in the availability of recent products such as the ATA5350 UWB (Ultra-Wideband) Transceiver [3], the NXP Mifare Plus EV2 Secure IC [5], and the EMV contactless payment standard [42] that implement distance bounding to counter relay attacks. Similarly, although Bluetooth devices operate under low power, the need for distance bounding measurements has driven the development of the NXP KW36 Bluetooth Low Energy radio platform, which features distance bounding checks. The corresponding white paper [50] demonstrates the feasibility and practicality of implementing distance bounding.

4.4

Attack Procedure and Impact

When the aforementioned infrastructure §4.1 and attacker’s resources §4.2 are present within the defined threat model, an adversary can exploit AInf to compromise a target user’s unlinkability. An attacker can launch the AInf attack as follows: First, the attacker identifies a static location for a target user who owns target devices satifying infrastructure requirements §4.1. Upon encountering a prospective device, the adversary is interested in determining whether the prospective device belongs to the target user. For the replay attack, the adversary records the wireless communication within the target devices and later uses it to replay the messages to the prospective device. In a relay attack, the adversary establishes a relay connection between the target device and the prospective device. Based on the positive/negative conditional outcome, the adversary infers whether the prospective device is paired with a target device. If so, the target user is present at the location of the prospective device. Note that if a protocol contains multiple privacy-critical conditions exposing distinguishing behaviors, the adversary can use any of these conditions independently to carry out our AInf attack. For example, if for any privacy-critical condition, the connection proceeds as a reconnection procedure among target devices, it indicates that the prospective device is carried by the target user. On the other hand, for any progression of the connection that does not follow this pattern, the prospective device does not belong to the target user, and the adversary continues hunting for other prospective devices, repeating the same attack procedure. The association of a prospective device with another target one allows the adversary to link the location and service interest of the target user, thereby undermining their unlinkability. For example, frequent visits to special medical facilities could reveal the physical conditions of the target user. For cases when the group of devices belongs a common theme ( such as a university, recreational club, religious organization, or specialized medical facility), an association inference of a prospective user to such a group can reveal information about their relationships, interests, or physical conditions. However, this setting does not enable the tracking of an individual user’s location. Instead, the privacy exposure for each individual user is 1/𝑁 , where 𝑁 represents the number of target device owners. Therefore, as 𝑁 increases, the overall privacy impact will be reduced.

Tag

Reader A

Reader B

𝑘

𝑘

∅

𝑛𝑇 ⟨𝑛𝑇 , h(𝑛𝑇 , 𝑘)⟩ ok ⟨𝑛𝑇 , h(𝑛𝑇 , 𝑘)⟩ err

Figure 3: Example of attack with multiple readers

Table 1: Syntax of processes, 𝑟 ∈ {A, B} 𝑃, 𝑄 := 0 |new 𝑛.𝑃 |in(𝑐, 𝑥).𝑃 |out(𝑐, 𝑢).𝑃 |insert𝑟 (𝑣) |lookup𝑟 𝑘 such that 𝑥¯ = 𝑡¯ in 𝑃else 𝑄 |(𝑃 |𝑄) |!𝑃 |𝑃; 𝑄 |¡𝑃

5

null process name restriction input output insert to database 𝑟 pairing test

𝑛∈N 𝑐 ∈ C, 𝑥 ∈ X 𝑐 ∈ C, 𝑢 ∈ T (Σ𝑐 , N ∪ X) 𝑣 ∈ T (Σ𝑐 , N ∪ X) 𝑘∈N 𝑥¯ ∈ X𝑙 𝑡¯ ∈ T (Σ, N ∪ X)𝑙

parallel composition replication sequence repetition

Formalization

In this section, we extend existing formalizations to capture our allowlist-based linkability attack. We employ a similar process algebra as in [10] to describe the possible protocol operations. To emphasize the differences introduced by the use of allowlists, we present a minimal extension of their Simple Hash protocol. Instead of a single global reader, we split the reader into two, each with its own database to illustrate the issue arising with allowlists. In this example, a tag has a key 𝑘 and uses it to authenticate to a reader by sampling a nonce 𝑛𝑇 and sending the tuple ⟨𝑛𝑇 , h(𝑛𝑇 , 𝑘)⟩ to the reader. If the reader has 𝑘 in its allowlist, and the hash matches, it replies ok, otherwise err. To demonstrate the effect of allowlists, we model two separate readers with their own databases acting as allowlists, i.e. sets of keys as shown in Figure 3. In this minimal example, we simplify the complexity of a system like Bluetooth pairing by only authenticating the tag and omitting the reverse authentication. Instead of multiple pairings between devices, there are only two groups of readers in this model.

5.1

Syntax

We model these processes using process algebra with the following syntax. Let N be a set of names, X variables and C channels. With these, T (Σ, 𝑉 ) creates terms using functions from the signature Σ and data 𝑉 . The full syntax is presented in Table 1. The main change is the parameter 𝑟 to insert and lookup which specifies the reader to act on. The reader identities A, B are public constants.

Jangid et al.

Table 2: Semantics for processes IN

(in(𝑐, 𝑥).𝑃 ∪ P; 𝜙; 𝐴)

OUT

−−−−−→ (𝑃 {𝑥 ↦→ 𝑢} ∪ P; 𝜙; 𝐴) (𝑅 a recipe for the computable message 𝑢) (out(𝑐, 𝑢).𝑃 ∪ P; 𝜙; 𝐴)

Tag

Reader A

Reader B

𝑘

𝑘

𝑘

𝑛𝑇

in(𝑐,𝑅)

⟨𝑛𝑇 , h(𝑛𝑇 , 𝑘)⟩ ok ⟨𝑛𝑇 , h(𝑛𝑇 , 𝑘)⟩ ok

out(𝑐,𝑤 )

NEW-N INSERT ALLOWED

𝜏then

-THEN ALLOWED

−−−−→ (𝑃 {𝑘 ↦→ 𝑘 ′𝑥¯ ↦→ 𝑤¯ } ∪ P; 𝜙; 𝐴) when 𝑘 ′ ∈ 𝐴𝑟 exists such that 𝑤¯ = 𝑡¯{𝑘 ↦→ 𝑘 ′ } ⇓ (lookup𝑟 𝑘 such that 𝑥¯ = 𝑡¯in𝑃else 𝑄 ∪ P; 𝜙; 𝐴) 𝜏else

-ELSE PARALLEL REPLICATE REPEAT SEQ ABORT

5.2

−−−−−−→ (𝑃 ∪ P; 𝜙 ∪ {𝑤 ↦→ 𝑢}; 𝐴) 𝜏 (new 𝑛.𝑃 ∪ P; 𝜙; 𝐴) → − (𝑃 ∪ P; 𝜙; 𝐴) (insert𝑟 (𝑣) ∪ P; 𝜙; (𝐴𝑟 , ·)) 𝜏 → − (𝑃 ∪ P; 𝜙; (𝐴𝑟 ∪ {𝑣 }, ·)) (lookup𝑟 𝑘 such that 𝑥¯ = 𝑡¯in𝑃else 𝑄 ∪ P; 𝜙; 𝐴)

−−−−→ (𝑄 ∪ P; 𝜙; 𝐴) when ∀𝑘 ′ ∈ 𝐴𝑟 , it holds that 𝑡¯{𝑘 ↦→ 𝑘 ′ } ̸⇓ 𝜏 ({𝑃 1 |𝑃 2 } ∪ P; 𝜙; 𝐴) → − ({𝑃 1, 𝑃2 } ∪ P; 𝜙; 𝐴) 𝜏 (!𝑃 ∪ P; 𝜙; 𝐴) → − (𝑃∪!𝑃 ∪ P; 𝜙; 𝐴) 𝜏 (¡𝑃 ∪ P; 𝜙; 𝐴) → − ({𝑃; ¡𝑃 } ∪ P; 𝜙; 𝐴) 𝛼 (𝑃 ∪ P; 𝜙; 𝐴) − → (𝑃 ′ ∪ P; 𝜙 ′ ; 𝐴′ ) for any sequence simplification rule 𝜏abort

((𝑃; 𝑄) ∪ P; 𝜙; 𝐴) −−−−→ (𝑄 ∪ P; 𝜙; 𝐴)

Semantics

To maintain a record of allowlists and the adversary’s knowledge, we define our system configurations 𝐾 as follows: (P; 𝜙; (𝐴𝐴 , 𝐴𝐵 )) where P represents the multiset of processes without any null processes. 𝜙 = {𝑤 1 ↦→ 𝑢 1, . . . , 𝑤𝑛 ↦→ 𝑢𝑛 } is a substitution of handles 𝑤𝑖 to messages 𝑢𝑖 modelling the information available to the adversary, referred to as the frame. And (𝐴𝐴 , 𝐴𝐵 ) denote the two allowlists of the readers, for example, 𝐴𝐴 = {𝑘 1, 𝑘 2 }. We write the combined tuple as 𝐴 := (𝐴𝐴 , 𝐴𝐵 ) With this configuration, we define our process semantics as the configuration transitions shown in Table 2.

5.3

Figure 4: Unified reader database example (wlog A) and disregarding the input on channel 𝑐 𝑋 : SΠ :=!(new 𝑘.in(𝑐 𝑋 , 𝑟 ).insert𝐴 (𝑘).¡new 𝑛𝑇 𝑇 )|(!𝑅 [𝐴]) We argue that if an adversary can distinguish between the processes M Π and SΠ , it can link tags using the allowlists. Using the initial example, we observe one possible execution trace: 𝜏repl .𝜏new .in(𝑐 𝑋 , A).𝜏insertA .𝜏repeat .𝜏new .out(𝑐𝑇 , 𝑤 0 ).𝜏seq .𝜏repl .in(𝑐𝑇 , 𝑧).𝜏then .out(𝑐 𝐴 , 𝑤 1 ) Continuing this trace with a subsequent interaction of tag 𝑘 ′ with 𝑅 [𝐵] leads to the following continuation of the trace: .𝜏repeat .𝜏new .out(𝑐𝑇 , 𝑤 2 ).𝜏seq .𝜏repl .in(𝑐𝑇 , 𝑧).𝜏else .out(𝑐 𝐵 , 𝑤 3 ) The resulting frame is {𝑤 0 → ⟨𝑛𝑇′ , ℎ(𝑘 ′, 𝑛𝑇′ )⟩, 𝑤 1 → ok, 𝑤 2 → ⟨𝑛𝑇′′, ℎ(𝑘 ′, 𝑛𝑇′′ )⟩, 𝑤 3 → err} In the unlinkable scenario with a single reader, or two readers having the same allowlist (as shown in Figure 4), there will be no err return, and the frame for the same observable communication trace in SΠ is: {𝑤 0 → ⟨𝑛𝑇′ , ℎ(𝑘 ′, 𝑛𝑇′ )⟩, 𝑤 1 → ok, 𝑤 2 → ⟨𝑛𝑇′′, ℎ(𝑘 ′, 𝑛𝑇′′ )⟩, 𝑤 3 → ok} Since the outputs of cryptographic hash functions and nonces are indistinguishable, it is true that the parts of the resulting frames are statically equivalent: {𝑤 0 → ⟨𝑛𝑇′ , ℎ(𝑘 ′, 𝑛𝑇′ )⟩, 𝑤 2 → ⟨𝑛𝑇′′, ℎ(𝑘 ′, 𝑛𝑇′′ )⟩} ∼ {𝑤 0 → ⟨𝑛𝑇′ , ℎ(𝑘 ′, 𝑛𝑇′ )⟩, 𝑤 2 → ⟨𝑛𝑇′′, ℎ(𝑘 ′, 𝑛𝑇′′ )⟩} However, the different remaining reply messages break the static equivalence:

Protocols

Using the algebra defined above, we model the real world execution as follows. Given a tag and receiver processes parametrized by 𝑟 as 𝑇 :=out(𝑐𝑇 , ⟨𝑛𝑇 , ℎ(𝑘, 𝑛𝑇 )⟩) 𝑅 [𝑟 ] :=in(𝑐𝑇 , 𝑧).lookup𝑟 𝑘 such that 𝑥¯ = eq(snd(𝑧), ℎ(𝑘, fst(𝑧))) in out(𝑐𝑟 , ok)else out(𝑐𝑟 , err) One tag and two receivers then form a real-world protocol M Π :=!(new 𝑘.in(𝑐 𝑋 , 𝑟 ).insert𝑟 (𝑘).¡new 𝑛𝑇 𝑇 )|(!𝑅 [A])|(!𝑅 [B]) This allows for the creation of as many tags as needed, as well as multiple sessions of both reader types. Upon tag creation, it is paired with a reader chosen by the adversary, supplied through the channel 𝑐 𝑋 . Once set up, the tag repeats many sessions, each with a fresh nonce 𝑛𝑇 . Our next objective is to establish a protocol that only has a global reader. To eliminate all effects from the allowlists, we define an “unlinkable by definition” protocol by creating a single receiver

{𝑤 1 → ok, 𝑤 3 → err} ≁ {𝑤 1 → ok, 𝑤 3 → ok} An adversary can exploit this discrepancy to distinguish the setting they are in and use it to link tag interactions.

6

Proposed Mitigation

To protect against AInf attacks, we employ a two-staged strategy combining: a) Prevention and Trapping, b) Detection. We describe these mechanisms in reverse order.

6.1

Detection

The purpose of this stage is to deterministically identify replay and relay attacks, enabling safe discconnection or continuation of the connection. Replay. A common method to prevent replay attacks is the use of counters, requiring synchronization between communicating devices to detect and discard replayed messages. However, this approach is susceptible to ND privacy violations [10]. Therefore, every reconnection establishes a fresh session key. Subsequent

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation

messages encrypted and integrity protected by this key cannot be replayed without being detected. On a reconnection with an allowlist, a mutually agreed fresh session key is derived by the end of the 3-round Authenticated Key Exchange (3AKE) [15, 52]. Our proposed protocol for A as initiator and B as responder combines preferred device verification within the 3AKE. Although the session key is only agreed upon by the end of the third round message, the key is generated at B after receiving the first message and after receiving a message at A in the second round. Therefore, all messages at the second round and onwards are sent ephemerally encrypted and integrity-protected. After mutual authentication with the 3AKE, a replay is detected deterministically. Relay. A common remedy for relay attacks is the use of GPS to determine the proximity of peer devices. However, the insufficient accuracy of GPS for this purpose [23, 45] leads us to adopt distance bounding protocols [27]. This protocol measures the distances of peer devices based on round-trip response delay to perform distance bounding (DiB). One caveat of DiB is that it requires authentication of the peer holding the same shared key (preferred device verification). Therefore, we perform DiB immediately after the 3AKE as described above. In this way, the handshake strategically combines the setup phase for DiB [46], preferred device verification, and fresh session key establishment all together. In this way, by the end of the DiB, agent A deterministically detects replay and relay attempts.

6.2

Prevention and Trapping

The goal of this stage is to prevent the exposure of any differentiable context during the 3AKE and to trap the adversary until the detection phase. Recall that our allowlist privacy violation allows an adversary to infer associations by observing positive or negative conditional outcomes. In our design, regardless of conditions’ outcomes, responses are sent. In the positive outcome, the messages are encrypted and integrity protected as per the specification. In the case of a negative condition outcome, responses are indistinguishable, random values of the same size and count as a positive conditional outcome to avoid exposing outcomes via other side channels employing oblivious responses. Further, we require the protocol to send messages that are encrypted by a fresh key and integrity-protected immediately after the session key generation. These messages are unique for the current session, hence cannot be replayed (unique response). Further, such messages cannot be predicted by the adversary (unpredictable response). Overall, we use fresh key bound messages to prevent exposing any relationship among messages, satisfying FO. Combining oblivious, unique, and unpredictable responses during 3AKE, prevents exposing differentiable context even if the adversary replays any message during the handshake. Therefore, the adversary is forced to continue to the later phases to find differentiable context, where, due to the mutually authenticated session key, any prior or recent replay is detected deterministically. At the same time, DiB detects the relay. As such, our approach is to employ prevention and trapping until after 3AKE and DiB are completed, whereafter both replay and relay attacks can be detected within the protocol, enabling devices to disregard further messages from adversaries without

compromising privacy. The salient feature of our design is that it keeps the faster reconnection requirements intact and provides a solution without needing synchronisation.

7

Tamarin Model Design

As explained in §4.1, modeling the formation of paired groups, unpaired groups; identities of users and devices; and shared data is critical to AInf. Precise protocol behavior and privacy properties are also essential. To achieve this, we use Tamarin Fact and its associated Tamarin Rule instantiation logic [6] to establish a hierarchical relationship among users, devices, protocol sessions, and the association of shared data/keys to the corresponding entities. Our model allows for an unbounded number of users and their respective devices. These devices interact with each other, executing an unbounded number of sessions based on the shared secrets stored as allowlists. The shared data is generated for each pair of devices associated with a user. This data is tied to the respective user and device identities. The sessions maintain the associated user and device identity terms through memory Facts. These sessions use the identity terms to validate messages such as message integrity checks and decryptions with shared keys. Further, Tamarin Facts model a database accessible to associated users and devices. In this way, the data is only accessed by the devices within an allowlist group. Pattern matching [6] is used with sessions to allow data access based on group hierarchy and device access control. For example, consider devices 1,2 of user Alice and devices 3,4 of user Bob. The Tamarin persistent Fact, with shared data LTK𝐴 , is generated as !DB(Alice, 1, LTK𝐴 ) and !DB(Alice, 2, LTK𝐴 ). These Facts represent the shared data LTK𝐴 accessible only by devices 1, 2 of user Alice. Similarly, for Bob the database Facts !DB(Bob, 3, LTK𝐵 ) and !DB(Bob, 4, LTK𝐵 ) act as local storage for user Bob. Devices of Alice cannot access shared secrets LTK𝐵 of Bob by means of pattern matching. By establishing the correct entity relationships and access control, as described above, allows encoding of required privacy properties. To prove WA, ND, and FO properties, we follow the symbolic formulation of [10, 48]. However, in order to secure privacy in paired communication, we formulate a trace-based property (termed as Lemma in Tamarin): oblivious and unpredictable responses. Additionally, we adapt the FO modeling. Lemma 1 (Unique Unpredicable Responses). Given labeled traces where every agent’s response message 𝑟𝑖 from session 𝑠𝑖 to the network is labeled Res(𝑠𝑖 , 𝑟𝑖 ) at timestep 𝑡𝑖 and the set of attacker derivable terms is KU A protocol has Unique and Unpredictable Responses if responses are unique: none of the privacy-critical responses are repeated: ∀𝑠 1, 𝑠 2, 𝑟, 𝑡 1, 𝑡 2 : Res(𝑠 1, 𝑟 )@𝑡 1 ∧ Res(𝑠 2, 𝑟 )@𝑡 2 ⇒ 𝑡 1 = 𝑡 2 and unpredictable: none of the privacy-critical responses can be constructed by adversaries before their release: ∧∀𝑠, 𝑟, 𝑡𝑖 , 𝑡 𝑗 : Res(𝑠, 𝑟 )@𝑡𝑖 ⇒ š(KU(𝑟 )@𝑡 𝑗 ∧ 𝑡 𝑗 < 𝑡𝑖 ) The DiB properties are obtained from prior research [54, 55]. Overall, to reason about privacy in our Tamarin model, we add the following security properties and revisions: Distance Bounding. Although DiB properties involve location and time measurements, Mauw et al. [55] proposes a symbolic formulation for the DiB property without using location and time. In

Jangid et al.

particular, it proves that as long as the response of a proximity check challenge cannot be sent before receiving the challenge itself, the protocol preserves a secure distance bounding check. Intuitively, an adversary can bypass the proximity check only if they can obtain protocol secrets to derive the DiB responses. Therefore we encode the DiB Lemma as follows: Lemma 2 (Distance Bounding). Given annotated traces using the label VS(𝑠, 𝑐) as the start of a verifier with session 𝑠 and challenge 𝑐, which waits for a corresponding response 𝑟 labeled VE(𝑠, 𝑟 ). The honest prover from the same session 𝑠 emits a response labeled P(𝑠, 𝑟 ). A protocol is Distance Bounding if ∀𝑠, 𝑐, 𝑟, 𝑡𝑠 , 𝑡𝑒 , 𝑡𝑝 , 𝑡𝑘 , 𝑠 ′, 𝑡𝑒 ′ it holds that for every verifier’s released challenge 𝑐 and received a response 𝑟 : VS(𝑠, 𝑐)@𝑡𝑠 ∧ VE(𝑠, 𝑟 )@𝑡𝑒 ⇒ ∃P(𝑠, 𝑟 )@𝑡𝑝 the prover is alive with the corresponding response at time 𝑡𝑝 ∧𝑡𝑠 < 𝑡𝑝 < 𝑡𝑒 the prover alive time 𝑡𝑝 is between released 𝑡𝑠 and received 𝑡𝑒 times ∧š(KU(𝑟 )@𝑡𝑘 ∧ 𝑡𝑘 < 𝑡𝑝 ) and the adversary cannot construct a correct response 𝑟 before the prover at 𝑡𝑘 ∧š(VE(𝑠 ′, 𝑟 )@𝑡𝑒 ′ ∧𝑡𝑒 ′ ≠ 𝑡𝑒 ) and each response is uniquely verified only once without replay (𝑟 is invalid in every other session 𝑠 ′ ) Revised Frame Opacity Modeling. Prior research [10, 48] emphasizes the FO property to prevent an attack that exploits the relationship between messages. However, it does not replace public constants with idealized random values for diff-equivalence checking. In the context of communication among paired devices, any plaintext response from protocol agents provides a clear signal for a successful or unsuccessful condition. Therefore, our FO forces all responses from the protocol to be indistinguishable from nonces. Finally, some protocols respond to the failure of verification checks by silently discarding the received message and stopping further communication. Since a silent discard response does not change among different protocol sessions, it forms an equality relationship of reactions in the protocols. Therefore, we can derive a FO privacy violation by modeling the silent discard behaviour as outputting a message of the public constant SILENT_DISCARD. It is worth noting that our oblivious and unpredictable response Lemma 1 ensures a similar goal as the FO property – no relationship among messages – but in the form of a trace property. Since the FO property is proved in a separate model with omitted conditions (§4.3), we prove our oblivious and unpredictable response lemma as a trace property with conditions intact. Lemma 1 compliant responses are required from the first privacy-critical condition until the checkpoint where replay and relay can be detected. In order to encode this property, we designate the Tamarin Action Fact PCCResponse(session, response) for all the individual outbound messages from both agents of the protocol. The response should be oblivious to preserve the FO, and it should be unpredictable to prohibit the adversary from gaining private information. Tamarin Model Assumptions. For our Tamarin model, we simplify the protocol design by omitting the exchange of public and privacyinsensitive messages, including channel selection, supported bit rates, vendor, and manufacturing details, etc. The DiB check procedures in distance bounding protocols often require multiple rounds

of challenges and response exchanges to improve statistics. However, following the formal verification of distance bounding by [55], we simplify it to only one round of challenge and keyed hash response. As described by Baelde et al., modeling FO requires removing privacy critical condition checks in the modeled protocol agents, thereby proving FO for a more generic protocol [10]. In this way, FO is verified for a superset of desired traces, implying verification on the desired subsets without loss of generality. Note that this applies only to the FO property.

8

Case Studies

In this section, we explain our analysis of two real-world wireless communication protocols and describe the identified vulnerabilities utilizing formal modeling.

8.1

Bluetooth

As depicted in Figure 5, the Bluetooth reconnection procedure starts with the advertisement of Random Private Addresses (RPA). Party activations 1 (between 1 and 1 ) and 2 indicate both 𝐴 and 𝐵 generating their respective RPA and verifying the received RPA in 2 and 3 respectively. If the IRK does not match any entry in the device’s allowlist, the receiving device silently discards the received message and stops responding further [11, 12]. After successfully resolving the IRK, the session key derivation phase begins. Since this is a reconnection procedure, both devices share a LTK from the pairing operation (§2). Both devices start by sharing nonces which are known as Session Key Diversifiers (skd). We omit the details of shared nonce IV, because the symbolic randomness of skd in Tamarin subsumes the randomness of IV as well. Note that when 𝐵 responds with its nonce skd𝐵 , it also informs 𝐴 to start the encryption by sending a plaintext START_ENC_REQ message [60]. Thereafter, both 𝐴 and 𝐵 encrypt a static, known value with the derived session key sessK. These packets are denoted by START_ENC_RSP. After the successful verification of encrypted values on both ends, secure data exchange follows. In the case of a MIC failure at 6 or 7 , the devices silently discard the received message and transition to their standby mode ("...it shall immediately exit the Connection state, and shall transition to the Standby state" [60, page. 3033]). The term MIC is used to distinguish from MAC, which could be confused with Media Access Control (MAC) addresses. Requirements for the AInf Attack. In the BAT attack, the shared data is the allowlist containing trusted device identities and keys: IRKs and LTKs. The allowlist is persistent across different Bluetooth communication sessions and local to only a few of the devices owned by a user forming a paired device group. The wireless communication medium and advertisement stages of Bluetooth communications allow an adversary to initiate a wireless connection without any user interaction. Finally, only the devices that share the same IRK and LTK can continue the connection. Other devices observe otherwise. Such deviating interactions of paired and known unpaired groups leak the information of devices belonging to the allowlist formed among IoT devices of the target user. The Discovered Privacy Vulnerabilities. There are a few key checkpoints in the protocol that violate privacy. The advertisement messages at 2 and 3 are vulnerable to replay or relay of the RPAs as explained in the BAT attack [65]. The Tamarin model reveals this

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation Device A irk𝐴 , irk𝐵 , LTK, DB𝐴

Device B irk𝐴 , irk𝐵 , LTK, DB𝐵

1

Device A irk𝐴 , irk𝐵 , LTK, DB𝐴

Device B irk𝐴 , irk𝐵 , LTK, DB𝐵

1

𝑛𝐴 ←$ N 𝑛𝐴 , h(𝑛𝐴 , irk𝐴 ) → ⟨𝑛𝐴 , 𝑚𝐴 ⟩ 1

𝑛𝐴 ←$ N 𝑛𝐴 , h(𝑛𝐴 , irk𝐴 ) → ⟨𝑛𝐴 , 𝑚 1 ⟩

2 1

If ∀irk𝑖 ∈ DB𝐵 : h(𝑛𝐴 , irk𝑖 ) ≠ 𝑚𝐴 𝑛𝐵 ←$ N 3

⟨𝑛𝐵 , 𝑚𝐵 ⟩ ← 𝑛𝐵 , h(𝑛𝐵 , irk𝐵 ) 2

If ∀irk𝑖 ∈ DB𝐴 : h(𝑛𝐵 , irk𝑖 ) ≠ 𝑚𝐵 3

skd𝐴 ←$ N

skd𝐴

4

3

skd𝐵 ←$ N

skd𝐵

5

SessK ← KDF(skd𝐴 , skd𝐵 , LTK)

SessK ← KDF(skd𝐴 , skd𝐵 , LTK)

"START_ENC_REQUEST" {"A_ENC_RESP"}SessK , MIC𝐴 5

4 6

𝑛𝐵 , 𝑚 2, MIC𝐵 2

If (∀(irk𝑖 , LTK𝑖 ) ∈ DB𝐴 SessK1 ∥SessK2 ← KDF(𝑛𝐴 , 𝑛𝐵 , LTK𝑖 ) MACSessK2 (𝑛𝐴 , 𝑛𝐵 , 𝑚 2, irk𝑖 ) ≠ MIC𝐵 ) 𝑚 3 ←$ N, MIC𝐴 ←$ N Else 𝑛𝐴SP ←$ N 𝑚 3 ← {𝑛𝐵 , 𝑛𝐵SP + 1, 𝑛𝐴SP }SessK1 MIC𝐴 ← MACSessK2 (𝑚 3 ) 𝑚 3, MIC𝐴 3

7

Verify MIC𝐵

{"B_ENC_RESP"}SessK , MIC𝐵

6

7

4

Verify MIC𝐴

MIC𝐴 invalid MIC𝐴 valid

2

𝑛𝐵 ←$ N, 𝑛𝐵SP ←$ N If ∀irk𝑖 ∈ DB𝐵 : h(𝑛𝐴 , irk𝑖 ) ≠ 𝑚 1 : 𝑚 2 ←$ N, MIC𝐵 ←$ N Else SessK1 ∥SessK2 ← KDF(𝑛𝐴 , 𝑛𝐵 , LTK) 𝑚 2 ← {𝑛𝐵SP }SessK1 MIC𝐵 ← MACSessK2 (𝑛𝐴 , 𝑛𝐵 , 𝑚 2, irk𝐵 )

𝑃0 ||𝑃1 ← PRF(𝑛𝐴SP, 𝑛𝐵SP, LTK)

𝑉0 ||𝑉1 ← PRF(𝑛𝐴SP, 𝑛𝐵SP, LTK) 4 6

loop 𝑖 ∈ 1 . . . 𝑁 5

𝑐𝑖

𝑐𝑖 ←$ {0, 1}

𝑃𝑐𝑖 𝑖 (𝑖 th bit)

Figure 5: Simplified Bluetooth advertisement and session key derivation protocol for reconnection procedure. by the failure of the WA and FO properties. FO is violated because of the silent discard, and WA is violated due to the possible replay of RPA messages. Similarly, at 6 the SILENT_DISCARD indicates different LTKs for each party. A relay adversary against privacy in the Bluetooth reconnection procedure uses the START_ENC_REQ response at 4 , which indicates correctness of all earlier verification checks: Both RPA resolutions in the advertisement phase at 2 and 3 . Note that during the relay, the random and hashed responses at 4 and 5 are not an indication of the verification condition outcomes. In contrast, START_ENC_REQ is a plaintext message that clearly indicates the positive condition outcome of the prior resolution of RPAs. In the Tamarin model, this is captured through a FO counter example using the plaintext message. Vulnerabilities at 4 and 6 are newly discovered in this paper as shown in Table 3. Note that all the checkpoints in the table independently contribute to our Ainf attack, and any one of them is sufficient. As mentioned earlier, some of these checkpoints were discovered in prior research; however, we provide new checkpoints deep into the sequences that expose our Ainf attack. Given the checkpoints’ independence, all must be mitigated to prevent the Ainf attack.

8.2

Countermeasures for Bluetooth

We propose an updated protocol for Bluetooth advertisement and session key derivation (Figure 6). We introduce a revised 3-way handshake, which ends with 𝐴 sending at 3 and 𝐵 receiving at 4 , followed by a DiB check. In the process, we add several critical modifications. Our modification begins at step 2 , where device

5

Δ𝑡 𝑃𝑐𝑖 𝑖 = 𝑉𝑐𝑖𝑖 ∧ Δ𝑡 < 𝑡 thr 6

Figure 6: Proposed Bluetooth advertisement and session key derivation protocol for the reconnection procedure. 𝐵 not only verifies 𝐴’s RPA. It derives a session key sessK, combining its own nonce 𝑛𝐵 with 𝐴’s nonce 𝑛𝐴 and the shared LTK (sessK = KDF(𝑛𝐴 , 𝑛𝐵 , LTK). Simultaneously, 𝐵 forgoes generating a hashed RPA and instead creates a MIC over 𝐵’s IRK using sessK as key. At step 3 , device 𝐴 resolves the IRK by constructing a local MIC and comparing it with the received one. This method of resolving the IRK using a MIC facilitates a multi-step process: simultaneous resolution of IRK and LTK; derivation of the identical session key sessK; and an integrity check for the proximity check nonce 𝑛 B−SP . To impose oblivious and unpredictable responses, steps 2 and 3 are designed to transmit some data independent of whether the MIC verification succeeds or fails. In the failure cases, nonces with the same structure as successful response messages are returned. For example, at 2 , the nonce MIC and 𝑀2 are crafted to match the size of the successful IRK resolution response messages. Uniformly random encrypted messages and MICs with the transient session key sessK facilitate oblivious responses across protocol sessions. Thus, even if 𝐴’s RPA is replayed at 1 , adversaries will be thwarted from decoding the IRK resolution condition outcome. Moreover, as the responses at 2 and 3 are encrypted with the ephemeral session key, these messages are immune to replay. Ultimately, at step 4 , 𝐵 can discern if any previous messages were replayed by verifying

Jangid et al. Device A netID, PSK, DB𝐴

Device B netID, PSK, DB𝐵

1

2

netID

Table 3: Summary of the identified vulnerabilities. Acronyms: BT: Bluetooth, WF: Wi-Fi-P2P

1

netID ∉ DB𝐵

3

Error

ocols Prot

Succes

BT BT BT WF WF WF

𝑛𝐵 ←$ N, rc = 0

𝑛𝐵 , rc 2

SessK ← KDF(𝑛𝐴 , 𝑛𝐵 , PSK)

SessK ← KDF(𝑛𝐴 , 𝑛𝐵 , PSK) MIC𝐴 invalid MIC𝐴 valid

5

𝑛𝐴 , rc + 1, {gtK}SessK, MIC𝐵 4

MIC𝐵 invalid

MIC𝐵 valid 5

{rc + 1}SessK, MIC3

6

verify MIC3 6

Figure 7: Simplified Wi-Fi P2P persistent group formation protocol flow.

the authenticated agreement of the transient session key sessK. Finally, at 4 , 𝐵 triggers a proximity check phase to validate 𝐴’s close proximity, enabling 𝐵 to detect both replay and relay attack vectors without exposing any associations.

8.3

1, 2, 3 4 6 1, 2 2, 3, 4 4 5

t(s)

poin

ck re Atta Failu play erty y/Re ? p a w l o e e r P R N

FO, WA FO FO FO, WA FO FO

Both Relay Relay Both Relay Relay

✗ ✓ ✓ ✗ ✓ ✓

n

Know

[65] – – [24, 37] – –

4

𝑛𝐴 , rc, MIC𝐴 3

k Chec

Wi-Fi

A simplified Wi-Fi P2P persistent reconnection procedure is shown in Figure 7. Assume device 𝐴 acts as a supplicant and device 𝐵 acts as an authenticator (§2). Similar to Bluetooth, there are two key phases: the advertisement and the session key derivation phase. In the former, 𝐴 seeks to join a previously connected group identified 1 with netID at invocation 1 (between and 1 ). If 𝐵 is part of this group, it retrieves its stored configuration for the netID group at 2 . If 𝐴 is also capable of acting as an authenticator, it proceeds to authenticate 𝐵. In the session key derivation phase, also known as the four-way handshake, 𝐵 generates and sends a random nonce 𝑛𝐵 and a replay counter rc. 𝐴 receives 𝐵’s nonce 𝑛𝐵 and combines it with its own nonce 𝑛𝐴 and the shared secret PSK to generate a session key sessK = KDF(𝑛𝐴 , 𝑛𝐵 , PSK) at 3 . In response, 𝐴 echoes back the replay counter rc, nonce 𝑛𝐴 , and MIC for the response. At 4 , 𝐵 verifies the MIC and responds with the necessary group information (e.g., the Group Temporal Key gtK). This key is used for sending secure and encrypted group messages in an established Wi-Fi P2P group. The response at 4 includes the incremented value of rc and the nonce 𝑛𝐵 . 𝐴 verifies the MIC and acknowledges the message

with an encryption of the incremented replay counter and the corresponding MIC. Note that the replay counter rc is increased by one after every pair of messages received and sent from either device. This is done to prevent replay of messages within the same session. Requirements for the AInf Attack. As per §4.1, Wi-Fi P2P stores network IDs and the PSKs as the allowlist in the local configuration file. This data persists across reconnecting procedures. Typically, IoT devices of a house form such persistent groups for faster reconnection of devices. Thus, our AInf attack on these network configurations exposes privacy-sensitive information about the ownership of the devices. Further, the wireless communication medium enables a device to initiate a reconnection without user involvement. The MIC verification conditions in the protocols serve as the privacy-critical conditions. Consequently, the Wi-Fi P2P persistent reconnection procedure is susceptible to our AInf attack. The Discovered Privacy Vulnerabilities. The first privacy violation occurs when device 𝐵 confirms the presence of netID in its locally stored configuration. It responds with the plaintext status of the match. In case of a failure, the response is sent with the response code “Fail; unknown P2P Group” [64, page. 93]. The plaintext responses expose an association between 𝐴 and the household’s devices group of 𝐵. Therefore, the Wi-Fi P2P advertisement phase is vulnerable to both replay and relay attacks due to the failure of FO, RR, and WA. Note that Wi-Fi’s plaintext SSID broadcast privacy violations were already studied [24, 37]. Recall that in the relay attack, any positive or negative indication of a conditional outcome can be inferred through later messages in the protocol. Particularly, the sequence of the replay counter rc, which is echoed back at 3 to 𝐴, and again the incremented value rc + 1 at 4 to 𝐵. Although successive rc values are designed to prevent message replay, their plaintext representations cause privacy violations. Moreover, the plaintext echo of the nonce 𝑛𝐴 is returned at 3 and 4 . This behavior violates the FO privacy property. The sequential relationship between the replay counter values and the equality of the nonce 𝑛𝐴 imply a successful pass of prior privacy-critical conditions. Such a violation is similar to the plaintext response at 4 in the Bluetooth reconnection procedure. Finally, SILENT_DISCARD at 4 and 5 of both devices [4, page. 2560-2564] further violates the FO property. Note that vulnerabilities due to the sequential message relationship at 2 , 3 , 4 and silent discard at 4 , 5 are newly discovered in this paper, as shown in Table 3.

8.4

Countermeasures for Wi-Fi

In our proposed Wi-Fi P2P persistent reconnection procedure, as shown in Figure 8, the revised 3-way handshake concludes with

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation Device A netID, PSK, DB𝐴

Device B netID, PSK, DB𝐵

1

𝑛𝐴 ←$ N, rc = 0 𝑛𝐴 , rc, h(𝑛𝐴 , rc, netID) → ⟨𝑛𝐴 , rc, 𝑚 1 ⟩ 1

3

2

𝑛𝐵 ←$ N If {∀netID𝑖 ∈ DB𝐵 : h(𝑛𝐴 , rc, netID𝑖 ) ≠ 𝑚 1 }: 𝑚 2 ←$ N, MIC𝐵 ←$ N Else SessK1 ∥SessK2 ← KDF(𝑛𝐴 , 𝑛𝐵 , PSK) 𝑛𝐵SP ←$ N 𝑚 2 ← {rc, 𝑛𝐵SP }SessK1 MIC𝐵 ← MACSessK2 (𝑛𝐴 , 𝑛𝐵 , 𝑚 2 )

𝑛𝐵 , 𝑚 2, MIC𝐵 2

If (∀(netID𝑖 , PSK𝑖 ) ∈ DB𝐴 SessK1 ∥SessK2 ← KDF(𝑛𝐴 , 𝑛𝐵 , PSK𝑖 ) MACSessK2 (𝑛𝐴 , 𝑛𝐵 , 𝑚 2 ) ≠ MIC𝐵 ) 𝑚 3 ←$ N, MIC𝐴 ←$ N Else 𝑛𝐴SP ←$ N 𝑚 3 ← {𝑛𝐴 , rc + 1, 𝑛𝐴SP, 𝑛𝐵SP + 1}SessK1 MIC𝐴 ← MACSessK2 (𝑚 3 )

𝑚 3, MIC𝐴 3

9

4

Verify MIC𝐴

5

𝑃0 ||𝑃1 ← PRF(𝑛𝐴SP, 𝑛𝐵SP, PSK)

𝑉0 ||𝑉1 ← PRF(𝑛𝐴SP, 𝑛𝐵SP, PSK) 4

loop 𝑖 ∈ 1 . . . 𝑁

6

𝑐𝑖

𝑐𝑖 ←$ {0, 1}

𝑃𝑐𝑖 𝑖 (𝑖 th bit)

Δ𝑡 𝑃𝑐𝑖 𝑖 = 𝑉𝑐𝑖𝑖 ∧ Δ𝑡 < 𝑡 thr

5

4 , random values replace the messages of successful conditional checks. These values are sampled from a distribution that is indistinguishable from success messages, thereby hindering an adversary’s ability to infer the outcome of the conditions. Consequently, if the adversary replays the initial message from 𝐴 at 1 , conditionoblivious responses prevent the adversary from concluding the AInf attack. Should the adversary persist in scrutinizing later responses, a replay of the message at 1 is detected at 4 . Since the adversary does not have access to shared secrets, they are thwarted from replaying messages during subsequent phases of the protocol. The additional safey measure of proximity checks at 5 and 6 allows for the identification and neutralization of both relay and replay attacks. Device 𝐵 can then choose to silently ignore further communication attempts by the adversary.

6

Figure 8: Proposed Wi-Fi P2P persistent group formation procedure. device 𝐴 sending at 3 and device 𝐵 receiving at 4 .Then a DiB check follows. Our method integrates the advertisement phase with a fourway handshake, initiating a series of strategic changes. Our first key modification in the advertisement phase is to hash the nonce 𝑛𝐴 , netID, and the replay counter 𝑟𝑐 like in the Simple Hash protocol: Hash(𝑛𝐴 , rc, netID). Similarly, device 𝐵 resolves the netID through the stored configuration file and responds with an encrypted replay counter, its own nonce, and a MIC. Note that the replay counter is encrypted using an ephemeral session key sessK. Following this, the response at 3 encrypts both nonces and the incremented replay counter value, thereby concealing the relationship between the nonce and the replay counter values during the message exchanges at 1 , 2 and 3 . As a result, the FO property is no longer violated because of the replay counter. Building on our Bluetooth solution, we introduce randomization for failure cases, making responses indistinguishable from those of successful condition outcomes. Specifically, at steps 2 , 3 , and

Tamarin Model and Evaluation

Tamarin Models. We use Tamarin-prover 1.6.1 on an Ubuntu 22.04 OS running on an Intel® i7-8550U CPU @ 1.80GHz × 8 processor with 16GB RAM. As shown in Table 4, we model the Bluetooth and Wi-Fi P2P reconnection procedures progressively. Starting from the advertisement phase models: BT-AD, Wi-Fi-P2P-AD and then extending the models with the session key derivation phase: BT-AD-SKD, Wi-Fi-P2P-AD-SKD for each case study. This progressive modeling allows for a granular examination of privacy violations within distinct segments of the entire protocol. Our proposed protocol models are referred to as BT-AD-SKD-PROPOSED and Wi-Fi-P2P-AD-SKD-PROPOSED. These refined models validate all the targeted privacy properties. The code can be accessed in folder “tamarin_code” in the provided artifact1 Overall, our proposed Tamarin models comprise a total of 1,137 lines of code, along with approximately 20 security lemmata. The number of lemmata varies depending on the quantity of privacycritical conditions identified in the protocols for each case study. Table 4 further illustrates the proving run times relevant to the privacy properties of the proposed models. We observe that the FO models require the most substantial computational time, roughly 3 minutes for BT-AD-SKD-PROPOSED and Wi-Fi-P2P-AD-SKD-PROPOSED. This disparity, relative to other properties across both case studies, can be attributed to the complexity of verifying the diff-equivalence between two execution systems, necessitating a more extensive state space than the traditional trace-based properties. The models demonstrating vulnerabilities in both protocols also concluded within 3 minutes, revealing the failure of privacy properties. Performance Overhead. We developed a preliminary prototype to compute the performance overhead of our proposed design changes. The simplified protocol specifications – as illustrated in Figures 5, 6, 7, and 8 – are encoded as user-level C++ socket programs, and the messages are channeled through Wi-Fi and Bluetooth adapters between two Linux devices. Since both of our machines do not have DiB measurement timing precision, we only implemented the challenge and response loops, passing one byte in each loop, without verifying the proximity through timing. The programs use 128-bit keys and nonces with AES provided by the Crypto++ library [32]. The responder device has an Intel i7-8550U CPU, 16GB RAM, Ubuntu 22.04 OS with an Intel Dual Band Wireless-AC 7265 1 Anonymized for reviewing: https://u.pcloud.link/publink/show?code=XgtitalK

Jangid et al.

Table 4: Protocol models, security properties, and runtimes for the proposed models. Acronyms. BT: Bluetooth, AD: Advertisement, SKD: Session Key Derivation Protocol

WA

FO

ND

SP

BT-AD BT-AD-SKD

✗ ✗

✗ ✗

✓ ✓

✗ ✗

BT-AD-SKD-PROPOSED (Runtimes)

✓ (6s)

✓ (160s)

✓ (1s)

✓ (12s)

Wi-Fi-P2P-AD Wi-Fi-P2P-AD-SKD

✗ ✗

✗ ✗

✓ ✓

✗ ✗

Wi-Fi-P2P-AD-SKD-PROPOSED (Runtimes)

✓ (9s)

✓ (195s)

✓ (2s)

✓ (20s)

wireless adapter, and an Intel Bluetooth wireless interface on HCI Version 4.2. The initiator device is equipped with an Intel i5-6200U CPU, 4GB RAM, Ubuntu 18.04.6 LTS with an Intel Wireless 3165 adapter, and the same Bluetooth configuration. The code can be accessed in folder “cpp_code” in the provided artifact1 . The runtimes for Wi-Fi and Bluetooth in Figure 9 are box-plots of 500 runs. Each runtime spans wall clock time from the beginning of the advertisement until the end of the session key establishment phase/ distance bounding check phase, as observed by the initiator 𝐴. We observe that our proposed changes ( prop boxplot) in the initial three rounds (3-way handshake) of message sequences have equivalent/less runtime than the original protocol (orig boxplot ). Only the round trips of the DiB challenge/response add significant overhead. The preliminary experiment suggests that as long as a distance bounding check can be optimized efficiently, the proposed protocol design can be implemented without a significant overhead.

𝑥˜ = 64.8

𝑥˜ = 80.1

𝑥˜ = 63.0

W

i-F i_ W Wi orig i-F Fi _ i W _pr pro i-F op p _ i_ pr DiB op _ _D 8 iB _1 BT 6 _o rig B BT T_ _p pr BT rop op _ _p Di ro B p_ _8 Di B_ 16

0

𝑥˜ = 47.8

50

𝑥˜ = 123.3

𝑥˜ = 11.0

𝑥˜ = 31.1

100

𝑥˜ = 52.5

runtime [ms]

150

Figure 9: Boxplot distribution of runtimes for the original specification (_orig), proposed protocols without DiB (_prop), and with DiB of 8 (_DiB_8) and 16 rounds (_DiB_16) of challenge and responses. Median runtimes are indicated with 𝑥˜ and the solid line in the box. Note that the standard outliers (1.5·IQR below and above Q1 and Q3 respectively) values are omitted.

10

Discussion

Limitations. Our research exhibits three salient limitations. First, the utilization of condition-oblivious responses, integral to the proposed solution, incurs an additional computational overhead. In the proposed protocols, condition-oblivious responses replace silent discard, which is more energy and performance-efficient. A potential compromise might allow users to toggle these features, adjusting the balance between privacy and performance according to individual needs. For instance, public figures or federal security personnel might willingly sacrifice some performance for more robust privacy protections. Second, allowlist groups for AInf can inadvertently misidentify target users, particularly in complex household scenarios where multiple family members access devices together. Such ambiguity can lead to false-positive identifications, misattributing a target user’s actions to another family member. Likewise, non-member inference may occur as a consequence of packet errors caused by wireless signal interference, which can yield false negatives, potentially misidentifying a vulnerable victim as nonvulnerable. Our process algebra formalization describes the possible processes with allowlists, but misses a rigorous proof that our additional requirements (distance bounding) are sufficient. Lastly, our formal modeling is not fully automated, requiring significant manual intervention for building and debugging the Tamarin model. Future Work. In terms of future developments, First, we plan to redesign the Bluetooth and Wi-Fi reconnection procedures, mandating changes to the stack code including comprehensive consideration of inconspicuous details of channel changes in the metadata exchange. Regarding the formalization, we would like to prove the absence of Ainf attacks given our proposed countermeasures. This will hopefully enhance existing privacy tools to adopt novel techniques to capture broader classes of privacy attacks. Ethics Consideration. We responsibly disclosed our findings to both the Bluetooth SIG and Wi-Fi Alliance. Both groups mentioned that due to the growing importance of privacy, they want to prioritize privacy protection for ongoing and future development efforts. They acknowledged our discoveries and proposed countermeasures. Additionally, they plan to inform their stakeholders after our publication.

11

Conclusion

We have addressed a privacy concern, wherein an individual’s association with sensitive groups can be inferred from wireless communications using allowlists. Our research clarifies how this privacy violation occurs, specifically within the context of Wi-Fi P2P persistent group formations and Bluetooth reconnection procedures. Through the development of formal models, we have not only validated the existence of this privacy violation but also devised a multifaceted strategy—including the use of oblivious and unpredictable responses, replay resistance, and proximity checks—to mitigate the risk. Our study enhances the understanding of privacy formalization and highlights critical privacy issues in prevalent wireless protocols. Overall, our work represents a significant step toward fostering privacy-preserving designs in the domain of wireless communication.

Association-based Privacy Attacks in Wireless Protocols: Formal Modeling and Mitigation

References [1] [n. d.]. Password Authenticated Connection Establishment Protocol PACE: Technical Advisory Group On Machine Readable Travel Documents (tag/mrtd).. ([n. d.]). Retrieved March 7, 2023 from http://www.icao.int/Meetings/TAGMRTD/TagMrtd22/TAG-MRTD-22_WP05.pdf. [2] 2017. BBC: Car theft ’relay’ devices seized in Birmingham. https://www.bbc. com/news/uk-england-birmingham-42370086, Accessed: July 31, 2023. [3] 2020. ATA5350 UWB Transceiver Security Considerations Application Note. https://ww1.microchip.com/downloads/aemDocuments/documents/WSG/ ApplicationNotes/ApplicationNotes/AN3523-ATA5350_UWB_Transceiver_ Security_Considerations_00003523A.pdf, Accessed: January 24, 2024. [4] 2020. Wi-Fi Protected Setup (WPS). Wi-Fi Alliance. https://www.wi-fi.org/ discover-wi-fi/wi-fi-protected-setup, Accessed: May 22, 2023. [5] 2021. MIFARE Plus EV2: Secure IC for Contactless Smart City Services. https://www.nxp.com/products/rfid-nfc/mifare-hf/mifare-plus/mifareplus-ev2-secure-ic-for-contactless-smart-city-services:MFPEV2, Accessed: January 24, 2024. [6] 2021. Tamarin Manual. (2021). Retrieved January 18, 2021 from https://tamarinprover.github.io/manual/book/001_introduction.html. [7] Adnan Abu-Mahfouz and Gerhard P Hancke. 2012. Distance bounding: A practical security solution for real-time location systems. IEEE transactions on industrial informatics 9, 1 (2012), 16–27. [8] Gennaro Avitabile, Vincenzo Botta, Vincenzo Iovino, and Ivan Visconti. 2022. Privacy and Integrity Threats in Contact Tracing Systems and Their Mitigations. IEEE Internet Computing 27, 2 (2022), 13–19. [9] Gildas Avoine, Ioana Boureanu, David Gérault, Gerhard P Hancke, Pascal Lafourcade, and Cristina Onete. 2021. From relay attacks to distance-bounding protocols. Security of Ubiquitous Computing Systems: Selected Topics (2021), 113–130. [10] David Baelde, Stéphanie Delaune, and Solène Moreau. 2020. A method for proving unlinkability of stateful protocols. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). IEEE, 169–183. [11] SIG Bluetooth. 2014. Bluetooth core specification version 4.2. Specification of the Bluetooth System (2014). [12] SIG Bluetooth. 2020. Bluetooth core specification version 5.2. Specification of the Bluetooth System (2020). [13] Ioana Boureanu, Aikaterini Mitrokotsa, and Serge Vaudenay. 2015. Practical and provably secure distance-bounding. Journal of Computer Security 23, 2 (2015), 229–257. [14] Rihab Boussada, Mohamed Elhoucine Elhdhili, and Leila Azouz Saidane. 2016. A survey on privacy: Terminology, mechanisms and attacks. In 2016 IEEE/ACS 13th International Conference of Computer Systems and Applications (AICCSA). IEEE, 1–7. [15] C. Boyd. 1995. Towards a classification of key agreement protocols. In Proceedings The Eighth IEEE Computer Security Foundations Workshop. 38–43. doi:10.1109/ CSFW.1995.518551 [16] Stefan Brands and David Chaum. 1994. Distance-bounding protocols, EUROCRYPT’93: Workshop on the theory and application of cryptographic techniques on Advances in cryptology (Secaucus, NJ, USA). [17] Alessandro Bruni, Eva Drewsen, and Carsten Schürmann. 2017. Towards a mechanized proof of selene receipt-freeness and vote-privacy. In Electronic Voting: Second International Joint Conference, E-Vote-ID 2017, Bregenz, Austria, October 24-27, 2017, Proceedings 2. Springer, 110–126. [18] Mayla Bruso, Konstantinos Chatzikokolakis, and Jerry Den Hartog. 2010. Formal verification of privacy for RFID systems. In 2010 23rd IEEE Computer Security Foundations Symposium. IEEE, 75–88. [19] Ksenia Budykho, Ioana Cristina Boureanu, Stephan Wesemeyer, Daniel Romero, Matt Lewis, Yogaratnam Rahulan, and Fortunat Rajaona. [n. d.]. Fine-Grained Trackability in Protocol Executions. In Network and Distributed System Security (NDSS) Symposium 2023. [20] Marco Casagrande, Mauro Conti, and Eleonora Losiouk. 2021. Contact tracing made un-relay-able. In Proceedings of the Eleventh ACM Conference on Data and Application Security and Privacy. 221–232. [21] Sofía Celi, Jonathan Hoyland, Douglas Stebila, and Thom Wiggers. 2022. A tale of two models: Formal verification of KEMTLS via Tamarin. In Computer Security–ESORICS 2022: 27th European Symposium on Research in Computer Security, Copenhagen, Denmark, September 26–30, 2022, Proceedings, Part III. Springer, 63–83. [22] Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, and Steve Kremer. 2016. Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic (TOCL) 17, 4 (2016), 1–32. [23] Nishanth Chandran, Vipul Goyal, Ryan Moriarty, and Rafail Ostrovsky. 2009. Position based cryptography. In Annual International Cryptology Conference. Springer, 391–407. [24] Maxim Chernyshev, Craig Valli, and Peter Hannay. 2015. On 802.11 access point locatability and named entity recognition in service set identifiers. IEEE Transactions on Information Forensics and Security 11, 3 (2015), 584–593.

[25] Vincent Cheval. 2014. Apte: an algorithm for proving trace equivalence. In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings 20. Springer, 587–592. [26] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: deciding equivalence properties in security protocols theory and practice. In 2018 IEEE symposium on security and privacy (SP). IEEE, 529–546. [27] Tom Chothia, Joeri De Ruiter, and Ben Smyth. 2018. Modelling and analysis of a hierarchy of distance bounding attacks. In 27th USENIX Security Symposium (USENIX Security 18). 1563–1580. [28] Tom Chothia, Flavio D Garcia, Joeri De Ruiter, Jordi Van Den Breekel, and Matthew Thompson. 2015. Relay cost bounding for contactless EMV payments. In Financial Cryptography and Data Security: 19th International Conference, FC 2015, San Juan, Puerto Rico, January 26-30, 2015, Revised Selected Papers 19. Springer, 189–206. [29] Véronique Cortier, Pierrick Gaudry, and Stéphane Glondu. 2019. Belenios: a simple private and verifiable electronic voting system. Foundations of Security, Protocols, and Equational Reasoning: Essays Dedicated to Catherine A. Meadows (2019), 214–238. [30] Cas Cremers, Kasper B Rasmussen, Benedikt Schmidt, and Srdjan Capkun. 2012. Distance hijacking attacks on distance bounding protocols. In 2012 IEEE symposium on security and privacy. IEEE, 113–127. [31] Ante Dagelić, Toni Perković, Bojan Vujatović, and Mario Čagalj. 2018. SSID oracle attack on undisclosed Wi-Fi preferred network lists. Wireless Communications and Mobile Computing 2018 (2018). [32] Wei Dai. 2024. Crypto++ Library 8.9. https://www.cryptopp.com/. [33] Sabyasachi Dash, Sushil Kumar Shakyawar, Mohit Sharma, and Sandeep Kaushik. 2019. Big data in healthcare: management, analysis and future prospects. Journal of big data 6, 1 (2019), 1–25. [34] Alexandre Debant and Stéphanie Delaune. 2019. Symbolic verification of distance bounding protocols. In Principles of Security and Trust: 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings 8. Springer, 149–174. [35] Yvo Desmedt. 1988. Major security problems with the ‘unforgeable’(Feige)Fiat-Shamir proofs of identity and how to overcome them. In Proceedings of SECURICOM, Vol. 88. 15–17. [36] Yvo Desmedt, Claude Goutier, and Samy Bengio. 1988. Special uses and abuses of the Fiat-Shamir passport protocol. In Advances in Cryptology—CRYPTO’87: Proceedings 7. Springer, 21–39. [37] Adriano Di Luzio, Alessandro Mei, and Julinda Stefa. 2016. Mind your probes: De-anonymization of large crowds through smartphone WiFi probe requests. In IEEE INFOCOM 2016-The 35th Annual IEEE International Conference on Computer Communications. IEEE, 1–9. [38] ICAO Doc. 2006. 9303-machine readable travel documents-part 1-2. Technical Report. Technical report, International Civil Aviation Organization, 2006. [39] D. Dolev and A. Yao. 1983. On the security of public key protocols. IEEE Transactions on Information Theory 29, 2 (1983), 198–208. doi:10.1109/TIT.1983. 1056650 [40] Christopher Ellis, Haohuang Wen, Zhiqiang Lin, and Anish Arora. 2022. Replay (far) away: Exploiting and fixing google/apple exposure notification contact tracing. Proceedings on Privacy Enhancing Technologies 4 (2022), 727–745. [41] Christopher Ellis, Yue Zhang, Mohit Kumar Jangid, Shixuan Zhao, and Zhiqiang Lin. [n. d.]. Deanonymizing Device Identities via Side-channel Attacks in Exclusive-use IoTs & Mitigation. ([n. d.]). [42] EMV EMVCo. 2009. Contactless specifications for payment systems. Book C-2, Kernel 2 (2009). [43] Aurélien Francillon, Boris Danev, and Srdjan Capkun. 2011. Relay attacks on passive keyless entry and start systems in modern cars. In Proceedings of the Network and Distributed System Security Symposium (NDSS). Eidgenössische Technische Hochschule Zürich, Department of Computer Science. [44] Jonathan Gordon, Jesko Perrey, and Dennis Spillecke. 2013. Big data, analytics and the future of marketing and sales. McKinsey: Digital Advantage (2013). [45] Xavier Torrent Gorjón, Jordi van den Breekel, and Paul van Iterson. 2015. Protecting against relay attacks forging increased distance reports. Research Project, Universiteit van Amsterdam (2015). [46] Gerhard P Hancke and Markus G Kuhn. 2005. An RFID distance bounding protocol. In First international conference on security and privacy for emerging areas in communications networks (SECURECOMM’05). IEEE, 67–73. [47] Gerhard P Hancke, Keith E Mayes, and Konstantinos Markantonakis. 2009. Confidence in smart token proximity: Relay attacks revisited. Computers & Security 28, 7 (2009), 615–627. [48] Lucca Hirschi, David Baelde, and Stéphanie Delaune. 2016. A method for verifying privacy-type properties: the unbounded case. In 2016 IEEE Symposium on Security and Privacy (SP). IEEE, 564–581.

Jangid et al.

[49] Naureen Hoque and Hanif Rahbari. 2023. Countering Relay and Spoofing Attacks in the Connection Establishment Phase of Wi-Fi Systems. In Proceedings of the 16th ACM Conference on Security and Privacy in Wireless and Mobile Networks. 275–285. [50] Interuniversity Microelectronics Centre (IMEC). [n. d.]. Distance Bounding Protocol for Bluetooth Secure Access. https://www.imec-int.com/en/expertise/ sensors-for-iot/secure-system-solutions/distance-bounding-white-paper, Accessed: Apr 17, 2024. [51] Mohit Kumar Jangid, Yue Zhang, and Zhiqiang Lin. 2023. Extrapolating Formal Analysis to Uncover Attacks in Bluetooth Passkey Entry Pairing. (2023). [52] Philippe Janson and Gene Tsudik. 1995. Secure and minimal protocols for authenticated key distribution. Computer Communications 18, 9 (1995), 645–653. doi:10.1016/0140-3664(95)99807-O [53] Ari Juels and Stephen A Weis. 2009. Defining strong privacy for RFID. ACM Transactions on Information and System Security (TISSEC) 13, 1 (2009), 1–23. [54] G. Lowe. 1997. A hierarchy of authentication specifications. In Proceedings 10th Computer Security Foundations Workshop. 31–43. [55] Sjouke Mauw, Zach Smith, Jorge Toro-Pozo, and Rolando Trujillo-Rasua. 2018. Distance-bounding protocols: Verification without time and location. In 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 549–566. [56] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN prover for the symbolic analysis of security protocols. (2013), 696– 701. http://tamarin-prover.github.io/ [57] Chrysanthi Paschou, Oliver Johnson, Ziming Zhu, and Angela Doufexi. 2023. Physical Layer Protection Against Relay/Replay Attacks for Short-Range Systems. In 2023 IEEE Wireless Communications and Networking Conference (WCNC). IEEE, 1–6. [58] Andreas Pfitzmann and Marit Hansen. 2008. Anonymity, unlinkability, undetectability, unobservability, pseudonymity, and identity management-a consolidated proposal for terminology. Version v0 31 (2008), 15. [59] Kasper Bonne Rasmussen and Srdjan Capkun. 2010. Realization of { RF } distance bounding. In 19th USENIX Security Symposium (USENIX Security 10). [60] Bluetooth SIG. 2019. Bluetooth SIG, Core specification version 5.2. Specification of the Bluetooth System (2019). https://www.bluetooth.com/specifications/specs/ core-specification-5-2/ Accessed: 2022-08-18. [61] David Stapleton. [n. d.]. The Human Toll: Examining The Impact Of Breaches On The Public. https://www.forbes.com/sites/forbestechcouncil/ 2022/05/27/the-human-toll-examining-the-impact-of-breaches-on-thepublic/?sh=1b2e148249a1. (Accessed on 10/07/2023). [62] Lo’ai Tawalbeh, Fadi Muheidat, Mais Tawalbeh, and Muhannad Quwaider. 2020. IoT Privacy and security: Challenges and solutions. Applied Sciences 10, 12 (2020), 4102. [63] Serge Vaudenay. 2007. On privacy models for RFID. In International conference on the theory and application of cryptology and information security. Springer, 68–87. [64] Wi-Fi Alliance. 2021. Wi-Fi Direct Technical Specification. https://www.wifi.org/discover-wi-fi/wi-fi-direct. Accessed: May 22, 2023. [65] Yue Zhang and Zhiqiang Lin. 2022. When Good Becomes Evil: Tracking Bluetooth Low Energy Devices via Allowlist-based Side Channel and Its Countermeasure. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security. 3181–3194.

Related documents

• FIDEM: A Standard-Compliant Framework for Secure Binding of MUD Profiles to IoT Devices#238511
• The Transport Layer Security (TLS) Protocol Version 1.3#139299
• Protocol Integration of Physical Layer Deception into EAP-TEAP Wi-Fi Authentication#1160935
• Protocol Integration of Physical Layer Deception into EAP-TEAP Wi-Fi Authentication#1156851
• A Survey of Privacy Vulnerabilities of Mobile Device Sensors#400466