利用双相似性发现电子护照漏洞
Discovering ePassport Vulnerabilities using Bisimilarity
AI总结：
本文利用双相似性发现ICAO 9303标准中电子护照的隐私漏洞，该漏洞影响BAC及PACE协议，并提出了开放双相似性与经典FM逻辑等方法来分析和认证此类攻击。
摘要：
我们发现了全球电子护照所实施的ICAO 9303标准中的隐私漏洞。这些漏洞已获ICAO确认，使得近期通过检查站的电子护照持有者无需打开其电子护照即可被重新识别。本文阐述了如何利用双相似性来发现这些漏洞，这些漏洞利用了BAC协议——ICAO 9303标准最初的电子护照认证协议——并且对于PACE协议仍然有效，PACE协议在最新的ICAO 9303标准中改进了BAC的安全性。为了处理此类双相似性问题，我们在此为应用π-演算开发了一系列方法，包括双相似性的符号下近似，称为开放双相似性，以及一种称为经典FM的模态逻辑，用于描述和认证攻击。我们提供证据来论证一种新的方案，用于指定此类不可链接性问题，该方案更准确地反映了攻击者的能力。
英文摘要：
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $π$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
