Apple Find My位置跟踪协议的符号验证
密码学与安全
2025-10-22 v2
摘要
跟踪设备虽然旨在帮助用户在遗失/被盗时找到自己的财物，但这带来了关于不仅用户自身，甚至在基于人群的定位跟踪中，与这些平台其他方面相关联的隐私和监视问题的新问题。Apple Find My或许是最普遍的此类系统，能够即使没有任何蜂窝支持或GPS，即可在全球数百万台设备上定位。Apple声称该系统是私人和安全的，但代码是专有的，这些宣称必须信赖。众所周知，即便拥有完美的密码学保证，逻辑缺陷仍可能滋生于协议中，导致不可取的攻击。本文我们提出了Find My协议的符号模型，以及一组精确的可接受属性规范，并在Tamarin证人中提供自动、机器可检查的这些属性的证明。
引用
@article{arxiv.2510.14589,
title = {Symbolic verification of Apple's Find My location-tracking protocol},
author = {Vaishnavi Sundararajan and Rithwik},
journal= {arXiv preprint arXiv:2510.14589},
year = {2025}
}