More on the Ideal

• Is it too big? No. Necessity follows because

  • exposing {X, Y} exposes both X and Y, and
  • exposing {X}K exposes X if the inverse of K is not protected.

• The tricky part is identifying a big enough S so that the invariant holds.

• Relation to analz and synth:

  • Theorem (JKM): Let P be the complement of I[k, S] (k as above). Then synth(analz(P)) = P.
  • Proof: follows from

    1. analz(P) = P (by fixpoint induction)
    
    2. synth(P) = P (by structural induction)

Previous slide

Next slide

Back to first slide

View graphic version