cardS4 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, cardS4 code, and a list of links related to smart cards and verification.
Here is a web interface to the cardS4 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.
Notes on syntax: Formulae must be in negated normal form (NNF) where all negation symbols are pushed in to the propositional atoms. AND : &, OR : |, ALL : , SOME : <>, NEGATION : ~. Propositions must start with capital letters. True is 1, there is no false (must be supplied as ~1). All other characters are ignored.
Source for both the web and card version are available here: cardS4source.tar.gz. The java_cup libraries are used by this project.
CardS4: Modal Theorem Proving on Java Smartcards. To appear LNCS Springer.
We describe a successful implementation of a theorem prover for modal logic S4 that runs on a Java smart card with only 512 KBytes of RAM and 32KBytes of EEPROM. Since proof search in S4 can lead to infinite branches, this is ``proof of principle'' that non-trivial modal deduction is feasible even on current Java cards. We hope to use this prover as the basis of an on-board security manager for restricting the flow of ``secrets'' between multiple applets residing on the same card, although much work needs to be done to design the appropriate modal logics of ``permission'' and ``obligations''. Such security concerns are the major impediments to the commercial deployment of multi-application smart cards.The paper is available in postscript as cards4-esmart01.ps.gz. Copyright Springer.
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 Card: sémantique, optimisations et sécurité
Email firstname.lastname@example.org with questions queries or comments.