CardS4: modal theorem proving on Java smart cards

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 32 KBytes 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.