section‹Study on knowledge equivalence --- results to relate the knowledge of an agent to that of another's› theory Knowledge imports NS_Public_Bad_GA begin (*Protocol independent study*) (*Whatever A knows, which is neither static-private nor dynamic-private for her, then also B knows that*) theorem knowledge_equiv: "⟦ X ∈ knows A evs; Notes A X ∉ set evs; X ∉ {Key (priEK A), Key (priSK A), Key (shrK A)} ⟧ ⟹ X ∈ knows B evs" apply (erule rev_mp, erule rev_mp, erule rev_mp) apply (induct_tac "A", induct_tac "B", induct_tac "evs") apply (induct_tac [2] "a") apply auto done lemma knowledge_equiv_bis: "⟦ X ∈ knows A evs; Notes A X ∉ set evs ⟧ ⟹ X ∈ {Key (priEK A), Key (priSK A), Key (shrK A)} ∪ knows B evs" apply (blast dest: knowledge_equiv) done lemma knowledge_equiv_ter: "⟦ X ∈ knows A evs; X ∉ {Key (priEK A), Key (priSK A), Key (shrK A)} ⟧ ⟹ X ∈ knows B evs ∨ Notes A X ∈ set evs" apply (blast dest: knowledge_equiv) done lemma knowledge_equiv_quater: " X ∈ knows A evs ⟹ X ∈ knows B evs ∨ Notes A X ∈ set evs ∨ X ∈ {Key (priEK A), Key (priSK A), Key (shrK A)}" apply (blast dest: knowledge_equiv) done lemma setdiff_diff_insert: "A-B-C=D-E-F ⟹ insert m (A-B-C) = insert m (D-E-F)" by simp (*IMPORTANT NOTE TO PREVIOUS LEMMA: removing parentheses from rhs falsifies the lemma because set insertion seems to have higher priority than set difference, hence insert m A-B-C ≠ insert m (A-B-C)! Seen such operand priority, it can be understood why the lemma wouldn't hold without parentheses*) lemma "A-B-C=D-E-F ⟹ insert m A-B-C = insert m D-E-F" oops lemma knowledge_equiv_eq_setdiff: "knows A evs - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X ∈ set evs} = knows B evs - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X ∈ set evs}" apply (induct_tac "evs", induct_tac "A", induct_tac "B") apply force apply (induct_tac "a") (*Gets case solves because this event doesn't touch any agent knowledge*) apply simp_all (*Says case fails because both agents extract the said message, plus discussion on lemma setdiff_diff_insert*) (*Notes case solves in case neither of the two agents is the agent of the current step, because no notes are extracted and inductive premise applies; it fails in the two subcases when either of them is the agent of the current step, because a note would be extracted i.e. inserted in his knowledge, and hence falsification by discussion on lemma setdiff_diff_insert*) oops (*So we have clear counterexamples of why this theorem CANNOT be proved inductively. Alternative stretegy using symbolic evaluation introduces clear counterexamples such as when an agent says A's shared key: it would be in the rhs but not in the lhs!*) (* Old proof*) lemma knowledge_equiv_eq_old: "knows A evs ∪ {Key (priEK B), Key (priSK B), Key (shrK B)} ∪ {X. Notes B X ∈ set evs} = knows B evs ∪ {Key (priEK A), Key (priSK A), Key (shrK A)} ∪ {X. Notes A X ∈ set evs}" apply (induct_tac "evs", induct_tac "A", induct_tac "B") apply force apply (induct_tac "a") txt‹Gets case solves because this event doesn't touch any agent knowledge› apply simp_all apply safe txt‹speeds up subsequent blasting› apply blast+ txt‹very very slow› done (* New proof*) theorem knowledge_eval: "knows A evs = {Key (priEK A), Key (priSK A), Key (shrK A)} ∪ (Key ` range pubEK) ∪ (Key ` range pubSK) ∪ {X. ∃ S R. Says S R X ∈ set evs} ∪ {X. Notes A X ∈ set evs}" apply (induct_tac "A", induct_tac "evs") apply (induct_tac [2] "a") apply auto done lemma knowledge_eval_setdiff: "knows A evs - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X ∈ set evs} = (Key ` range pubEK) ∪ (Key ` range pubSK) ∪ {X. ∃ S R. Says S R X ∈ set evs}" apply (simp only: knowledge_eval) apply auto oops(*here are clear counterexamples!*) theorem knowledge_equiv_eq: "knows A evs ∪ {Key (priEK B), Key (priSK B), Key (shrK B)} ∪ {X. Notes B X ∈ set evs} = knows B evs ∪ {Key (priEK A), Key (priSK A), Key (shrK A)} ∪ {X. Notes A X ∈ set evs}" apply (force simp only: knowledge_eval) done lemma "knows A evs ∪ {Key (priEK B), Key (priSK B), Key (shrK B)} ∪ {X. Notes B X ∈ set evs} - ( {Key (priEK B), Key (priSK B), Key (shrK B)} ∪ {X. Notes B X ∈ set evs} ) = knows A evs" apply auto oops (*Here the prover tells you why this fails*) theorem parts_knowledge_equiv_eq: " parts(knows A evs) ∪ {Key (priEK B), Key (priSK B), Key (shrK B)} ∪ parts({X. Notes B X ∈ set evs}) = parts(knows B evs) ∪ {Key (priEK A), Key (priSK A), Key (shrK A)} ∪ parts({X. Notes A X ∈ set evs})" apply (simp only: knowledge_eval parts_Un) apply force done lemmas parts_knowledge_equiv = parts_knowledge_equiv_eq [THEN equalityD1, THEN subsetD] thm parts_knowledge_equiv theorem noprishr_parts_knowledge_equiv: " ⟦ X ∉ {Key (priEK A), Key (priSK A), Key (shrK A)}; X ∈ parts(knows A evs) ⟧ ⟹ X ∈ parts(knows B evs) ∪ parts({X. Notes A X ∈ set evs})" apply (force dest: UnI1 [THEN UnI1, THEN parts_knowledge_equiv]) done (*Protocol-dependent study*) lemma knowledge_equiv_eq_NS: " evs ∈ ns_public ⟹ knows A evs ∪ {Key (priEK B), Key (priSK B), Key (shrK B)} = knows B evs ∪ {Key (priEK A), Key (priSK A), Key (shrK A)}" apply (force simp only: knowledge_eval NS_no_Notes) done lemma parts_knowledge_equiv_eq_NS: " evs ∈ ns_public ⟹ parts(knows A evs) ∪ {Key (priEK B), Key (priSK B), Key (shrK B)} = parts(knows B evs) ∪ {Key (priEK A), Key (priSK A), Key (shrK A)}" apply (simp only: knowledge_eval NS_no_Notes parts_Un) apply force done theorem noprishr_parts_knowledge_equiv_NS: " ⟦ X ∉ {Key (priEK A), Key (priSK A), Key (shrK A)}; X ∈ parts(knows A evs); evs ∈ ns_public ⟧ ⟹ X ∈ parts(knows B evs)" apply (drule noprishr_parts_knowledge_equiv, simp) apply (simp add: NS_no_Notes) done theorem Agent_not_analz_N: "⟦ Nonce N ∉ parts(knows A evs); evs ∈ ns_public ⟧ ⟹ Nonce N ∉ analz(knows B evs)" apply (force intro: noprishr_parts_knowledge_equiv_NS analz_into_parts) done (*Conclusion in terms of analz because we are more used to it. It would have been a stronger law in terms of parts, though*) end