Theory Guard_Yahalom

(*  Title:      HOL/Auth/Guard/Guard_Yahalom.thy
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    Copyright   2002  University of Cambridge
*)

section‹Yahalom Protocol›

theory Guard_Yahalom imports "../Shared" Guard_Shared begin

subsection‹messages used in the protocol›

abbreviation (input)
  ya1 :: "agent => agent => nat => event" where
  "ya1 A B NA == Says A B ⦃Agent A, Nonce NA⦄"

abbreviation (input)
  ya1' :: "agent => agent => agent => nat => event" where
  "ya1' A' A B NA == Says A' B ⦃Agent A, Nonce NA⦄"

abbreviation (input)
  ya2 :: "agent => agent => nat => nat => event" where
  "ya2 A B NA NB == Says B Server ⦃Agent B, Ciph B ⦃Agent A, Nonce NA, Nonce NB⦄⦄"

abbreviation (input)
  ya2' :: "agent => agent => agent => nat => nat => event" where
  "ya2' B' A B NA NB == Says B' Server ⦃Agent B, Ciph B ⦃Agent A, Nonce NA, Nonce NB⦄⦄"

abbreviation (input)
  ya3 :: "agent => agent => nat => nat => key => event" where
  "ya3 A B NA NB K ==
    Says Server A ⦃Ciph A ⦃Agent B, Key K, Nonce NA, Nonce NB⦄,
                    Ciph B ⦃Agent A, Key K⦄⦄"

abbreviation (input)
  ya3':: "agent => msg => agent => agent => nat => nat => key => event" where
  "ya3' S Y A B NA NB K ==
    Says S A ⦃Ciph A ⦃Agent B, Key K, Nonce NA, Nonce NB⦄, Y⦄"

abbreviation (input)
  ya4 :: "agent => agent => nat => nat => msg => event" where
  "ya4 A B K NB Y == Says A B ⦃Y, Crypt K (Nonce NB)⦄"

abbreviation (input)
  ya4' :: "agent => agent => nat => nat => msg => event" where
  "ya4' A' B K NB Y == Says A' B ⦃Y, Crypt K (Nonce NB)⦄"


subsection‹definition of the protocol›

inductive_set ya :: "event list set"
where

  Nil: "[] ∈ ya"

| Fake: "⟦evs ∈ ya; X ∈ synth (analz (spies evs))⟧ ⟹ Says Spy B X # evs ∈ ya"

| YA1: "⟦evs1 ∈ ya; Nonce NA ∉ used evs1⟧ ⟹ ya1 A B NA # evs1 ∈ ya"

| YA2: "⟦evs2 ∈ ya; ya1' A' A B NA ∈ set evs2; Nonce NB ∉ used evs2⟧
  ⟹ ya2 A B NA NB # evs2 ∈ ya"

| YA3: "⟦evs3 ∈ ya; ya2' B' A B NA NB ∈ set evs3; Key K ∉ used evs3⟧
  ⟹ ya3 A B NA NB K # evs3 ∈ ya"

| YA4: "⟦evs4 ∈ ya; ya1 A B NA ∈ set evs4; ya3' S Y A B NA NB K ∈ set evs4⟧
  ⟹ ya4 A B K NB Y # evs4 ∈ ya"

subsection‹declarations for tactics›

declare knows_Spy_partsEs [elim]
declare Fake_parts_insert [THEN subsetD, dest]
declare initState.simps [simp del]

subsection‹general properties of ya›

lemma ya_has_no_Gets: "evs ∈ ya ⟹ ∀A X. Gets A X ∉ set evs"
by (erule ya.induct, auto)

lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
by (auto simp: Gets_correct_def dest: ya_has_no_Gets)

lemma ya_is_one_step [iff]: "one_step ya"
  unfolding one_step_def by (clarify, ind_cases "ev#evs ∈ ya" for ev evs, auto)

lemma ya_has_only_Says' [rule_format]: "evs ∈ ya ⟹
ev ∈ set evs ⟶ (∃A B X. ev=Says A B X)"
by (erule ya.induct, auto)

lemma ya_has_only_Says [iff]: "has_only_Says ya"
by (auto simp: has_only_Says_def dest: ya_has_only_Says')

lemma ya_is_regular [iff]: "regular ya"
apply (simp only: regular_def, clarify)
apply (erule ya.induct, simp_all add: initState.simps knows.simps)
by (auto dest: parts_sub)

subsection‹guardedness of KAB›

lemma Guard_KAB [rule_format]: "⟦evs ∈ ya; A ∉ bad; B ∉ bad⟧ ⟹
ya3 A B NA NB K ∈ set evs ⟶ GuardK K {shrK A,shrK B} (spies evs)" 
apply (erule ya.induct)
(* Nil *)
apply simp_all
(* Fake *)
apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
(* YA1 *)
(* YA2 *)
apply safe
apply (blast dest: Says_imp_spies)
(* YA3 *)
apply blast
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
(* YA4 *)
apply (blast dest: Says_imp_spies in_GuardK_kparts)
by blast

subsection‹session keys are not symmetric keys›

lemma KAB_isnt_shrK [rule_format]: "evs ∈ ya ⟹
ya3 A B NA NB K ∈ set evs ⟶ K ∉ range shrK"
by (erule ya.induct, auto)

lemma ya3_shrK: "evs ∈ ya ⟹ ya3 A B NA NB (shrK C) ∉ set evs"
by (blast dest: KAB_isnt_shrK)

subsection‹ya2' implies ya1'›

lemma ya2'_parts_imp_ya1'_parts [rule_format]:
     "⟦evs ∈ ya; B ∉ bad⟧ ⟹
      Ciph B ⦃Agent A, Nonce NA, Nonce NB⦄ ∈ parts (spies evs) ⟶
      ⦃Agent A, Nonce NA⦄ ∈ spies evs"
by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)

lemma ya2'_imp_ya1'_parts: "⟦ya2' B' A B NA NB ∈ set evs; evs ∈ ya; B ∉ bad⟧
⟹ ⦃Agent A, Nonce NA⦄ ∈ spies evs"
by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)

subsection‹uniqueness of NB›

lemma NB_is_uniq_in_ya2'_parts [rule_format]: "⟦evs ∈ ya; B ∉ bad; B' ∉ bad⟧ ⟹
Ciph B ⦃Agent A, Nonce NA, Nonce NB⦄ ∈ parts (spies evs) ⟶
Ciph B' ⦃Agent A', Nonce NA', Nonce NB⦄ ∈ parts (spies evs) ⟶
A=A' ∧ B=B' ∧ NA=NA'"
apply (erule ya.induct, simp_all, clarify)
apply (drule Crypt_synth_insert, simp+)
apply (drule Crypt_synth_insert, simp+, safe)
apply (drule not_used_parts_false, simp+)+
by (drule Says_not_parts, simp+)+

lemma NB_is_uniq_in_ya2': "⟦ya2' C A B NA NB ∈ set evs;
ya2' C' A' B' NA' NB ∈ set evs; evs ∈ ya; B ∉ bad; B' ∉ bad⟧
⟹ A=A' ∧ B=B' ∧ NA=NA'"
by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)

subsection‹ya3' implies ya2'›

lemma ya3'_parts_imp_ya2'_parts [rule_format]: "⟦evs ∈ ya; A ∉ bad⟧ ⟹
Ciph A ⦃Agent B, Key K, Nonce NA, Nonce NB⦄ ∈ parts (spies evs)
⟶ Ciph B ⦃Agent A, Nonce NA, Nonce NB⦄ ∈ parts (spies evs)"
apply (erule ya.induct, simp_all)
apply (clarify, drule Crypt_synth_insert, simp+)
apply (blast intro: parts_sub, blast)
by (auto dest: Says_imp_spies parts_parts)

lemma ya3'_parts_imp_ya2' [rule_format]: "⟦evs ∈ ya; A ∉ bad⟧ ⟹
Ciph A ⦃Agent B, Key K, Nonce NA, Nonce NB⦄ ∈ parts (spies evs)
⟶ (∃B'. ya2' B' A B NA NB ∈ set evs)"
apply (erule ya.induct, simp_all, safe)
apply (drule Crypt_synth_insert, simp+)
apply (drule Crypt_synth_insert, simp+, blast)
apply blast
apply blast
by (auto dest: Says_imp_spies2 parts_parts)

lemma ya3'_imp_ya2': "⟦ya3' S Y A B NA NB K ∈ set evs; evs ∈ ya; A ∉ bad⟧
⟹ (∃B'. ya2' B' A B NA NB ∈ set evs)"
by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)

subsection‹ya3' implies ya3›

lemma ya3'_parts_imp_ya3 [rule_format]: "⟦evs ∈ ya; A ∉ bad⟧ ⟹
Ciph A ⦃Agent B, Key K, Nonce NA, Nonce NB⦄ ∈ parts(spies evs)
⟶ ya3 A B NA NB K ∈ set evs"
apply (erule ya.induct, simp_all, safe)
apply (drule Crypt_synth_insert, simp+)
by (blast dest: Says_imp_spies2 parts_parts)

lemma ya3'_imp_ya3: "⟦ya3' S Y A B NA NB K ∈ set evs; evs ∈ ya; A ∉ bad⟧
⟹ ya3 A B NA NB K ∈ set evs"
by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)

subsection‹guardedness of NB›

definition ya_keys :: "agent ⇒ agent ⇒ nat ⇒ nat ⇒ event list ⇒ key set" where
"ya_keys A B NA NB evs ≡ {shrK A,shrK B} ∪ {K. ya3 A B NA NB K ∈ set evs}"

lemma Guard_NB [rule_format]: "⟦evs ∈ ya; A ∉ bad; B ∉ bad⟧ ⟹
ya2 A B NA NB ∈ set evs ⟶ Guard NB (ya_keys A B NA NB evs) (spies evs)"
apply (erule ya.induct)
(* Nil *)
apply (simp_all add: ya_keys_def)
(* Fake *)
apply safe
apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
apply (frule_tac B=B in Guard_KAB, simp+)
apply (drule_tac p=ya in GuardK_Key_analz, simp+)
apply (blast dest: KAB_isnt_shrK, simp)
(* YA1 *)
apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
(* YA2 *)
apply blast
apply (drule Says_imp_spies)
apply (drule_tac n=NB in Nonce_neq, simp+)
apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
apply (rule No_Nonce, simp)
(* YA3 *)
apply (rule Guard_extand, simp, blast)
apply (case_tac "NAa=NB", clarify)
apply (frule Says_imp_spies)
apply (frule in_Guard_kparts_Crypt, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
apply (case_tac "NBa=NB", clarify)
apply (frule Says_imp_spies)
apply (frule in_Guard_kparts_Crypt, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
apply (simp add: No_Nonce, blast)
(* YA4 *)
apply (blast dest: Says_imp_spies)
apply (case_tac "NBa=NB", clarify)
apply (frule_tac A=S in Says_imp_spies)
apply (frule in_Guard_kparts_Crypt, simp+)
apply (blast dest: Says_imp_spies)
apply (case_tac "NBa=NB", clarify)
apply (frule_tac A=S in Says_imp_spies)
apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
apply (frule ya3'_imp_ya2', simp+, blast, clarify)
apply (frule_tac A=B' in Says_imp_spies)
apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
apply (drule ya3'_imp_ya3, simp+)
apply (simp add: Guard_Nonce)
apply (simp add: No_Nonce)
done

end