Formal Methods in the Software Life Cycle

[ main | cases | smart cards | formal methods | schedule | groups ]

Below some information and pointers about smart cards and Java card that you will use in this OOTI course. This should help you get started writing your first smart card applets and host applications.

Smart Card

Smart cards communicate with the outside world by receiving commands and answering them. The protocol is described in the ISO7816-4 standard.

Java Card is a "dialect" of Java for programming such smart cards. A brief introduction to Java Card is available at JavaWorld. Lots more information is available from Sun's Java Card site. In particular, you can download the Java Card Development Kit there. The kit includes the Java Card API which contains classes you can use in your applet. Applets are compiled using a normal Java compiler and transformed to CAP files using a converter included in the kit. The protocol to download CAP files onto a smart card is described in the Global Platform standard.

We will be using IBM JCOP smart cards which support Java Card 2.2.1 and Global Platform 2.1.1. Applets can be loaded onto the card using the JCOP toolset software that comes with the cards. The latest version of the JCOP toolset is only available as an Eclipse plugin. (For unclear reasons, the card simulator in Eclipse plugin does not work for RMI applications. Please rely on a real card instead.)

Terminal

The terminal (or host application) is also written in Java. Obviously, you will need to install a recent version of the Java 2 SDK. Two extra APIs are needed: one to communicate with the reader and one to do cryptographic computations.

For communicating with the smart card 'reader' JPCSC is used. JPCSC is a simple Java-based middleware API for programming smart card host applications. An alternative for JPCSC is the OpenCard Framework (OCF).

Since the host application will need to do some cryptographic computations, you also need to install a cryptographic provider compatible with Sun's JCE. (The standard Java library does provide an API for cryptography, but the underlying engine lacks some of the important cryptographic primitives due to export restrictions.) The Bouncy Castle provider is recommended.

The smart card reader used in this course, the Towitoko ChipDrive micro, connects to a USB port. You might need to download drivers for your operating system from the Towitoko web site. The JCOP tools talk to the Chipdrive via PC/SC.

API Documentation and Jars

Jar files should be copied to the jre\lib\ext folder of the Java 2 SDK in use. The dll files should be copied to \Windows or \Windows\System32.

Example applications

Some small example smart card applications are available:

Chipknip terminal

A simple JPCSC terminal to get the current balance of your Chipknip card. (Chipknip is the Dutch national E-Purse.) Have a look at the Java file: ChipknipTerminal.java. This example demonstrates that your setup (reader and middleware APIs) is ok.

Table applet and terminal

This simple applet implements a multiplication table which supports two commands: one for initializing the table (can only be called once), and one for getting entries from an initialized table. The terminal can be used to first initialize and then use the applet. Have a look at the source files in TableAppletRMI.zip and TableHostRMI.zip. This example demonstrates Java Card (RMI) and JPCSC programming. You can unzip the files to your Eclipse project/workspace directory and load the applet (after compiling it) to the card with JCOP shell. To complie and run the host application you first need to edit the TableHostRMI classpath to include offcard.jar, rmioffcard.jar, and jpcsc.jar, to be found in the Eclipse JCOP toolset plugin directory. The applet is specified in JML.

Calculator applet and terminal

This simple applet implements a calculator which operates on signed shorts. Overflow is silent. The terminal sends a command for every key on the keypad a user presses, the applet responds by sending the number to put on the display (i.e. the terminal has no state at all). Have a look at the source files in CalcAppletRMI.zip and CalcHostRMI.zip. This example demonstrates Java Card (RMI) and JPCSC programming. You can unzip the files to your Eclipse project/workspace directory and load the applet (after compiling it) to the card with JCOP shell. To complie and run the host application you first need to edit the CalcHostRMI classpath to include offcard.jar, rmioffcard.jar, and jpcsc.jar, to be found in the Eclipse JCOP toolset plugin directory.

RSA crypto example

This simple example shows how to do RSA keypair generation, encryption and decryption in Java. Have a look at the source files in: RSAKeyGen.java, RSAEncrypt.java and RSADecrypt.java.

RSA crypto applet and terminal

The applet encrypts or decrypts blocks of data (length at most 128 bytes) using RSA keys which are generated off-card and uploaded to the card. RSA keys have to be sent to the card first and then the card needs to be "issued" before any encryption and decryption is done. The files with private and public keys that the host application requires/asks for can be generated with RSAKeyGen.java above. Have a look at the source files in CryptoAppletRMI.zip and CryptoHostRMI.zip. This example demonstrates Java Card (RMI), JPCSC programming and Java Card cryptography (RSA). You can unzip the files to your Eclipse project/workspace directory and load the applet (after compiling it) to the card with JCOP shell. To complie and run the host application you first need to edit the CryptoHostRMI classpath to include offcard.jar, rmioffcard.jar, and jpcsc.jar, to be found in the Eclipse JCOP toolset plugin directory.