Reference implementations for Mondex using JavaCard

We introduce three different implementations for the Mondex electronic purse verification challenge . In previous work (see here and here ) we verified security and correctness properties of the Mondex money transfer protocol.

Here we present a way to translate the formal specifications into running JavaCard code. We introduce three different ways to implement the protocol, one using symmetric cryptography, one using asymmetric cryptography and finally one using special datatypes for cryptographic protocols and symmetric cryptography. All implementations presented in this paper are able to run on a Gemplus GemxpressoRAD ProR3 SmartCard.

• Implementation using symmetric cryptography and APDU communication
• Implementation using asymmetric cryptography and APDU communication
• Implementation using symmetric cryptography and specialized communication data types

Here you find an Eclipse Project containing the third implementation above embedded into a Smart Card simulation environment and a rudimentary console terminal. Run it by simply executing java -jar mondex.jar . If you want to make changes or try out attacks, feel free to modify the MondexTerm class containing the main method and a very simple exemplary money transfer. Please note that we assume that the card initialization (installation of the applet and initialization of data) happens in a secure environment.

The KIV project containing the refinement correctness proof for the third implementation is here