Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Compositional verification for secure loading of smart card applets
KTH, Superseded Departments, Microelectronics and Information Technology, IMIT.ORCID iD: 0000-0002-0074-8786
2004 (English)In: SECOND ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2004, 211-222 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present an algorithmic compositional verification method for smart card applets and control flow based safety properties expressed in a modal logic with simultaneous greatest fixed points. Our method builds on a technique proposed by Grumberg and Long who use maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We adapt this technique to applets, a class of infinite-state sequential processes. This requires a refinement of the method, since for a given applet interface and behavioural formula a maximal applet does not always exist. We therefore propose a two-level approach, where local assumptions restrict the control flow structure of applets, while the global guarantee restricts the control flow behaviour of the system. We present a novel maximal model construction for our logic and then adapt it to applets. By separating the tasks of verifying global and local properties our method supports secure post-issuance loading of applets onto a smart card.

Place, publisher, year, edition, pages
2004. 211-222 p.
Keyword [en]
MODEL CHECKING
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-50779ISI: 000229217000028Scopus ID: 2-s2.0-28344456357OAI: oai:DiVA.org:kth-50779DiVA: diva2:462671
Conference
2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design. San Diego, CA. JUN 22-25, 2004
Note
QC 20111208Available from: 2011-12-07 Created: 2011-12-07 Last updated: 2011-12-09Bibliographically approved

Open Access in DiVA

No full text

Scopus

Authority records BETA

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Microelectronics and Information Technology, IMIT
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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