Symbolic verification of Apple's Find My location-tracking protocol
- URL: http://arxiv.org/abs/2510.14589v2
- Date: Tue, 21 Oct 2025 10:04:23 GMT
- Title: Symbolic verification of Apple's Find My location-tracking protocol
- Authors: Vaishnavi Sundararajan, Rithwik,
- Abstract summary: We present a symbolic model of the Find My protocol, as well as a precise formal specification of desirable properties.<n>We provide automated, machine-checkable proofs of these properties in the Tamarin prover.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Tracking devices, while designed to help users find their belongings in case of loss/theft, bring in new questions about privacy and surveillance of not just their own users, but in the case of crowd-sourced location tracking, even that of others even orthogonally associated with these platforms. Apple's Find My is perhaps the most ubiquitous such system which can even locate devices which do not possess any cellular support or GPS, running on millions of devices worldwide. Apple claims that this system is private and secure, but the code is proprietary, and such claims have to be taken on faith. It is well known that even with perfect cryptographic guarantees, logical flaws might creep into protocols, and allow undesirable attacks. In this paper, we present a symbolic model of the Find My protocol, as well as a precise formal specification of desirable properties, and provide automated, machine-checkable proofs of these properties in the Tamarin prover.
Related papers
- WatchWitch: Interoperability, Privacy, and Autonomy for the Apple Watch [50.89778047875175]
We reverse-engineer the Apple Watch's wireless protocols.<n>With WatchWitch, we break out of Apple's walled garden.<n>We thus pave the way for more consumer choice in the smartwatch ecosystem.
arXiv Detail & Related papers (2025-07-09T18:33:58Z) - On the (In)Security of Non-resettable Device Identifiers in Custom Android Systems [4.319029420721902]
We present IDRadar, a scalable and accurate approach for identifying vulnerable properties and settings on custom Android ROMs.<n>We have identified 8,192 system properties and 3,620 settings that store non-resettable identifiers, with 3,477 properties and 1,336 settings lacking adequate access control.<n>Our large-scale analysis can identify a large number of security issues which are two orders of magnitude greater than existing techniques.
arXiv Detail & Related papers (2025-02-21T07:52:46Z) - Privacy Analysis of Samsung's Crowd-Sourced Bluetooth Location Tracking System [11.347823817094485]
We present a detailed privacy analysis of Samsung's Offline Finding protocol.<n>The OF protocol uses Bluetooth Low Energy to broadcast a unique beacon for a lost device.<n>We examine several security and privacy related properties of the protocol and its implementation.
arXiv Detail & Related papers (2022-10-26T13:31:24Z) - AirGuard -- Protecting Android Users From Stalking Attacks By Apple Find
My Devices [78.08346367878578]
We reverse engineer Apple's tracking protection in iOS and discuss its features regarding stalking detection.
We design "AirGuard" and release it as an Android app to protect against abuse by Apple tracking devices.
arXiv Detail & Related papers (2022-02-23T22:31:28Z) - A Non-Intrusive Machine Learning Solution for Malware Detection and Data
Theft Classification in Smartphones [0.06999740786886537]
Successful mobile malware attacks could steal a user's location, photos, or even banking information.
There is a need besides just detecting malware intrusion in smartphones to also identify the data that has been stolen to assess, aid in recovery and prevent future attacks.
We propose an accessible, non-intrusive machine learning solution to not only detect malware intrusion but also identify the type of data stolen for any app under supervision.
arXiv Detail & Related papers (2021-02-12T13:31:27Z) - BeeTrace: A Unified Platform for Secure Contact Tracing that Breaks Data
Silos [73.84437456144994]
Contact tracing is an important method to control the spread of an infectious disease such as COVID-19.
Current solutions do not utilize the huge volume of data stored in business databases and individual digital devices.
We propose BeeTrace, a unified platform that breaks data silos and deploys state-of-the-art cryptographic protocols to guarantee privacy goals.
arXiv Detail & Related papers (2020-07-05T10:33:45Z) - Adding Location and Global Context to the Google/Apple Exposure
Notification Bluetooth API [10.538285220638988]
There are four ways of propagating context between any two users.
Two such methods allow private location logging, without revealing the location history within an app.
The other two are encryption-based methods.
arXiv Detail & Related papers (2020-07-01T08:03:21Z) - Mind the GAP: Security & Privacy Risks of Contact Tracing Apps [75.7995398006171]
Google and Apple have jointly provided an API for exposure notification in order to implement decentralized contract tracing apps using Bluetooth Low Energy.
We demonstrate that in real-world scenarios the GAP design is vulnerable to (i) profiling and possibly de-anonymizing persons, and (ii) relay-based wormhole attacks that basically can generate fake contacts.
arXiv Detail & Related papers (2020-06-10T16:05:05Z) - Decentralized Privacy-Preserving Proximity Tracing [50.27258414960402]
DP3T provides a technological foundation to help slow the spread of SARS-CoV-2.
System aims to minimise privacy and security risks for individuals and communities.
arXiv Detail & Related papers (2020-05-25T12:32:02Z) - PGLP: Customizable and Rigorous Location Privacy through Policy Graph [68.3736286350014]
We propose a new location privacy notion called PGLP, which provides a rich interface to release private locations with customizable and rigorous privacy guarantee.
Specifically, we formalize a user's location privacy requirements using a textitlocation policy graph, which is expressive and customizable.
Third, we design a private location trace release framework that pipelines the detection of location exposure, policy graph repair, and private trajectory release with customizable and rigorous location privacy.
arXiv Detail & Related papers (2020-05-04T04:25:59Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.