cardTAP : The First Theorem Prover on a Smart Card

cardTAP is a 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 reports on the research done, cardTAP code, and a list of links related to smart cards and verification.

This is the web version of cardTAP is here.   It requires that your browser fully support Java Version 1.1.  Enter formulae in Negated Normal Form (NNF), Reverse Polish Notation (RPN). Use "+" for logical OR, "&" for logical AND, and "-" for negation. The lowercase letters "a" to "z" can be used as variables. Currently no informative syntax checking or normal form conversion is properly supported. 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 cardTAP that is used for this web page here: wcardtap.tar.gz

Some papers describing the theorem prover and motivations behind the construction as well as experimental results are available.  The following is an abstract from one of these papers.

  We present the first implementation of a theorem prover which runs on a smart card. The prover is written in Java and implements a dual tableau calculus. Due to the limited resources available on current smart cards, the prover is restricted to propositional classical logic. It can be easily extended to full first-order logic.
The potential applications for our prover lie within the context of security related functions based on trusted devices such as smart cards.
 The system description presented at CADE-15 is available in postscript as  (33Kb) and in dvi format as cTAPCADE.dvi.gz (7 Kb). Copyright Springer.

An extended version of the paper will be presented at AI98 and is available as  (66 Kb). 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  with questions queries or comments.