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