Learned models

Learned models of bank card protocols

We have learned models for several client implementations, i.e. real bank cards from different banks. Access to the smart cards was realised via a standard smart card reader. The models might be incorrect, but already showed reproducible bugs in some cases.

Pictures of Learned Models

Some of the learned models listed in the table above are shown below :

Fig. 2: Automaton of Dutch Maestro application. Just to highlight one observation that can be made from this diagram: the VERIFY operation, i.e. the verification of the PIN code by the smartcard, is optional; this makes sense because the terminal may check the PIN code with the bank (so-called online PIN verification), or choose not to verify the PIN at all.

Fig. 3: Automaton of Dutch SecureCode Aut application. Note that here the VERIFY operation - i.e. verification of the PIN code - must be passed successfully before cryptograms can be generated, except for the AAC cryptogram to abort the session.

Fig. 4: Automaton of Maestro application on Volksbank bank card.

Fig. 5: Automaton of Visa Debit application on Barclays card. Note that the INTERNAL AUTHENTICATE can be performed at any stage of the protocol.