Theory Knowledge

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