CardKt: Automated multi-modal deduction on Java cards for multi-application security. (English) Zbl 0980.68975

Attali, Isabelle (ed.) et al., Java on Smart Cards: programming and security. 1st international workshop, JavaCard 2000, Cannes, France, September 14, 2000. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2041, 38-51 (2001).
Summary: 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 personalized 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.
For the entire collection see [Zbl 0968.68557].


68U99 Computing methodologies and applications
68N15 Theory of programming languages
68P25 Data encryption (aspects in computer science)


KtSeqC; CardKt