Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Model checking of multi-applet JavaCard applications
RISE, Swedish ICT, SICS.
RISE, Swedish ICT, SICS.
RISE, Swedish ICT, SICS.
2002 (English)Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
2002, 1.
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:ri:diva-22509OAI: oai:DiVA.org:ri-22509DiVA, id: diva2:1042074
Conference
IFIP/USENIX conference CARDIS'02, the 5th Smart Card Research and Advanced Application Conference, 20-22 Nov 2002, San José, California, USA
Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2020-12-02Bibliographically approved

Open Access in DiVA

No full text in DiVA

By organisation
SICS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 33 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf