暴露通知系统的自动化安全分析

我们首次对两个部署最广泛的暴露通知系统 ROBERT 与 Google 和 Apple 暴露通知（GAEN）框架的安全性进行了形式化分析与比较。ROBERT 是集中式暴露通知方法最流行的实现，其中风险评分由中央服务器计算。相比之下，GAEN 遵循去中心化方法，由用户手机计算风险。集中式与去中心化系统的相对优劣已被证明是一个有争议的问题。先前大多数分析聚焦于这些系统的隐私影响，而我们的工作是首个评估已部署系统安全性——即不存在虚假风险警报——的形式化分析。我们对 ROBERT 的法国部署以及部署最广泛的 GAEN 变体德国 Corona-Warn-App 进行了建模。我们隔离了这些系统防止虚假警报的精确条件。我们确切确定了攻击者可通过网络与蓝牙嗅探、数据库泄露或手机、后端系统及卫生机构的 compromised 来破坏系统的途径。我们还研究了 DP3T 协议原始规范的安全性，以识别所提出方案与其最终部署之间的差距。我们共发现 27 种攻击模式，包括许多区分集中式与去中心化方法的模式，以及针对授权过程的、区分全部三种协议的攻击。我们的结果表明，ROBERT 的集中式设计对于试图执行大规模通知攻击的机会主义攻击者和资源高度充足的攻击者都更为脆弱。