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: |
|---|---|---|
| run-base | ⊦ run(sys, []) = sys | An Axiom |
| run-rec | ⊦ run(sys, co ' + cl) = run(step(sys, co), cl) | An Axiom |
| run-initial | ⊦ run(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); ipurged(co) + ipurge(cl, d))) | An Axiom |
| eqds-def | ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0)) | An Axiom |
| Security | ⊦ ipurge(cl, d) = ipurge(cl0, d) → obs(run(cl), d) = obs(run(cl0), d) | A User Theorem |
| Security-simple | ⊦ obs(run(cl), d) = obs(run(ipurge(cl, d)), d) | 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 |
| eqs-ipurged | ⊦ eqS(sys, step(sys0, ipurged(co))) ↔ eqS(sys, step(sys0, co)) | A User Theorem |
| eqs-reflexivity | ⊦ eqS(sys, sys) | A User Theorem |
| eqs-step | ⊦ eqS(sys, sys0) ∧ eqd(sys, cdom(co), sys0) → eqS(step(sys, co), step(sys0, co)) | A User Theorem |
| ipurge-idempotent | ⊦ ipurge(ipurge(cl, d), d) = ipurge(cl, d) | A User Theorem |
| lemma2 | ⊦ eqd(run(cl), d, run(ipurge(cl, d))) | A User Theorem |
| lemma3-2 | ⊦ eqds(sys, sources(co + cl, d), sys0) ∧ eqS(sys, sys0) → eqds(step(sys, co), sources(cl, d), step(sys0, co)) | A User Theorem |
| lemma4 | ¬ cdom(co) ∈ sources(co ' + cl, d) ⊦ eqds(sys, sources(cl, d), step(sys, co)) | A User Theorem |
| lemma5-2 | ⊦ eqds(sys, sources(cl, d), sys0) ∧ eqS(sys, sys0) → eqd(run(sys, cl), d, run(sys0, ipurge(cl, d))) | A User Theorem |
| locally-respects | ⊦ ¬ cdom(co) ⇒ d0 → eqd(sys, d0, step(sys, co)) | A User Theorem |
| locally-respects2 | ⊦ ¬ cdom(co) ⇒ d0 → eqd(sys, d0, step(sys, ipurged(co))) | A User Theorem |
| sources-1 | ⊦ d ∈ sources(cl, d) | A User Theorem |
| sources-ipurge | ⊦ d0 ∈ sources(ipurge(cl, d), d) ↔ d0 ∈ sources(cl, d) | A User Theorem |
| weakly-step-consistent2 | ⊦ eqd(sys, d, sys0) ∧ eqd(sys, cdom(co), sys0) ∧ eqS(sys, sys0) → eqd(step(sys, co), d, step(sys0, co)) | A User Theorem |