Symbolic verification of Apple's Find My location-tracking protocol
Vaishnavi Sundararajan, Rithwik
TL;DR
The paper tackles the privacy guarantees claimed by Apple's Find My protocol by building a symbolic model in the Tamarin prover under a DY adversary. It formalizes the protocol’s master beacon keys, rolling-key beacons, and the end-to-end encryption of location reports, and then proves a set of secrecy and forward-secrecy properties, delivering machine-checked proofs and discussing several verifiable lemmas. The work represents the first symbolic analysis of Find My, extending prior cryptographic analyses, and highlights both successful proofs (10/12 lemmas) and limitations (two inductive steps timing out) due to modelling and termination challenges. The results contribute to public trust in Find My’s privacy claims and provide a blueprint for symbolic verification of similar real-world crowd-sourced location protocols, while outlining concrete avenues for improving modelling fidelity and extending to indistinguishability properties. Overall, the study demonstrates the value and constraints of formal symbolic methods for assessing large-scale privacy-preserving location services in practice.
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.