src/HOL/Auth/Guard/Guard_Yahalom.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01 ago)
changeset 35416 d8d7d1b785af
parent 23746 a455e69c31cc
child 39216 62332b382dba
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
     1 (******************************************************************************
     2 date: march 2002
     3 author: Frederic Blanqui
     4 email: blanqui@lri.fr
     5 webpage: http://www.lri.fr/~blanqui/
     6 
     7 University of Cambridge, Computer Laboratory
     8 William Gates Building, JJ Thomson Avenue
     9 Cambridge CB3 0FD, United Kingdom
    10 ******************************************************************************)
    11 
    12 header{*Yahalom Protocol*}
    13 
    14 theory Guard_Yahalom imports Guard_Shared begin
    15 
    16 subsection{*messages used in the protocol*}
    17 
    18 abbreviation (input)
    19   ya1 :: "agent => agent => nat => event" where
    20   "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
    21 
    22 abbreviation (input)
    23   ya1' :: "agent => agent => agent => nat => event" where
    24   "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
    25 
    26 abbreviation (input)
    27   ya2 :: "agent => agent => nat => nat => event" where
    28   "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    29 
    30 abbreviation (input)
    31   ya2' :: "agent => agent => agent => nat => nat => event" where
    32   "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    33 
    34 abbreviation (input)
    35   ya3 :: "agent => agent => nat => nat => key => event" where
    36   "ya3 A B NA NB K ==
    37     Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
    38                     Ciph B {|Agent A, Key K|}|}"
    39 
    40 abbreviation (input)
    41   ya3':: "agent => msg => agent => agent => nat => nat => key => event" where
    42   "ya3' S Y A B NA NB K ==
    43     Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
    44 
    45 abbreviation (input)
    46   ya4 :: "agent => agent => nat => nat => msg => event" where
    47   "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
    48 
    49 abbreviation (input)
    50   ya4' :: "agent => agent => nat => nat => msg => event" where
    51   "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
    52 
    53 
    54 subsection{*definition of the protocol*}
    55 
    56 inductive_set ya :: "event list set"
    57 where
    58 
    59   Nil: "[]:ya"
    60 
    61 | Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
    62 
    63 | YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
    64 
    65 | YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
    66   ==> ya2 A B NA NB # evs2:ya"
    67 
    68 | YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
    69   ==> ya3 A B NA NB K # evs3:ya"
    70 
    71 | YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
    72   ==> ya4 A B K NB Y # evs4:ya"
    73 
    74 subsection{*declarations for tactics*}
    75 
    76 declare knows_Spy_partsEs [elim]
    77 declare Fake_parts_insert [THEN subsetD, dest]
    78 declare initState.simps [simp del]
    79 
    80 subsection{*general properties of ya*}
    81 
    82 lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
    83 by (erule ya.induct, auto)
    84 
    85 lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
    86 by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
    87 
    88 lemma ya_is_one_step [iff]: "one_step ya"
    89 by (unfold one_step_def, clarify, ind_cases "ev#evs:ya" for ev evs, auto)
    90 
    91 lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
    92 ev:set evs --> (EX A B X. ev=Says A B X)"
    93 by (erule ya.induct, auto)
    94 
    95 lemma ya_has_only_Says [iff]: "has_only_Says ya"
    96 by (auto simp: has_only_Says_def dest: ya_has_only_Says')
    97 
    98 lemma ya_is_regular [iff]: "regular ya"
    99 apply (simp only: regular_def, clarify)
   100 apply (erule ya.induct, simp_all add: initState.simps knows.simps)
   101 by (auto dest: parts_sub)
   102 
   103 subsection{*guardedness of KAB*}
   104 
   105 lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
   106 ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
   107 apply (erule ya.induct)
   108 (* Nil *)
   109 apply simp_all
   110 (* Fake *)
   111 apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
   112 (* YA1 *)
   113 (* YA2 *)
   114 apply safe
   115 apply (blast dest: Says_imp_spies)
   116 (* YA3 *)
   117 apply blast
   118 apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   119 apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   120 (* YA4 *)
   121 apply (blast dest: Says_imp_spies in_GuardK_kparts)
   122 by blast
   123 
   124 subsection{*session keys are not symmetric keys*}
   125 
   126 lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
   127 ya3 A B NA NB K:set evs --> K ~:range shrK"
   128 by (erule ya.induct, auto)
   129 
   130 lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
   131 by (blast dest: KAB_isnt_shrK)
   132 
   133 subsection{*ya2' implies ya1'*}
   134 
   135 lemma ya2'_parts_imp_ya1'_parts [rule_format]:
   136      "[| evs:ya; B ~:bad |] ==>
   137       Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
   138       {|Agent A, Nonce NA|}:spies evs"
   139 by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
   140 
   141 lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
   142 ==> {|Agent A, Nonce NA|}:spies evs"
   143 by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
   144 
   145 subsection{*uniqueness of NB*}
   146 
   147 lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
   148 Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
   149 Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
   150 A=A' & B=B' & NA=NA'"
   151 apply (erule ya.induct, simp_all, clarify)
   152 apply (drule Crypt_synth_insert, simp+)
   153 apply (drule Crypt_synth_insert, simp+, safe)
   154 apply (drule not_used_parts_false, simp+)+
   155 by (drule Says_not_parts, simp+)+
   156 
   157 lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
   158 ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
   159 ==> A=A' & B=B' & NA=NA'"
   160 by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
   161 
   162 subsection{*ya3' implies ya2'*}
   163 
   164 lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
   165 Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
   166 --> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
   167 apply (erule ya.induct, simp_all)
   168 apply (clarify, drule Crypt_synth_insert, simp+)
   169 apply (blast intro: parts_sub, blast)
   170 by (auto dest: Says_imp_spies parts_parts)
   171 
   172 lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
   173 Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
   174 --> (EX B'. ya2' B' A B NA NB:set evs)"
   175 apply (erule ya.induct, simp_all, safe)
   176 apply (drule Crypt_synth_insert, simp+)
   177 apply (drule Crypt_synth_insert, simp+, blast)
   178 apply blast
   179 apply blast
   180 by (auto dest: Says_imp_spies2 parts_parts)
   181 
   182 lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
   183 ==> (EX B'. ya2' B' A B NA NB:set evs)"
   184 by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
   185 
   186 subsection{*ya3' implies ya3*}
   187 
   188 lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
   189 Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
   190 --> ya3 A B NA NB K:set evs"
   191 apply (erule ya.induct, simp_all, safe)
   192 apply (drule Crypt_synth_insert, simp+)
   193 by (blast dest: Says_imp_spies2 parts_parts)
   194 
   195 lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
   196 ==> ya3 A B NA NB K:set evs"
   197 by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
   198 
   199 subsection{*guardedness of NB*}
   200 
   201 definition ya_keys :: "agent => agent => nat => nat => event list => key set" where
   202 "ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
   203 
   204 lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
   205 ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
   206 apply (erule ya.induct)
   207 (* Nil *)
   208 apply (simp_all add: ya_keys_def)
   209 (* Fake *)
   210 apply safe
   211 apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
   212 apply (frule_tac B=B in Guard_KAB, simp+)
   213 apply (drule_tac p=ya in GuardK_Key_analz, simp+)
   214 apply (blast dest: KAB_isnt_shrK, simp)
   215 (* YA1 *)
   216 apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   217 (* YA2 *)
   218 apply blast
   219 apply (drule Says_imp_spies)
   220 apply (drule_tac n=NB in Nonce_neq, simp+)
   221 apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
   222 apply (rule No_Nonce, simp)
   223 (* YA3 *)
   224 apply (rule Guard_extand, simp, blast)
   225 apply (case_tac "NAa=NB", clarify)
   226 apply (frule Says_imp_spies)
   227 apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   228 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   229 apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
   230 apply (case_tac "NBa=NB", clarify)
   231 apply (frule Says_imp_spies)
   232 apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   233 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   234 apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
   235 apply (simp add: No_Nonce, blast)
   236 (* YA4 *)
   237 apply (blast dest: Says_imp_spies)
   238 apply (case_tac "NBa=NB", clarify)
   239 apply (frule_tac A=S in Says_imp_spies)
   240 apply (frule in_Guard_kparts_Crypt, simp+)
   241 apply (blast dest: Says_imp_spies)
   242 apply (case_tac "NBa=NB", clarify)
   243 apply (frule_tac A=S in Says_imp_spies)
   244 apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   245 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
   246 apply (frule ya3'_imp_ya2', simp+, blast, clarify)
   247 apply (frule_tac A=B' in Says_imp_spies)
   248 apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   249 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   250 apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
   251 apply (drule ya3'_imp_ya3, simp+)
   252 apply (simp add: Guard_Nonce)
   253 apply (simp add: No_Nonce)
   254 done
   255 
   256 end