Java Machine Readable Travel Documents
June 22, 2010 – 6 years, 9 months ago, by woj
Not really a verification problem, but an interesting Java case study for verification. JMRTD is a comprehensive Java implementation of biometric e-Passports. The project provides a host side application to read biometric passports. It supports the full International Civil Aviation Organization passport specification. Additionally, the project provides a smart card reference implementation of an epassport for Java Cards. This part allows creation of specification conformant biometric passports on Java Cards.
All the code of the project is available at SourceForge and accessible with:
svn co https://jmrtd.svn.sourceforge.net/svnroot/jmrtd jmrtd
The verification problems for ePassports can be generally divided into two categories: formal verification of the open source implementation quoted above, and testing and validation of actual passports. With respect to the latter RU have been involved in several security and standard conformance evaluations of actual passports. Validation of actual passports is considerably more difficult as there are no implementation details available, and the passport is a sealed black box. In this presentation we discuss a method to thoroughly test passports using the model-based testing approach. First a formal model of the passport protocols was created in terms of transition graphs. Then the TorXakis tool performs random walks through the model and correspondingly executes a protocol run on the passport and validates the passport's response.
A comprehensive set of ePassport related links can be found at JMRTD website. Additionally here some relevant interesting papers: