论文标题
使用双次症发现Epassport脆弱性
Discovering ePassport Vulnerabilities using Bisimilarity
论文作者
论文摘要
我们在全球Epassports实施的ICAO 9303标准中发现了隐私漏洞。 ICAO确认的这些漏洞使一个Epassport持有人最近通过了检查站，可以在不打开Epassport的情况下重新识别。本文解释了如何使用双象性来发现这些漏洞，从而利用BAC协议 - 原始ICAO 9303标准Epassport身份验证协议 - 对PACE协议仍然有效，该协议在最新的ICAO 9303标准中提高了BAC的安全性。为了解决此类差异性问题，我们在这里开发了一系列用于应用的$π$ -CALCULUS的方法，包括对双性异性的象征性不足，称为开放式双性异性，以及一种称为Classical 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.
