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证明器为这些属性提供了可机检的自动化证明。