Java Card Related and Other Downloads


Here you can find some programs, libraries, and specifications I developed over the time.

Java Card Firwall Tester

Java Card Firwall Tester has been developed for the PinPas Java Card Project, its page can be found here.

ocfjpcsc

The ocfjpcsc library provides an OCF driver for PCSC compliant smart card readers. The library is based on JPCSC Java API, which is required to run ocfjpcsc. ocfjpcsc provides the same functionality as OCF To PC/SC Shim, but probably provides more stable and simpler setup for Linux - it relies on the native layer in JPCSC.

You can download the current version of ocfjpcsc here.

ESC/Java2 JML specs for Java Card API 2.2.1

These JML specifications can be used to check JML annotated Java Card 2.2.1 applets with ESC/Java2. For more information see NOTES file in the distribution.

You can download the current version of the Java Card API 2.2.1 specs here (a zip file here). Note: this should be still considered work in progress. If you find mistakes, bugs, ommisions, or things that you don't like, write me an e-mail.

KeY specs/reference implementation for Java Card API 2.2.1

Here you can find Java Card API 2.2.1 specifications and reference implementation for the KeY System. So far the specs are only Dynamic Logic ones. As soon as the KeY JML front-end stabilises I will make an effort to include JML specs too. There are two versions of the API available:

  1. javacardapi-20070821.tar.gz (or ZIP) with very lightweight invariant semantics, i.e., each invariant is established for only one instance of a given class. This version of the specification has been fully verified.
  2. javacardapi-20070821-allinv.tar.gz (or ZIP) with stronger invariant semantics, i.e., each invariant is established for all instances of a given class. This version of the specification has not yet been fully verified, however, initial attempts show that most specs should be verifiable.
For these projects you will need a failrly recent development version of the KeY system, you can download a working version here (only the source distribution): key-0.2610-source.tgz. See also the README file included in the archive and check out the paper that describes this case study.

Proofs

All the proofs for the lightweight invariant semantics version can be downloaded here:
  1. proofs-20070821.tar.gz
  2. proofs-20070821.zip
Please note that some proofs may not load correctly/fully due to current bugs in KeY.

The Mobius Demonstrator Case Study

Together with Erik we specified and annotated in JML the Mobius Demontrator Case Study to prove so-called midlet navigation property. The case study and JML annotations are described in this technical report and this LNCS paper, the full code can be downloaded here. To verify it you will need a recent version of ESC/Java2 running on a SUN/Oracle JDK 1.4.

This case study is also published at the Verify This repository of the COST Action IC0701.

Java Card Tools for Together CC

Some long time ago I also wrote Java Card Tools [PDF] for Borland Together Control Center CASE tool. Unfortunately, it is out of date (as is Together CC) and it is not maintained anymore.

Wojciech Mostowski