Verifying smart card applications An ASM approach

We present PROSECCO1, a formal model for security protocols of smart card applications, based on Abstract State Machines (ASM) [BS03]JGur95], and a suitable method for verifying security properties of such protocols. The main part of this article describes the structure of the protocol ASM and all its relevant parts. Our modeling technique enables an attacker model exactly tailored to the application, instead of only an attacker similar to the Dolev-Yao model. We also introduce a proof technique for security properties of the protocols. Properties are proved in the KIV system using symbolic execution and invariants. Furthermore we describe a graphical notation based on UML diagrams that allows to specify the important parts of the application in a simple way. Our formal approach is exemplified with a small e-commerce application. We use an electronic wallet to demonstrate the ASM-based protocol model and we also show what the proof obligations of some of the security properties look like.