# 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

1. Conspiracy
1. Access set
2. Deletion set
3. Conspiracy graph
4. I, T sets
5. Theorem: can•share(α, x, y, G0) iff there is a path from some h(p) ∈ I(x) to some h(q) ∈ T(y)
2. de facto rules
1. Explicit edges
2. Implicit edges
1. Pass
2. Post
3. Spy
4. Find
3. Paths and spans
1. rw-path, rwtg-path
2. rw-initial span
3. rw-terminal span
4. Connection
4. Information flow from x to y
1. Definition: can•know(x, y, G0) true iff there exists a sequence of protection graphs G0, …, Gn such that G0 |–* Gn using the de jure and de facto rules and in Gn, 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
2. Theorem: can•know(r, x, y, G0) iff there is a sequence of subjects u1, …, un, n ≥ 1, in G0, such that the following hold:
1. u1 = x or u1 rw-terminally spans to x;
2. un = y or un rw-terminally spans to y; and
3. for all i such that 1 ≤ i < n, there is an rwtg-path between ui and ui+1 with associated word in BC.
5. Snooping
1. Definition: can•snoop(r, x, y, G0) true iff can•steal(r, x, y, G0) or there exists a sequence of graphs and rule applications G0 |–ρ1 … |–ρn Gn for which all the following conditions hold:
1. there is no explicit edge from x to y labeled r in G0;
2. there is an implicit edge from x to y labeled r in Gn; and
3. neither y nor any vertex directly connected to y in G0 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
2. Example
3. Theorem: For distinct vertices x and y in a protection graph G0 with explicit edges only, can•snoop(x, y, G0) iff can•steal(r, x, y, G0) or the following hold simultaneously:
1. there is no edge from x to y labeled r in G0.
2. there is a subject x′ such that x′ = x or x′ rw-initially spans to x in G0;
3. there is a subject vertex y′ such that y′y, there is no edge labeled r from y′ to y in G0, and y′ rw-terminally spans to y in G0; and
4. can•know(x′, y′, G0) holds.

 You can also obtain a PDF version of this. Version of April 9, 2013 at 9:12PM