Security:Strawman Model

Types:

Principal = (System, Origin, Null)    // disjoint type union
System    = {system}                  // system principal singleton
Origin    = {origin1, ... originN}    // set of N origin principals
Null      = {null}                    // null principal singleton

Definitions:

Let P be the set of all principals.

Let <= be a binary relation by which P is partially ordered.

For all p in P, p <= system.

For all Origin principals p and q in P, !(p <= q) && !(q <= p).

For all p in P, unknown <= p.

For all principals p and q, there exists in P the greatest lower bound (p ^ q), the meet of p and q, defined by <=. (P, <=) is a meet semi-lattice.

For all p in P, (p ^ system) == p.

For all p in P, (p ^ null) == null.