Logic and Automated Reasoning for Security of Mobile Code

Rajeev Goré

Automated Reasoning Group and Department of Computer Science

Australian Research Council Queen Elizabeth II Fellow

Part 1: (10') brief introduction to my research themes

Part 2: (45') technical talk with abstract below

We describe a successful implementation of a theorem prover for modal logic S4 that runs on a Java smart card with only 512 KBytes if RAM and 32KBytes of EEPROM. We describe how this prover might be used as the basis of an on-board security manager for restricting the flow of ``secrets'' between multiple applets residing on the same card. Such security concerns are the major impediments to the commercial deployment of multi-application smart cards.

The talk is intended for non-specialists.

Part 3: (5') prospects for future research

Back to schedule.