利用互模拟发现电子护照漏洞
密码学与安全
2023-06-22 v5 计算机科学中的逻辑
摘要
我们揭示了全球电子护照所实现的 ICAO 9303 标准中的隐私漏洞。这些经 ICAO 确认的漏洞使得近期通过检查点的电子护照持有者无需打开其电子护照即可被重新识别。本文解释了如何利用互模拟发现这些漏洞，它们利用了 BAC 协议——最初的 ICAO 9303 标准电子护照认证协议——并且对 PACE 协议仍然有效，后者在最新 ICAO 9303 标准中改进了 BAC 的安全性。为解决此类互模拟问题，我们在此开发了一系列应用于 -演算的方法，包括互模拟的符号欠近似（称为开放互模拟）以及用于描述和认证攻击的模态逻辑（称为经典 FM）。我们提供了证据以论证一种用于规范此类不可链接性问题的新方案，该方案更准确地反映了攻击者的能力。
引用
@article{arxiv.2002.07309,
title = {Discovering ePassport Vulnerabilities using Bisimilarity},
author = {Ross Horne and Sjouke Mauw},
journal= {arXiv preprint arXiv:2002.07309},
year = {2023}
}