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 |
| purge-base | ⊦ purge([], d) = [] | An Axiom |
| purge-rec | ⊦ purge(co ' + cl, d) = ((cdom(co) ⇒ d ⊃ co + purge(cl, d); purge(cl, d))) | An Axiom |
| LanguageBasedNIF-follows | obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| Security | ⊦ purge(cl, d) = purge(cl0, d) → obs(run(cl), d) = obs(run(cl0), d) | A Proof Obligation |
| Security-simple | ⊦ obs(run(cl), d) = obs(run(purge(cl, d)), d) | 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 |
| Security-without-initialstate | ⊦ purge(cl, d) = purge(cl0, d) ∧ eqd(sys, d, sys0) → obs(run(sys, cl), d) = obs(run(sys0, cl0), d) | A Proof Obligation |
| Security-simple-without-initialstate | ⊦ obs(run(sys, cl), d) = obs(run(sys, purge(cl, d)), d) | A Proof Obligation |
| LanguageBasedNIF-run | eqd(sys, d, sys0) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(run(sys, cl), nam) = contents(run(sys0, cl), nam) | A Proof Obligation |
| eqd-reflexivity | ⊦ eqd(sys, d, sys) | A User Theorem |
| eqd-run-lemma | ⊦ eqd(sys, d, sys0) → eqd(run(sys, cl), d, run(sys0, cl)) | 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(run(cl), d, run(purge(cl, d))) | A User Theorem |
| lemma1-gen | ⊦ eqd(sys, d, sys0) → eqd(run(sys, cl), d, run(sys0, purge(cl, d))) | A User Theorem |
| observe-names | ⊦ usedName(nam) → observe(nam, cdom(nam)) | A User Theorem |
| purge-idempotent | ⊦ purge(purge(cl, d), d) = purge(cl, d) | A User Theorem |
| step-eqd | ⊦ cdom(co) ⇒ d ∧ eqd(sys, d, sys0) → eqd(step(sys, co), d, step(sys0, co)) | A User Theorem |
| step1-eqd | ⊦ ¬ cdom(co) ⇒ d ∧ eqd(sys, d, sys0) → eqd(step(sys, co), d, sys0) | A User Theorem |