CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security
Rajeev Goré and Lan Duy Nguyen

cardKt is a modal theorem prover written in Java specifically designed to be used with Java smart cards to investigate the possibility of onboard software verification.  This page contains information on the research done, cardKt code, and a list of links related to smart cards and verification.


Here is a web interface to the cardKt prover. The web interface simulates the client interface software to a card reader, and connects to the prover code as it would when the prover code resided on a smart card.

Notation for input formula: <F> : forward (future) diamond operator (prefix), <P> : backward (past) diamond operator (prefix), [F] : forward box operator (prefix), [P] : backward box operator (prefix), - : negation operator (prefix), & : conjunction operator (infix), + : disjunction operator (infix), -> : implies operator (infix), <- : backward implies operator (infix), <-> : if and only if operator (infix), T : constant true, F : constant false. Parentheses may be used for grouping. Lower case letters (a..z) can be used for variables.

Some sample inputs in the correct format are available as inputs.txt.

To try the cardTAP theorem prover, your browser must be Java enabled.


You may obtain a version of the java source for cardKt that was used here: cardKt.tar.gz  This code was designed and used on a GemPlus smart card reader, but the prover code is a separate package (KtSeq2k.java, IKtSeq2k.java) and may be used as a library as such.



A paper describing the theorem prover and motivations behind the construction as well as experimental results are available. 

CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security, Rajeev Goré, and Lan Duy Nguyen. In Proceedings Java Card Workshop, Cannes, September 2000, 15 pages. To appear LNCS Springer.
 

Abstract:
  We describe an implementation of a Java program to perform automated deduction in propositional multi-modal logics on a Java smart card. The tight space limits of Java smart cards make the implementation non-trivial. A potential application is to ensure that applets down-loaded off the internet conform to personalised security permissions stored on the Java card using a security policy encoded in multi-modal logic. In particular, modal logic may be useful to ensure that previously checked ``trust'' relationships between pre-existing multiple applets on a Java card are not broken by the addition of a new applet. That is, by using multi-modal logic to express notions of permissions and obligations, we can turn the security check into an on-board theorem proving task. Our theorem prover itself could be down-loaded ``just in time'' to perform the check, and then deleted to free up space on the card once the check has been completed. Our work is thus a ``proof of principle'' for the application of formal logic to the security of multi-application Java cards.
The paper is available in postscript as cardkt.ps.gz  (932Kb). Copyright Springer.


Related Links:
The cardTAP Home Page
The cardKt Home Page
The cardS4 Home Page
The leanTAP Home Page
Sun Java Card
Gemplus Smart Cards
Cyberflex Smart Cards
Java Card Forum - Home page
Defensive Java Virtual Machine Announcement
Java Semantics
Java Card: sémantique, optimisations et sécurité


Email rpg@arp.anu.edu.au  with questions queries or comments.