Basic Security Theorem, Step 2

•      If a system is initially in a secure state, and every transition of the system satisfies the simple security condition, step 2, and the *-property, step 2, then every state of the system is secure

–    Proof: induct on the number of transitions

–    In actual Basic Security Theorem, discretionary access control treated as third property, and simple security property and *-property phrased to eliminate discretionary part of the definitions — but simpler to express the way done here.

Problem

•      Colonel has (Secret, {NUC, EUR}) clearance

•      Major has (Secret, {EUR}) clearance

–   Major can talk to colonel (“write up” or “read down”)

–   Colonel cannot talk to major (“read up” or “write down”)

•      Clearly absurd!

Solution

•      Define maximum, current levels for subjects

–    maxlevel(s) dom curlevel(s)

•      Example

–    Treat Major as an object (Colonel is writing to him/her)

–    Colonel has maxlevel (Secret, { NUC, EUR })

–    Colonel sets curlevel to (Secret, { EUR })

–    Now L(Major) dom curlevel(Colonel)

•    Colonel can write to Major without violating “no writes down”

–    Does L(s) mean curlevel(s) or maxlevel(s)?

•    Formally, we need a more precise notation