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: |
|---|---|---|
| eqds-def | ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0)) | An Axiom |
| 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); ipurge(cl, d))) | An Axiom |
| Security-strong | ⊦ ipurge(cl, d) = ipurge(cl0, d) ∧ eqds(sys, sources(cl, d), sys0) → obs(run(sys, cl), d) = obs(run(sys0, cl0), d) | A Proof Obligation |
| Security | ⊦ ipurge(cl, d) = ipurge(cl0, d) → obs(run(cl), d) = obs(run(cl0), d) | A Proof Obligation |
| Security-simple | ⊦ obs(run(cl), d) = obs(run(ipurge(cl, d)), d) | A Proof Obligation |
| Security-simple-without-initialstate | ⊦ obs(run(sys, cl), d) = obs(run(sys, ipurge(cl, d)), d) | A Proof Obligation |
| LanguageBasedNIF-run-observe | eqds(sys, sources(cl, d), sys0) ⊦ ∀ nam. usedName(nam) ∧ observe(nam, d) → contents(run(sys, cl), nam) = contents(run(sys0, cl), nam) | A Proof Obligation |
| LanguageBasedNIF-run | eqds(sys, sources(cl, d), sys0) ⊦ ∀ nam. usedName(nam) ∧ observe(nam, d) ∧ cdom(nam) ⇒ d → contents(run(sys, cl), nam) = contents(run(sys0, cl), nam) | A Proof Obligation |
| LanguageBasedNIF-follows | obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| eqd-implies-LanguageBasedNIF | eqd(sys, d, sys0) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| LanguageBasedNIF-weaker | obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d ∧ observe(nam, d) → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| 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-sources-ipurge | ⊦ eqds(sys, sources(cl, d), sys0) ↔ eqds(sys, sources(ipurge(cl, d), d), sys0) | A User Theorem |
| eqds-sources-ipurge-01 | ⊦ eqds(sys, sources(ipurge(cl, d), d), sys0) ↔ eqds(sys, sources(cl, d), sys0) | 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 |
| 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 | ⊦ eqds(sys, sources(co + cl, d), 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 | 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, step(sys, co)) | A User Theorem |
| run-eqd | ⊦ eqds(sys, sources(cl, d), sys0) → eqd(run(sys, cl), d, run(sys0, cl)) | 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-consistent | ⊦ eqd(sys, d, sys0) ∧ eqd(sys, cdom(co), sys0) → eqd(step(sys, co), d, step(sys0, co)) | A User Theorem |