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, G₀) 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, G₀) true iff there exists a sequence of protection graphs G₀, …, G_n such that G₀ |–^* 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
   2. Theorem: can•know(r, x, y, G₀) iff there is a sequence of subjects u₁, …, u_n, n ≥ 1, in G₀, such that the following hold:
      1. u₁ = x or u₁ rw-terminally spans to x;
      2. u_n = y or u_n rw-terminally spans to y; and
      3. 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.
5. Snooping
   1. Definition: can•snoop(r, x, y, G₀) true iff can•steal(r, x, y, G₀) or there exists a sequence of graphs and rule applications G₀ |–_ρ1 … |–_ρn G_n for which all the following conditions hold:
      1. there is no explicit edge from x to y labeled r in G₀;
      2. there is an implicit edge from x to y labeled r in G_n; and
      3. neither y nor any vertex directly connected to y in G₀ 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 G₀ with explicit edges only, can•snoop(x, y, G₀) iff can•steal(r, x, y, G₀) or the following hold simultaneously:
      1. there is no edge from x to y labeled r in G₀.
      2. there is a subject x′ such that x′ = x or x′ rw-initially spans to x in G₀;
      3. there is a subject vertex y′ such that y′ ≠ y, there is no edge labeled r from y′ to y in G₀, and y′ rw-terminally spans to y in G₀; and
      4. can•know(x′, y′, G₀) holds.