We present the first formal analysis and comparison of the security of the two most widely deployed exposure notification systems, ROBERT and the Google and Apple Exposure Notification (GAEN) framework. ROBERT is the most popular instalment of the centralised approach to exposure notification, in which the risk score is computed by a central server. GAEN, in contrast, follows the decentralised approach, where the user's phone calculates the risk. The relative merits of centralised and decentralised systems have proven to be a controversial question. The majority of the previous analyses have focused on the privacy implications of these systems, ours is the first formal analysis to evaluate the security of the deployed systems -- the absence of false risk alerts. We model the French deployment of ROBERT and the most widely deployed GAEN variant, Germany's Corona-Warn-App. We isolate the precise conditions under which these systems prevent false alerts. We determine exactly how an adversary can subvert the system via network and Bluetooth sniffing, database leakage or the compromise of phones, back-end systems and health authorities. We also investigate the security of the original specification of the DP3T protocol, in order to identify gaps between the proposed scheme and its ultimate deployment. We find a total of 27 attack patterns, including many that distinguish the centralised from the decentralised approach, as well as attacks on the authorisation procedure that differentiate all three protocols. Our results suggest that ROBERT's centralised design is more vulnerable against both opportunistic and highly resourced attackers trying to perform mass-notification attacks.
翻译:我们首次正式分析和比较了两个最广泛部署的暴露通知系统(ROBERT和Google和苹果接触通知(GAEN)框架)的安全性。ROBERT是风险评分由中央服务器计算的最受欢迎的接触通知中央办法的分批。GAEN则采用分散管理办法,用户的手机计算风险。中央和分散管理的系统的相对优点证明是一个有争议的问题。前几次分析大多侧重于这些系统的隐私影响,我们是评价所部署系统安全性的第一个正式分析,即没有虚假的风险警告。我们模拟法国部署的ROBERT和最广泛部署的GAEN变体,即德国的Corona-Warn-App。我们孤立了这些系统防止错误警报的准确条件。我们确切地确定对手如何通过网络和蓝牙嗅探、数据库渗漏或所有手机的妥协、后端系统和卫生当局来破坏系统。我们还调查了对部署系统的最初规格的安全性,即没有虚假的风险警报。我们模拟了ROB的部署和最广泛的GARC协议,以便从我们提出的第27次的中央协议设计中找出了对攻击方案进行彻底的判断。