Abstract:

Compositional Verification for Secure Loading of Smart Card Applets

Christoph Sprenger and Dilian Gurov and Marieke Huisman


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 f
low 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.