6th European Symposium on Research in Computer Security (ESORICS 2000)
Verification of a Formal Security Model for Multiapplicative Smart Cards
Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul Karger, Vernon Austel, David Toll
Keywords :
Abstract : We present a generic formal security model for operating systems of multiapplicative smart cards. The model formalizes the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applications. The model satisfies a security policy consisting of authentication and intransitive noninterference. The model extends the classical security models of Bell/LaPadula and Biba, but avoids the need for trusted processes, which are not subject to the security policy by incorporating such processes directly in the model itself. The correctness of the security policy has been formally proven with the VSE II system.
(Pages 17-36)