Theorem Security-strong

⊦ ipurge(cl, d) = ipurge(cl0, d) ∧ eqds(sys, sources(cl, d), sys0) → obs(run(sys, cl), d) = obs(run(sys0, cl0), d)

Type: A proof obligation
Validity: The proof is valid.
Features: theorem,
Comment: This is the standard (generalized) purge security property starting with two different states. Proved with RMA-1 and lemma1-gen. Because of sources-ipurge the eqds precondition is equivalent to eqds(sys, sources(ipurge(cl, d), d), sys0) and eqds(sys, sources(ipurge(cl0, d), d), sys0) and eqds(sys, sources(cl0, d), sys0)
Used by:
Used by units in proved state:
Proof exists?: Yes

View the proof