Ross Horne ; Sjouke Mauw - Discovering ePassport Vulnerabilities using Bisimilarity

lmcs:6117 - Logical Methods in Computer Science, June 2, 2021, Volume 17, Issue 2 -
Discovering ePassport Vulnerabilities using Bisimilarity

Authors: Ross Horne ; Sjouke Mauw

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.

Volume: Volume 17, Issue 2
Published on: June 2, 2021
Accepted on: June 2, 2021
Submitted on: February 19, 2020
Keywords: Computer Science - Cryptography and Security,Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 340 times.
This article's PDF has been downloaded 218 times.