|
Abstract : |
The paper describes the status of a joint project between Gemplus and ONERA. Gemplus developed an electronic purse running on Java enabled smart cards. The project goal is to verify security properties that should be enforced by the applets involved in this application. A security policy has been de ned that associates levels to applet attributes and methods and de nes authorized ows between levels. We propose a technique based on model checking to verify that actual information ows between applets are authorized. 1 Context and case study 1.1 Open smart cards A new type of smart cards is getting more and more attractive: multiapplication smart cards. The main characteristics of such cards are that applications can be loaded after the card issuance and that several applications run on the same card. A few operating systems have been proposed to manage multiapplication, |
