Skip to Main content Skip to Navigation

Simulation Logic, Applets and Compositional Verification

Christoph Sprenger 1 Dilian Gurov Marieke Huisman
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We present a compositional verification method for control flow based safety properties of smart card applets. Our method rests on a close correspondence between transition system models ordered by simulation and Hennessy-Milner logic extended with simultaneous greatest fixed points. We show that simulation can be characterised logically and, vice versa, logical satisfaction can be represented behaviourally by a maximal model for a given formula. Based on these results and earlier ideas by Grumberg and Long we develop a compositional verification technique, where maximal models replace logical assumptions to reduce compositional verification to standard model checking. However, in the context of applets, equipped with interfaces, this technique needs to be refined. Since for a given behavioural formula and interface a maximal applet does not always exist, we propose a two-level approach, where local assumptions restrict the control flow \emph{structure} of applets, while the global property restricts the control flow \emph{behaviour} of the system. By separating the tasks of verifying global and local properties of applets, our method supports secure post-issuance loading of new applets onto a smart card.
Document type :
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:33:02 PM
Last modification on : Saturday, January 27, 2018 - 1:31:25 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:41:55 PM


  • HAL Id : inria-00071692, version 1



Christoph Sprenger, Dilian Gurov, Marieke Huisman. Simulation Logic, Applets and Compositional Verification. RR-4890, INRIA. 2003. ⟨inria-00071692⟩



Record views


Files downloads