Ross Horne ; Sjouke Mauw - Discovering ePassport Vulnerabilities using Bisimilarity

lmcs:6117 - Logical Methods in Computer Science, June 2, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:24)2021
Discovering ePassport Vulnerabilities using BisimilarityArticle

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: March 16, 2021
    Submitted on: February 19, 2020
    Keywords: Computer Science - Cryptography and Security,Computer Science - Logic in Computer Science

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1372 times.
    This article's PDF has been downloaded 573 times.