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 {parent:Object,
                    location: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 origin(s) = (s matches 'scheme://hostpart') || 'unknown origin'.

Let fake(s) = (s matches 'about:' || s matches 'data:' || s.matches('javascript:').

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

Let w.open(s) = new Window(null, s, fake(s) ? stack.top() : origin(s), w).