CardKt: Automated multi-modal deduction on Java cards for multi-application security. 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
References in zbMATH (referenced in 1 article , 1 standard article )
Showing result 1 of 1.
- Goré, Rajeev; Lan Duy Nguyen: CardKt: Automated multi-modal deduction on Java cards for multi-application security (2001)