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.

翻译：追踪设备虽旨在帮助用户在遗失或被盗时寻找个人物品，却引发了新的隐私与监控问题——不仅涉及设备用户自身，在众包位置追踪场景下，甚至可能波及与这些平台仅存在间接关联的其他个体。苹果公司的Find My系统或许是当前应用最广泛的此类系统，其能够定位全球数百万台甚至不具备蜂窝网络支持或GPS功能的设备。苹果宣称该系统具有隐私性与安全性，但由于其代码属于专有技术，此类声明仅能依赖用户信任。众所周知，即使具备完美的密码学保障，协议仍可能潜藏逻辑缺陷，从而导致非预期的攻击。本文构建了Find My协议的符号化模型，制定了目标属性的精确形式化规约，并利用Tamarin证明器为这些属性提供了可自动验证的机器可检证明。