Outline for April 10, 2013
Reading: [Bis96] (This is available in the Resources area of SmartSite; look in the folder “Handouts”)
Due: Homework #1, due April 12, 2013
- Conspiracy
- Access set
- Deletion set
- Conspiracy graph
- I, T sets
- Theorem: can•share(α, x, y, G_{0}) iff there is a path from some h(p) ∈ I(x) to some h(q) ∈ T(y)
- de facto rules
- Explicit edges
- Implicit edges
- Pass
- Post
- Spy
- Find
- Paths and spans
- rw-path, rwtg-path
- rw-initial span
- rw-terminal span
- Connection
- Information flow from x to y
- Definition: can•know(x, y, G_{0}) true iff there exists a sequence of protection graphs G_{0}, …, G_{n} such that G_{0} |–^{*} G_{n} using the de jure and de facto rules and in G_{n}, there is an edge from x to y labeled r or an edge from y to x labeled w, and if the edge is explicit, its source is a subject
- Theorem: can•know(r, x, y, G_{0}) iff there is a sequence of subjects u_{1}, …, u_{n}, n ≥ 1, in G_{0}, such that the following hold:
- u_{1} = x or u_{1} rw-terminally spans to x;
- u_{n} = y or u_{n} rw-terminally spans to y; and
- for all i such that 1 ≤ i < n, there is an rwtg-path between u_{i} and u_{i+1} with associated word in B ∪ C.
- Snooping
- Definition: can•snoop(r, x, y, G_{0}) true iff can•steal(r, x, y, G_{0}) or there exists a sequence of graphs and rule applications G_{0} |–_{ρ1} … |–_{ρn} G_{n} for which all the following conditions hold:
- there is no explicit edge from x to y labeled r in G_{0};
- there is an implicit edge from x to y labeled r in G_{n}; and
- neither y nor any vertex directly connected to y in G_{0} is an actor in a grant rule or a de facto rule resulting in an (explicit or implicit) read edge with y as its target
- Example
- Theorem: For distinct vertices x and y in a protection graph G_{0} with explicit edges only, can•snoop(x, y, G_{0}) iff can•steal(r, x, y, G_{0}) or the following hold simultaneously:
- there is no edge from x to y labeled r in G_{0}.
- there is a subject x′ such that x′ = x or x′ rw-initially spans to x in G_{0};
- there is a subject vertex y′ such that y′ ≠ y, there is no edge labeled r from y′ to y in G_{0}, and y′ rw-terminally spans to y in G_{0}; and
- can•know(x′, y′, G_{0}) holds.