| Summary: | 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.
|
|---|