Discovering ePassport vulnerabilities using bisimilarity

Horne, Ross and Mauw, Sjouke (2021) Discovering ePassport vulnerabilities using bisimilarity. Logical Methods in Computer Science, 17 (2). 24. ISSN 1860-5974 (https://doi.org/10.23638/LMCS-17(2:24)2021)

[thumbnail of Horne-Mauw-LMCS-2021-Discovering-ePassport-vulnerabilities-using-bisimilarity]
Preview
 Text. Filename: Horne-Mauw-LMCS-2021-Discovering-ePassport-vulnerabilities-using-bisimilarity.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (689kB)| Preview

Abstract

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.

CORE (COnnecting REpositories)