Verification of a Formal Security Model for Multiapplicative Smart Cards

  • Schellhorn G
  • Reif W
  • Schairer A
 et al. 
  • 23


    Mendeley users who have this article in their library.
  • 37


    Citations of this article.


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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Gerhard Schellhorn

  • Wolfgang Reif

  • Axel Schairer

  • Paul Karger

  • Vernon Austel

  • David Toll

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free