Compositional verification for secure loading of smart card applets
2004 (English)In: SECOND ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2004, 211-222 p.Conference paper (Refereed)
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.
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-50779ISI: 000229217000028ScopusID: 2-s2.0-28344456357OAI: oai:DiVA.org:kth-50779DiVA: diva2:462671
2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design. San Diego, CA. JUN 22-25, 2004
QC 201112082011-12-072011-12-072011-12-09Bibliographically approved