Verified Formal Security Models for Multiapplicative Smart Cards

G. Schellhorn, W. Reif, A. Schairer, P. Karger, V. Austel, D. Toll

We present two generic formal security models for operating systems of multiapplicative smart cards. The models formalize the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applications. The first model is as abstract as possible, whereas the second extends the first by adding practically relevant issues such as a structured file system. The models satisfy a common security policy consisting of authentication and intransitive noninterference. The policy extends the classical security policy of Bell/LaPadula and Biba models, but avoids the need for trusted processes that are allowed to circumvent the security policy. Instead trusted processes are incorporated directly in the model itself and are subject to the security policy. The security policy has been formally proven to be correct for both models.
published 2002 Journal for Computer Security, vol. 10, no. 4, p. 339 - 367, 2002