Résumé de séminaire

Résumé :

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 personalised 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.