We used authentic bank cards as SUT. Access to the smartcards was realised via a standard smartcard reader and a testing harness/mapper, as illustrated in Fig. 1. As learner we used to the LearnLib library. The test harness is just over 300 lines of Java code. Most of this code is generic code to set-up a connection to the smartcard reader. A regular smartcard reader was used, and communication was performed using the standard Java Smart Card I/O library.
The mapper translates the abstract command (from the input alphabet of the Learner) to a concrete command APDU, and translates a response APDU to a more abstract response (in the output alphabet of the Learner). For many parameters of these commands the mapper uses some fixed value, for instance for the random number sent as argument of INTERNAL AUTHENTICATE, the payload data for the cryptograms generated by the card, and the (correct) guess for the PIN code. One would not expect a different random number to affect the control flow of the application in any meaningful way, so by fixing values here we are unlikely to miss interesting behaviour. Note that we have two different payloads when requesting the cryptograms due to the difference between the first and second request for a cryptogram. As these payloads are different, both a correct and an incorrect payload is used when requesting cryptograms. Obviously, entering an incorrect PIN code would affect the control flow, but learning about the behaviour in response to incorrect PIN guesses is very destructive as it will quickly block the card. For several commands different variants are provided by the mapper:
The mapper does not output the entire response of the smartcard to the learner. It only returns the 2 byte status word, but not any additional data returned by the card. For most commands, like GET PROCESSING OPTIONS, this additional data returned will always be the same, so there is not much interest in learning it. The only exception to this is the GENERATE AC command: here the mapper does return the type of cryptogram that was returned by the card.
The Visa branded card can perform the GET DATA command to retrieve the current value of the ATC. The mapper keeps track of the value of the counter to be able to learn the transitions where a counter is increased. The GET DATA command only returns the current value of the ATC if the Visa Debit application is selected. Since the mapper depends on the value of the ATC, the Visa Debit application is automatically selected before an output query is performed. The mapper retrieves the value of the ATC after each output query and adds the difference with the stored value of the ATC to the response, e.g. ‘+1’ on an edge indicates the ATC was increased by one in this transition.