print · source · login   

Biometric Passport

Related publications: [ASV10]

Description

The biometric passport is an electronic passport provided with a computer chip and antenna to authenticate the identity of travelers. The data on the passport is highly confidential, e.g. it might contain a fingerprint of its owner, and therefore is protected via several mechanisms to avoid and/or detect attacks. Examples of used protocols are Basic Access Control (BAC), Active Authentication (AA) and Extended Access Control (EAC). The interaction of the different protocols and according results are hard to understand. Official standards are documented in the International Civil Aviation Organisation's (ICAO) Doc 9303 [ICAO9303P1V1],[ICAO9303P1V2],[ICAO9303P3], which are extensive and informal. For a better understanding formal models can be useful, which can also provide a basis for model-based testing. This has been done manually by Mostowski et al. [MPSTW09]. However, developing such models by hand is a time-consuming task. Therefore, we used inference techniques to automatically generate a model of an existing passport implementation and could verify that the learned model is ioco-conforming [Tre08] to the hand-made specification by Mostowski et al.

We took a look at the interaction of the following messages:

  • Reset resets the system.
  • GetChallenge followed by CompleteBAC forms a BAC, which establishes secure messaging with the passport by encrypting transmitted information.
  • FailBAC constitutes an invalid BAC.
  • ReadFile(int file) tries to access highly sensitive data specified in a certain file, which is represented as an integer value in the range from 256 up to (and including) 511.
  • AA prevents cloning of passport chips.
  • CA followed by TA forms an EAC, which uses mutual authentication and stronger encryption than BAC to control access to highly confidential data.
  • FailEAC constitutes a valid CA and an invalid TA.

For each of these messages a value OK or NOK may be returned by the SUT. A global overview of the valid behavior is depicted in Figure 1, where a BAC consists of a GetChallenge followed by a CompleteBAC and an EAC constitutes a CA followed by a TA. The files 257 and 258 should be readable after a BAC. File 257 contains Machine Readable Zone (MRZ) data, i.e. name, date of birth, nationality, document number, etc. whereas file 258 contains a facial image. File 259 comprises biometric data like fingerprints or an iris scan, which are only readable after a BAC followed by an EAC. All other files should not be readable at any point in time.

Simplified model of the biometric passport
Fig. 1: Simplified model of the biometric passport

The SUT

We used an authentic biometric passport as SUT. The data on the chip could be accessed via a smart card reader; JMRTD served as API. We connected the SUT to an abstraction mapping, which performed a translation as described in the following section. As an alternative, the SUT can be substituted by the SUT model in .xml format that behaves like the real SUT.

SUT model
Fig. 2: SUT model