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 [Activation]          // array of activation objects
Activation = record {global:Window,
                     subject: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.

Functions:

Let origin(s) = (s matches 'scheme://hostpart') || 'unknown origin'.

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

Let global() = stack.top().global

Let subject() = stack.top().subject

Let open(s) = new Window(null, s, fake(s) ? subject() : origin(s), global()).

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

Let access(o) = principal(o) <= (stack[0] ^ ... ^ stack.top()).