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