Checking Secure Interactions of Smart Card.pdf

Checking Secure Interactions of Smart Card Applets? P. Bieber1, J. Cazin1, P. Girard2, J.-L. Lanet2, V. Wiels1, G. Zanon1 1 ONERA-CERT/DTIM BP 4025, 2 avenue E. Belin, F-31055 Toulouse Cedex 4, France fbieber,cazin,wiels,zanong@cert.fr 2 GEMPLUS avenue du pic de Bertagne, 13881 Gemenos cedex, France fPierre.GIRARD,Jean-Louis.LANETg@ Abstract. This paper presents an approach enabling a smart card is- suer to verify that a new applet securely interacts with already down- loaded applets. 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. We illustrate our approach on applets involved in an electronic purse running on Java enabled smart cards. Introduction 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 smart cards, namely Java Card 1, Multos 2 and more recently Smart Cards for Windows3. In this paper, we will focus on Java Card. Following this standard, applications for multiapplication smart cards are implemented as interacting Java applets. Multiapplication smart cards involve several participants: the card provider, the card issuer that proposes the card to the users, application providers and card holders (users). The card issuer is usually considered responsible for the security of the card. The card issuer does not trust application providers: applets could be malicious or simply faulty. As in a classical mobile code setting, a malicious downloaded applet could try to observe, alter, use information or resources it is not authorized to. Of course, ? The Pacap project is partially funded by MENRT decision