Checking Absence of Illicit Applet Interactions: A Case Study

Marieke Huisman, Dilian Gurov, Christoph Sprenger, Gennady Chugunov

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

21 Citations (Scopus)

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 means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings
EditorsMichel Wermelinger, Tiziana Margaria
PublisherSpringer Singapore
Pages84-98
Number of pages15
DOIs
Publication statusPublished - 2004
Externally publishedYes
Event7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004 - Barcelona, Spain
Duration: 29 Mar 20042 Apr 2004
Conference number: 7

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2984

Conference

Conference7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004
Abbreviated titleFASE 2004
CountrySpain
CityBarcelona
Period29/03/042/04/04
OtherHeld as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004

Fingerprint Dive into the research topics of 'Checking Absence of Illicit Applet Interactions: A Case Study'. Together they form a unique fingerprint.

Cite this