Discovering ePassport vulnerabilities using bisimilarity

Ross Horne, Sjouke Mauw

Research output: Contribution to journalArticlepeer-review

8 Citations (Scopus)
13 Downloads (Pure)


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.
Original languageEnglish
Article number24
Number of pages52
JournalLogical Methods in Computer Science
Issue number2
Publication statusPublished - 2 Jun 2021


  • bisimilarity
  • ePassports
  • modal logic
  • privacy
  • protocols


Dive into the research topics of 'Discovering ePassport vulnerabilities using bisimilarity'. Together they form a unique fingerprint.

Cite this