Checking Absence of Illicit Applet Interactions: A Case Study

Abstract. This paper presents the use of a method – and its corresponding tool set – for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by m...

• Type: Conference
• Year: 2004
• Where: FASE
• Authors: Marieke Huisman, Dilian Gurov, Christoph Sprenger, Gennady Chugunov
• Keywords: Case Study, FASE 2004, Smart Card Case, Smart Cards, Software Engineering