Model checking of multi-applet JavaCard applications

Chugunov, Gennady and Fredlund, Lars-Åke and Gurov, Dilian (2002) Model checking of multi-applet JavaCard applications. In: IFIP/USENIX conference CARDIS'02, the 5th Smart Card Research and Advanced Application Conference, 20-22 Nov 2002, San José, California, USA.

Full text not available from this repository.


The paper describes a framework for model checking JavaCard applets on the bytecode level. >From a set of JavaCard applets we extract their method call graphs using a static analysis tool. The resulting structure is translated into a pushdown system for which the model checking problem for Linear Temporal Logic (LTL) is decidable, and for which there are efficient model checking tools available. The model checking approach of the paper is tailored to the analysis of inter applet (intra card) communications and we demonstrate its effectiveness using a prototypical example of a purse applet and a set of loyalty applets.

Item Type:Conference or Workshop Item (Paper)
ID Code:2932
Deposited On:11 Jul 2008
Last Modified:18 Nov 2009 16:16

Repository Staff Only: item control page