Compositional verification for secure loading of smart card applets

Christoph Sprenger, Dilian Gurov, Marieke Huisman

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

6 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publication2nd ACM IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 23-25 June 2004, San Diego, California, USA, Proceedings
PublisherIEEE Computer Society Press
Pages211-222
Number of pages12
ISBN (Print)0-7803-8509-8
DOIs
Publication statusPublished - 2004
Externally publishedYes
Event2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2004 - San Diego, United States
Duration: 23 Jun 200425 Jun 2004
Conference number: 2

Conference

Conference2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2004
Abbreviated titleMEMOCODE 2004
CountryUnited States
CitySan Diego
Period23/06/0425/06/04

Fingerprint

Dive into the research topics of 'Compositional verification for secure loading of smart card applets'. Together they form a unique fingerprint.

Cite this