Checking Secure Interactions of Smart Card Applets: Extended Version

Abstract. This paper presents an approach enabling a smart card issuer to verify that a new applet securely interacts with already downloaded applets. 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. We illustrate our approach on applets involved in an electronic purse running on Java enabled smart cards.

• Type: Journal
• Year: 2002
• Where: JCS
• Authors: Pierre Bieber, Jacques Cazin, Pierre Girard, Jean-Louis Lanet, Virginie Wiels, Guy Zanon
• Keywords: Applets, JCS 2002, Smart Card Issuer, Smart Cards