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: |
|---|---|---|
| RMA-2 | ⊦ eqd(sys, cdom(co), sys0) ∧ (contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) ∨ contents(exec(sys0, co) .1, nam) ≠ contents(sys0, nam)) → contents(exec(sys, co) .1, nam) = contents(exec(sys0, co) .1, nam) | An Axiom |
| 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-3 | ⊦ contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) → nam ∈ alter(cdom(co)) | An Axiom |
| policy-respects-observe | ⊦ d ⇒ d0 → observe(d) ⊆ observe(d0) | An Axiom |
| alter-observe-respects-policy | ⊦ nam ∈ alter(d) ∧ nam ∈ observe(d0) → d ⇒ d0 | An Axiom |
| execl | ⊦ execl(cl) = run(initialstate, cl) | An Axiom |
| run-rec | ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl) | An Axiom |
| run-base | ⊦ run(sys, []) = sys | An Axiom |
| step | ⊦ step(sys, co) = exec(sys, co) .1 | An Axiom |
| test | ⊦ test(cl, co) = exec(execl(cl), co) .2 | An Axiom |
| purge-rec | ⊦ purge(sys, co ' + cl, d) = ((cdom(co) ⇒ d ⊃ co + purge(exec(sys, co) .1, cl, d); purge(sys, cl, d))) | An Axiom |
| purge-base | ⊦ purge(sys, [], d) = [] | An Axiom |
| RMA-2-weaker | ⊦ 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-2-implies-RMA-2-weaker | eqd(sys, cdom(co), sys0) ∧ (contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) ∨ contents(exec(sys0, co) .1, nam) ≠ contents(sys0, nam)) → contents(exec(sys, co) .1, nam) = contents(exec(sys0, co) .1, nam) ⊦ 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) | A User Theorem |
| Security | ⊦ test(cl, co) = test(purge(initialstate, 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 |
| lemma1 | ⊦ eqd(execl(cl), d, execl(purge(initialstate, cl, d))) | A User Theorem |
| lemma1-gen | ⊦ eqd(sys, d, sys0) → eqd(run(sys, cl), d, run(sys0, purge(sys0, cl, d))) | A User Theorem |