一句话：用开放互模拟与经典FM模态逻辑发现并证明电子护照BAC/PACE协议的可链接性隐私漏洞。
本文揭示全球电子护照所实现的 ICAO 9303 标准中的隐私漏洞：近期通过检查站的持照人可在不打开电子护照的情况下被重新识别。作者以互模拟（bisimilarity）为核心分析工具，针对 applied π-calculus 提出一链方法：符号欠近似的开放互模拟（open bisimilarity），以及用于描述和证明攻击的经典 FM 模态逻辑。该漏洞利用 BAC 认证协议，并对改进安全性的 PACE 协议仍然有效，且已获 ICAO 确认。论文还给出证据，论证一种更准确反映攻击者能力的不可链接性（unlinkability）规约方案。
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 $\pi$-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.