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
Stack     = array [Principal]           // array of Principal
Object    = record {parent:Object}      // record with parent field
Window    = record {url:String,
                    principal:Principal,
                    opener:Window,
                    document:Object}

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.

Let principal(x) = (x is Window) ? x.principal : (x is Object) ? principal(x.parent) : origin(x)

Let open(u) = new Window(u, principal(u), window)