@InProceedings{ sprenger.ea:compositional:2004, 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. }, author = {Christoph Sprenger and Dilian Gurov and Marieke Huisman}, booktitle = {Formal Methods and Models for Co-Design (MEMOCODE)}, copyright = {\copyright IEEE Computer Society}, copyrighturl = {http://www.computer.org/publications}, language = {USenglish}, pages = {211--222}, publisher = {IEEE Computer Society}, title = {Compositional Verification for Secure Loading of Smart Card Applets}, year = 2004, user = {csprenge} }