Verified Formal Security Models for Multiapplicative Smart Cards

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 ally abstract, 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.

• Type: Journal
• Year: 2002
• Where: JCS
• Authors: Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll
• Keywords: Common Security Policy, Formal Security Models, JCS 2002, Security Policy