This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| eqd-def | ⊦ eqd(sys, d, sys0) ↔ (∀ nam. nam ∈ observe(d) → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| RMA-1 | ⊦ eqd(sys, cdom(co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2 | An Axiom |
| RMA-2 | ⊦ eqd(sys, cdom(co), sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ nam ∈ alter(cdom(co)) → contents(exec(sys, co) .1, nam) = contents(exec(sys0, co) .1, nam) | An Axiom |
| RMA-3 | ⊦ contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) → nam ∈ alter(cdom(co)) | An Axiom |
| alter-observe-respects-policy | ⊦ nam ∈ alter(d) ∧ nam ∈ observe(d0) → d ⇒ d0 | An Axiom |
| test | ⊦ test(cl, co) = exec(execl(cl), co) .2 | An Axiom |
| step | ⊦ step(sys, co) = exec(sys, co) .1 | An Axiom |
| run-base | ⊦ run(sys, []) = sys | An Axiom |
| run-rec | ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl) | An Axiom |
| execl | ⊦ execl(cl) = run(initialstate, cl) | An Axiom |
| sources-base | ⊦ sources([], d) = ∅ ++ d | An Axiom |
| sources-rec | ⊦ sources(co ' + cl, d) = (((∃ d0. d0 ∈ sources(cl, d) ∧ cdom(co) ⇒ d0) ⊃ sources(cl, d) ++ cdom(co); sources(cl, d))) | An Axiom |
| ipurge-base | ⊦ ipurge([], d) = [] | An Axiom |
| ipurge-rec | ⊦ ipurge(co ' + cl, d) = ((cdom(co) ∈ sources(co + cl, d) ⊃ co + ipurge(cl, d); ipurge(cl, d))) | An Axiom |
| eqds-def | ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0)) | An Axiom |
| Security | ⊦ test(cl, co) = test(ipurge(cl, cdom(co)), co) | A User Theorem |
| eqd-reflexivity | ⊦ eqd(sys, d, sys) | A User Theorem |
| eqd-symmetry | ⊦ eqd(sys, d, sys0) → eqd(sys0, d, sys) | A User Theorem |
| eqd-transitivity | ⊦ eqd(sys, d, sys0) ∧ eqd(sys0, d, sys1) → eqd(sys, d, sys1) | A User Theorem |
| eqds-refl | ⊦ eqds(sys, ds, sys) | A User Theorem |
| eqds-symm | ⊦ eqds(sys, ds, sys0) → eqds(sys0, ds, sys) | A User Theorem |
| eqds-trans | ⊦ eqds(sys, ds, sys0) ∧ eqds(sys0, ds, sys1) → eqds(sys, ds, sys1) | A User Theorem |
| lemma2 | ⊦ eqd(execl(cl), d, execl(ipurge(cl, d))) | A User Theorem |
| lemma3 | ⊦ eqds(sys, sources(co + cl, d), sys0) → eqds(exec(sys, co) .1, sources(cl, d), exec(sys0, co) .1) | A User Theorem |
| lemma4 | ¬ cdom(co) ∈ sources(co ' + cl, d) ⊦ eqds(sys, sources(cl, d), exec(sys, co) .1) | A User Theorem |
| lemma5 | eqds(sys, sources(cl, d), sys0) ⊦ eqd(run(sys, cl), d, run(sys0, ipurge(cl, d))) | A User Theorem |
| locally-respects | ⊦ ¬ cdom(co) ⇒ d0 → eqd(sys, d0, exec(sys, co) .1) | A User Theorem |
| sources-1 | ⊦ d ∈ sources(cl, d) | A User Theorem |
| weakly-step-consistent | ⊦ eqd(sys, d, sys0) ∧ eqd(sys, cdom(co), sys0) → eqd(exec(sys, co) .1, d, exec(sys0, co) .1) | A User Theorem |