Electronic Purse Applet Certification

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 defined that associates levels to applet attributes and methods and defines authorized flows between levels. We propose a technique based on model checking to verify that actual information flows between applets are authorized.