CardS4: Modal Theorem Proving on Java Smartcards
Rajeev Goré and Phuong Thê Nguyên

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.

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


Source for both the web and card version are available here: cardS4source.tar.gz. The java_cup libraries are used by this project.



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

CardS4: Modal Theorem Proving on Java Smartcards. To appear LNCS Springer.

Abstract:
  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.


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.