Theory ConfidentialityGA

section‹Inductive Study of Confidentiality against the General Attacker›

theory  ConfidentialityGA imports NS_Public_Bad_GA begin

text‹New subsidiary lemmas to reason on a generic agent initial state›

lemma parts_initState: "parts(initState C) = initState C"
by (cases C, simp)

lemma analz_initState: "analz(initState C) = initState C"
by (cases C, force dest: analz_into_parts)


text‹Generalising over all initial secrets the existing treatment, which is limited to private encryption keys›

definition staticSecret :: "agent ⇒ msg set" where
 [simp]: "staticSecret A == {Key (priEK A), Key (priSK A), Key (shrK A)}"


text‹More subsidiary lemmas combining initial secrets and knowledge of generic agent›

lemma staticSecret_in_initState [simp]:
"staticSecret A ⊆ initState A"
by (cases A, simp)
thm parts_insert

lemma staticSecretA_notin_initStateB:
"m ∈ staticSecret A ⟹ m ∈ initState B = (A=B)"
by (cases B, auto)

lemma staticSecretA_notin_parts_initStateB:
"m ∈ staticSecret A ⟹ m ∈ parts(initState B) = (A=B)"
by (cases B, auto)

lemma staticSecretA_notin_analz_initStateB:
"m ∈ staticSecret A ⟹ m ∈ analz(initState B) = (A=B)"
by (cases B, force dest: analz_into_parts)

lemma staticSecret_synth_eq: 
"m ∈ staticSecret A ⟹ (m ∈ synth H) = (m ∈ H)"
apply force
done

declare staticSecret_def [simp del]

lemma nonce_notin_analz_initState:
  "Nonce N ∉ analz(initState A)" 
by(cases A, auto dest: analz_into_parts)


subsection‹Protocol independent study›

lemma staticSecret_parts_agent:
 "⟦m ∈ parts (knows C evs); m ∈ staticSecret A⟧ ⟹  
   A=C ∨ 
  (∃D E X. Says D E X ∈ set evs ∧ m ∈ parts{X}) ∨
  (∃Y. Notes C Y ∈ set evs ∧ m ∈ parts{Y})"
apply (erule rev_mp)
apply (induct_tac evs)
txt‹@{subgoals [display,indent =1]}›
apply (simp add: staticSecretA_notin_parts_initStateB)
apply (induct_tac a)
(*Says*) 
apply (rule impI) 
apply simp
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
(*Gets*)
apply simp
(*Notes*)
apply simp
apply clarify 
txt‹@{subgoals [display,indent =1]}›
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
done

lemma staticSecret_analz_agent:
 "⟦m ∈ analz (knows C evs); m ∈ staticSecret A⟧ ⟹  
   A=C ∨ 
  (∃D E X. Says D E X ∈ set evs ∧ m ∈ parts{X}) ∨
  (∃Y. Notes C Y ∈ set evs ∧ m ∈ parts{Y})"
by (drule analz_into_parts [THEN staticSecret_parts_agent])

lemma secret_parts_agent:
 "m ∈ parts (knows C evs)  ⟹ m ∈ initState C ∨
 (∃A B X. Says A B X ∈ set evs ∧ m ∈ parts{X}) ∨
 (∃Y. Notes C Y ∈ set evs ∧ m ∈ parts{Y})"
apply (erule rev_mp)
apply (induct_tac "evs")
apply (simp add: parts_initState)
apply (induct_tac "a")
(*Says*)
apply (rule impI)
apply simp
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
(*Gets*)
apply simp
(*Notes*)
apply simp 
apply clarify
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
done

subsection‹Protocol dependent study›

(*NS_no_Notes moved up in NS_Public_Bad_GA.thy so that it's visible to a sibling theory of this one's

As with DolevYao, studying a guarantee similar to
NS_no_Says_staticSecret makes the specialisation proof strategy collapse, because it elicits the same assumptions of the theorem that should be specified.
*)

lemma NS_staticSecret_parts_agent_weak:
 "⟦m ∈ parts (knows C evs); m ∈ staticSecret A; 
   evs ∈ ns_public⟧ ⟹
  A=C ∨ (∃D E X. Says D E X ∈ set evs ∧ m ∈ parts{X})"
apply (blast dest: NS_no_Notes staticSecret_parts_agent)
done

text‹Can't prove the homologous theorem of NS\_Says\_Spy\_staticSecret, hence the specialisation proof strategy cannot be applied›

(*Simple though illustrative corollary*)
(*note use of Says_imp_knows, an enforcement of the threat model*)
lemma NS_staticSecret_parts_agent_parts:
"⟦m ∈ parts (knows C evs); m ∈ staticSecret A; A≠C; evs ∈ ns_public⟧ ⟹
  m ∈ parts(knows D evs)"
apply (blast dest: NS_staticSecret_parts_agent_weak Says_imp_knows [THEN parts.Inj] parts_trans)
(*Alternative proof
apply (blast dest: staticSecret_parts_agent NS_no_Notes Says_imp_knows [THEN parts.Inj] parts_trans)*)
done

text‹
The previous theorems show that in general any agent could send anybody's initial secret, namely the threat model does not impose anything against it. However, the actual protocol specification will, where agents either follow the protocol or build messages out of their traffic analysis - this is actually the same in DY

Therefore, we are only left with the direct proof strategy.
›

lemma NS_staticSecret_parts_agent:
 "⟦m ∈ parts (knows C evs); m ∈ staticSecret A; 
   C≠A; evs ∈ ns_public⟧
 ⟹ ∃ B X. Says A B X ∈ set evs ∧ m ∈ parts {X}"
apply (erule rev_mp, erule ns_public.induct)
(*Nil*)
apply (simp add: staticSecretA_notin_parts_initStateB)
(*Fake*)
apply simp
apply clarify
apply (drule parts_insert [THEN equalityD1, THEN subsetD])(*shot1*)
apply (case_tac "Aa=A") 
apply clarify
txt‹@{subgoals [display,indent=1,goals_limit=2]}›
apply blast
(*Aa≠A*)
apply simp
apply clarify (*applies induction hypothesis!*)(*shot2*)
txt‹@{subgoals [display,indent=1,goals_limit=1]}›
apply (drule Fake_parts_sing [THEN subsetD], simp)  (*shot3*)
apply (simp add: staticSecret_synth_eq) 
txt‹@{subgoals [display,indent=1,goals_limit=1]}›
apply (blast dest: NS_staticSecret_parts_agent_parts)
(*rest!*)
apply (force simp add: staticSecret_def)+
done


lemma NS_agent_see_staticSecret:
 "⟦m ∈ staticSecret A; C≠A; evs ∈ ns_public⟧
 ⟹ m ∈ parts (knows C evs) = (∃ B X. Says A B X ∈ set evs ∧ m ∈ parts {X})"
apply (force dest: NS_staticSecret_parts_agent Says_imp_knows [THEN parts.Inj] intro: parts_trans)
done


declare analz.Decrypt [rule del]

lemma analz_insert_analz: "
⟦ c ∉ parts{Z}; ∀K. Key K ∉ parts{Z}; c ∈ analz(insert Z H)⟧ ⟹ c ∈ analz H"
apply (erule rev_mp, erule rev_mp)
apply (erule analz.induct)
prefer 4
apply clarify
txt‹@{subgoals [display,indent=1,goals_limit=1]}›
apply (blast dest: parts.Body analz.Decrypt)
apply blast+
done

lemma Agent_not_see_NA:
     "⟦ Key (priEK B) ∉ analz(knows C evs); 
        Key (priEK A) ∉ analz(knows C evs);
        ∀S R Y. Says S R Y ∈ set evs ⟶ 
         Y = Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∨
         Y = Crypt (pubEK A) ⦃Nonce NA, Nonce NB⦄ ∨
         Nonce NA ∉ parts{Y} ∧ (∀K. Key K ∉ parts{Y});
        C≠A; C≠B;  evs ∈ ns_public⟧                     
       ⟹ Nonce NA ∉ analz (knows C evs)"
apply (erule rev_mp, erule rev_mp, erule rev_mp, erule ns_public.induct) 
apply (simp add: nonce_notin_analz_initState)
apply clarify
apply simp
(*fixing confidentiality of both private keys*)
apply (drule subset_insertI [THEN analz_mono, THEN contra_subsetD])+
txt‹@{subgoals [display,indent=1,goals_limit=1]}›
apply (subgoal_tac "
        ∀S R Y.
           (S = Aa ∧ R = Ba ∧ Y = X ⟶
            X = Crypt (pubK B) ⦃Nonce NA, Agent A⦄ ∨
            X = Crypt (pubK A) ⦃Nonce NA, Nonce NB⦄ ∨
            Nonce NA ∉ parts {X} ∧ (∀K. Key K ∉ parts {X}))")
prefer 2 
apply blast 
apply simp
txt‹@{subgoals [display,indent=1,goals_limit=1]}›
apply (force dest!: analz_insert_analz)
(*Alternative proof
apply (erule disjE) apply simp 
apply (erule disjE) apply simp 
apply (blast dest: analz_insert_analz)
*)
apply auto
done



end