Up to index of Isabelle/HOL/Inductive_Confidentiality
theory ConfidentialityDYheader{*Inductive Study of Confidentiality against Dolev-Yao*}
theory ConfidentialityDY imports NS_Public_Bad begin
section{*Existing study - fully spelled out*}
text{*In order not to leave hidden anything of the line of reasoning, we cancel some relevant lemmas that were installed previously*}
declare Spy_see_priEK [simp del]
Spy_analz_priEK [simp del]
image_eq_UN [simp del]
analz_into_parts [rule del]
subsection{*On static secrets*}
lemma Spy_see_priEK:
"evs ∈ ns_public ==> (Key (priEK A) ∈ parts (spies evs)) = (A ∈ bad)"
apply (erule ns_public.induct, simp_all)
(*Fake: screenshot1*)
apply (cases "A:bad")
thm ccontr
(*apply (rule ccontr) apply simp*)
apply blast (*Spy knows bad agents' keys since start*)
apply clarify (*screenshot2*)
thm Fake_parts_insert [THEN subsetD]
apply (drule Fake_parts_insert [THEN subsetD], simp)(*screenshot3*)
apply (blast dest: analz_into_parts)
done
lemma Spy_analz_priEK:
"evs ∈ ns_public ==> (Key (priEK A) ∈ analz (spies evs)) = (A ∈ bad)"
(*apply (auto simp: Spy_see_priEK dest: analz_into_parts)*)
apply (erule ns_public.induct, simp_all)
(*Nil*)
thm analz_image_freshK_simps
apply (simp add: analz_image_freshK_simps)
(*Fake*)
(*apply spy_analz would close, alternatively:*)
apply (cases "A:bad")
apply clarify apply simp
apply blast (*Spy knows bad agents' keys since start*)
apply clarsimp
apply (drule Fake_analz_insert [THEN subsetD], simp)
apply clarsimp
done
subsection{*On dynamic secrets*}
lemma Spy_not_see_NA:
"[|Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) ∈ set evs;
A ∉ bad; B ∉ bad; evs ∈ ns_public|]
==> Nonce NA ∉ analz (spies evs)"
apply (erule rev_mp, erule ns_public.induct)
apply (simp_all add: Spy_analz_priEK)
(*screenshot1*)
thm conjI
apply (rule conjI)
apply clarify
apply clarify
(*screenshot2*)
apply (drule Fake_analz_insert [THEN subsetD], simp)
(*screenshot3*)
apply simp
apply (blast dest: unique_NA analz_into_parts intro: no_nonce_NS1_NS2)+
done
lemma Spy_not_see_NB:
"[|Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) ∈ set evs;
∀C. Says A C (Crypt (pubEK C) (Nonce NB)) ∉ set evs;
A ∉ bad; B ∉ bad; evs ∈ ns_public|]
==> Nonce NB ∉ analz (spies evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule ns_public.induct)
apply (simp_all add: Spy_analz_priEK)
txt{*apply @{term spy_analz}
is replaced here with the following list...*}
apply (rule ccontr)
apply clarsimp
apply (erule disjE)
apply simp
apply simp
apply clarify
apply (drule Fake_analz_insert [THEN subsetD], simp)
apply simp
txt{*...of commands!*}
apply (simp_all add: all_conj_distrib) txt{*speeds up next*}
apply (blast dest: analz_into_parts intro: no_nonce_NS1_NS2)+
done
section{*Novel study*}
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)}"
subsection{*Protocol independent study*}
text{*Converse doesn't hold because something that is said or noted is not necessarily an initial secret*}
lemma staticSecret_parts_Spy:
"[|m ∈ parts (knows Spy evs); m ∈ staticSecret A|] ==>
A ∈ bad ∨
(∃C B X. Says C B X ∈ set evs ∧ m ∈ parts{X}) ∨
(∃C Y. Notes C Y ∈ set evs ∧ C ∈ bad ∧ m ∈ parts{Y})"
apply (erule rev_mp)
apply (induct_tac "evs")
apply force
apply (induct_tac "a")
txt{*Says*}
txt{*@{subgoals [display,indent=1]}*}
apply (rule impI)
apply simp
txt{*@{subgoals [display,indent=1]}*}
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
txt{*@{subgoals [display,indent=1]}*}
apply blast
txt{*Gets*}
apply simp
txt{*Notes*}
apply (rule impI)
apply simp
apply (case_tac "agent∉bad")
apply simp apply blast
apply simp
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
done
lemma staticSecret_analz_Spy:
"[|m ∈ analz (knows Spy evs); m ∈ staticSecret A|] ==>
A ∈ bad ∨
(∃C B X. Says C B X ∈ set evs ∧ m ∈ parts{X}) ∨
(∃C Y. Notes C Y ∈ set evs ∧ C ∈ bad ∧ m ∈ parts{Y})"
by (drule analz_into_parts [THEN staticSecret_parts_Spy])
lemma secret_parts_Spy:
"m ∈ parts (knows Spy evs) ==>
m ∈ initState Spy ∨
(∃C B X. Says C B X ∈ set evs ∧ m ∈ parts{X}) ∨
(∃C Y. Notes C Y ∈ set evs ∧ C ∈ bad ∧ m ∈ parts{Y})"
apply (erule rev_mp)
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
txt{*Says*}
apply (rule impI)
apply (simp del: initState_Spy)
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply (simp only: Un_iff)
apply blast
txt{*Gets*}
apply simp
txt{*Notes*}
apply (rule impI)
apply (simp del: initState_Spy)
apply (case_tac "agent∉bad")
apply (simp del: initState_Spy)
apply blast
apply (simp del: initState_Spy)
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
done
lemma secret_parts_Spy_converse:
" m ∈ initState Spy ∨
(∃C B X. Says C B X ∈ set evs ∧ m ∈ parts{X}) ∨
(∃C Y. Notes C Y ∈ set evs ∧ C ∈ bad ∧ m ∈ parts{Y})
==> m ∈ parts(knows Spy evs)"
apply (erule disjE)
apply force
apply (erule disjE)
apply (blast dest: Says_imp_knows_Spy [THEN parts.Inj] parts_trans)
apply (blast dest: Notes_imp_knows_Spy [THEN parts.Inj] parts_trans)
done
lemma secret_analz_Spy:
"m ∈ analz (knows Spy evs) ==>
m ∈ initState Spy ∨
(∃C B X. Says C B X ∈ set evs ∧ m ∈ parts{X}) ∨
(∃C Y. Notes C Y ∈ set evs ∧ C ∈ bad ∧ m ∈ parts{Y})"
by (blast dest: analz_into_parts secret_parts_Spy)
subsection{*Protocol-dependent study*}
text{*Proving generalised version of @{thm Spy_see_priEK} using same strategy, the "direct" strategy*}
lemma NS_Spy_see_staticSecret:
"[|m ∈ staticSecret A; evs ∈ ns_public|] ==>
m ∈ parts(knows Spy evs) = (A ∈ bad)"
apply (erule ns_public.induct)
apply simp_all
prefer 2
apply (cases "A:bad")
apply blast (*Spy knows bad agents' keys since start*)
apply clarify
apply (drule Fake_parts_insert [THEN subsetD], simp)
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (blast dest: analz_into_parts)
apply force+
done
text{*Seeking a proof of @{thm NS_Spy_see_staticSecret} using an alternative, "specialisation" strategy*}
lemma NS_no_Notes:
"evs ∈ ns_public ==> Notes A X ∉ set evs"
apply (erule ns_public.induct)
apply simp_all
done
lemma NS_staticSecret_parts_Spy_weak:
"[|m ∈ parts (knows Spy evs); m ∈ staticSecret A;
evs ∈ ns_public|] ==> A ∈ bad ∨
(∃C B X. Says C B X ∈ set evs ∧ m ∈ parts{X})"
apply (blast dest: staticSecret_parts_Spy NS_no_Notes)
done
lemma NS_Says_staticSecret:
"[|Says A B X ∈ set evs; m ∈ staticSecret C; m ∈ parts{X};
evs ∈ ns_public|] ==> A=Spy"
apply (erule rev_mp)
apply (erule ns_public.induct)
apply force+
done
text{*This generalises @{thm Key_synth_eq}*}
lemma staticSecret_synth_eq:
"m ∈ staticSecret A ==> (m ∈ synth H) = (m ∈ H)"
apply force
done
lemma NS_Says_Spy_staticSecret:
"[|Says Spy B X ∈ set evs; m ∈ parts{X};
m ∈ staticSecret A; evs ∈ ns_public|] ==> A ∈ bad"
(*
txt{*Alternative start to appreciate that it reduces to @{thm NS_Spy_see_staticSecret}*}
apply (erule rev_mp, erule ns_public.induct)
apply (simp_all del: staticSecret_def)
apply clarify
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (drule Fake_parts_sing [THEN subsetD], simp)
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (simp del: staticSecret_def add: staticSecret_synth_eq)
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
oops
*)
apply (drule Says_imp_knows_Spy [THEN parts.Inj])
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (drule parts_trans, simp)
apply (rotate_tac -1)
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (erule rev_mp)
apply (erule ns_public.induct)
apply simp_all
prefer 2
apply (cases "A:bad")
apply blast (*Spy knows bad agents' keys since start*)
apply clarsimp
apply (drule Fake_parts_insert [THEN subsetD], simp)
apply (blast dest: analz_into_parts)
apply force+
done
text{*Here's the specialised version of @{thm staticSecret_parts_Spy}*}
lemma NS_staticSecret_parts_Spy:
"[|m ∈ parts (knows Spy evs); m ∈ staticSecret A;
evs ∈ ns_public|] ==> A ∈ bad"
apply (drule staticSecret_parts_Spy)
apply assumption
txt{*@{subgoals [display,indent=1]}*}
apply (erule disjE)
(*Case A bad*)
apply assumption
apply (erule disjE)
(*Case: Says*)
apply (erule exE)+
txt{*@{subgoals [display,indent=1]}*}
apply (case_tac "C=Spy")
apply (blast dest: NS_Says_Spy_staticSecret)
apply (blast dest: NS_Says_staticSecret)
apply (blast dest: NS_no_Notes)
done
text{*Concluding the specialisation proof strategy...*}
lemma NS_Spy_see_staticSecret_spec:
"[|m ∈ staticSecret A; evs ∈ ns_public|] ==>
m ∈ parts (knows Spy evs) = (A ∈ bad)"
txt{*one line proof:
apply (force dest: @{term NS_staticSecret_parts_Spy})
*}
apply safe
apply (blast dest: NS_staticSecret_parts_Spy)
txt{*one line proof: force*}
apply simp
apply (erule disjE)
apply clarify
apply (drule_tac b=Encryption and evs=evs in Spy_spies_bad_privateKey)
apply (drule parts.Inj, assumption)
apply (erule disjE)
apply clarify
apply (drule_tac b=Signature and evs=evs in Spy_spies_bad_privateKey)
apply (drule parts.Inj, assumption)
apply clarify
apply (drule_tac evs=evs in Spy_spies_bad_shrK)
apply (drule parts.Inj, assumption)
done
lemma NS_Spy_analz_staticSecret:
"[|m ∈ staticSecret A; evs ∈ ns_public|] ==>
m ∈ analz (knows Spy evs) = (A ∈ bad)"
apply (force dest: analz_into_parts NS_staticSecret_parts_Spy)
done
lemma NS_staticSecret_subset_parts_knows_Spy:
"evs ∈ ns_public ==>
staticSecret A ⊆ parts (knows Spy evs) = (A ∈ bad)"
apply (force dest: NS_staticSecret_parts_Spy)
done
lemma NS_staticSecret_subset_analz_knows_Spy:
"evs ∈ ns_public ==>
staticSecret A ⊆ analz (knows Spy evs) = (A ∈ bad)"
apply (force dest: analz_into_parts NS_staticSecret_parts_Spy)
done
end