src/HOL/Auth/Guard/Extensions.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/Auth/Guard/Extensions.thy
     2     Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     3     Copyright   2001  University of Cambridge
     4 *)
     5 
     6 section {*Extensions to Standard Theories*}
     7 
     8 theory Extensions
     9 imports "../Event"
    10 begin
    11 
    12 subsection{*Extensions to Theory @{text Set}*}
    13 
    14 lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B"
    15 by auto
    16 
    17 lemma insert_Un: "P ({x} Un A) ==> P (insert x A)"
    18 by simp
    19 
    20 lemma in_sub: "x:A ==> {x}<=A"
    21 by auto
    22 
    23 
    24 subsection{*Extensions to Theory @{text List}*}
    25 
    26 subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
    27 
    28 primrec remove :: "'a list => 'a => 'a list" where
    29 "remove [] y = []" |
    30 "remove (x#xs) y = (if x=y then xs else x # remove xs y)"
    31 
    32 lemma set_remove: "set (remove l x) <= set l"
    33 by (induct l, auto)
    34 
    35 subsection{*Extensions to Theory @{text Message}*}
    36 
    37 subsubsection{*declarations for tactics*}
    38 
    39 declare analz_subset_parts [THEN subsetD, dest]
    40 declare parts_insert2 [simp]
    41 declare analz_cut [dest]
    42 declare split_if_asm [split]
    43 declare analz_insertI [intro]
    44 declare Un_Diff [simp]
    45 
    46 subsubsection{*extract the agent number of an Agent message*}
    47 
    48 primrec agt_nb :: "msg => agent" where
    49 "agt_nb (Agent A) = A"
    50 
    51 subsubsection{*messages that are pairs*}
    52 
    53 definition is_MPair :: "msg => bool" where
    54 "is_MPair X == EX Y Z. X = {|Y,Z|}"
    55 
    56 declare is_MPair_def [simp]
    57 
    58 lemma MPair_is_MPair [iff]: "is_MPair {|X,Y|}"
    59 by simp
    60 
    61 lemma Agent_isnt_MPair [iff]: "~ is_MPair (Agent A)"
    62 by simp
    63 
    64 lemma Number_isnt_MPair [iff]: "~ is_MPair (Number n)"
    65 by simp
    66 
    67 lemma Key_isnt_MPair [iff]: "~ is_MPair (Key K)"
    68 by simp
    69 
    70 lemma Nonce_isnt_MPair [iff]: "~ is_MPair (Nonce n)"
    71 by simp
    72 
    73 lemma Hash_isnt_MPair [iff]: "~ is_MPair (Hash X)"
    74 by simp
    75 
    76 lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)"
    77 by simp
    78 
    79 abbreviation
    80   not_MPair :: "msg => bool" where
    81   "not_MPair X == ~ is_MPair X"
    82 
    83 lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P"
    84 by auto
    85 
    86 declare is_MPair_def [simp del]
    87 
    88 definition has_no_pair :: "msg set => bool" where
    89 "has_no_pair H == ALL X Y. {|X,Y|} ~:H"
    90 
    91 declare has_no_pair_def [simp]
    92 
    93 subsubsection{*well-foundedness of messages*}
    94 
    95 lemma wf_Crypt1 [iff]: "Crypt K X ~= X"
    96 by (induct X, auto)
    97 
    98 lemma wf_Crypt2 [iff]: "X ~= Crypt K X"
    99 by (induct X, auto)
   100 
   101 lemma parts_size: "X:parts {Y} ==> X=Y | size X < size Y"
   102 by (erule parts.induct, auto)
   103 
   104 lemma wf_Crypt_parts [iff]: "Crypt K X ~:parts {X}"
   105 by (auto dest: parts_size)
   106 
   107 subsubsection{*lemmas on keysFor*}
   108 
   109 definition usekeys :: "msg set => key set" where
   110 "usekeys G == {K. EX Y. Crypt K Y:G}"
   111 
   112 lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)"
   113 apply (simp add: keysFor_def)
   114 apply (rule finite_imageI)
   115 apply (induct G rule: finite_induct)
   116 apply auto
   117 apply (case_tac "EX K X. x = Crypt K X", clarsimp)
   118 apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F}
   119 = insert K (usekeys F)", auto simp: usekeys_def)
   120 by (subgoal_tac "{K. EX X. Crypt K X = x | Crypt K X:F} = usekeys F",
   121 auto simp: usekeys_def)
   122 
   123 subsubsection{*lemmas on parts*}
   124 
   125 lemma parts_sub: "[| X:parts G; G<=H |] ==> X:parts H"
   126 by (auto dest: parts_mono)
   127 
   128 lemma parts_Diff [dest]: "X:parts (G - H) ==> X:parts G"
   129 by (erule parts_sub, auto)
   130 
   131 lemma parts_Diff_notin: "[| Y ~:H; Nonce n ~:parts (H - {Y}) |]
   132 ==> Nonce n ~:parts H"
   133 by simp
   134 
   135 lemmas parts_insert_substI = parts_insert [THEN ssubst]
   136 lemmas parts_insert_substD = parts_insert [THEN sym, THEN ssubst]
   137 
   138 lemma finite_parts_msg [iff]: "finite (parts {X})"
   139 by (induct X, auto)
   140 
   141 lemma finite_parts [intro]: "finite H ==> finite (parts H)"
   142 apply (erule finite_induct, simp)
   143 by (rule parts_insert_substI, simp)
   144 
   145 lemma parts_parts: "[| X:parts {Y}; Y:parts G |] ==> X:parts G"
   146 by (frule parts_cut, auto) 
   147 
   148 
   149 lemma parts_parts_parts: "[| X:parts {Y}; Y:parts {Z}; Z:parts G |] ==> X:parts G"
   150 by (auto dest: parts_parts)
   151 
   152 lemma parts_parts_Crypt: "[| Crypt K X:parts G; Nonce n:parts {X} |]
   153 ==> Nonce n:parts G"
   154 by (blast intro: parts.Body dest: parts_parts)
   155 
   156 subsubsection{*lemmas on synth*}
   157 
   158 lemma synth_sub: "[| X:synth G; G<=H |] ==> X:synth H"
   159 by (auto dest: synth_mono)
   160 
   161 lemma Crypt_synth [rule_format]: "[| X:synth G; Key K ~:G |] ==>
   162 Crypt K Y:parts {X} --> Crypt K Y:parts G"
   163 by (erule synth.induct, auto dest: parts_sub)
   164 
   165 subsubsection{*lemmas on analz*}
   166 
   167 lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)"
   168   by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+
   169 
   170 lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H"
   171 by (auto dest: analz_mono)
   172 
   173 lemma analz_Diff [dest]: "X:analz (G - H) ==> X:analz G"
   174 by (erule analz.induct, auto)
   175 
   176 lemmas in_analz_subset_cong = analz_subset_cong [THEN subsetD]
   177 
   178 lemma analz_eq: "A=A' ==> analz A = analz A'"
   179 by auto
   180 
   181 lemmas insert_commute_substI = insert_commute [THEN ssubst]
   182 
   183 lemma analz_insertD:
   184      "[| Crypt K Y:H; Key (invKey K):H |] ==> analz (insert Y H) = analz H"
   185 by (blast intro: analz.Decrypt analz_insert_eq)  
   186 
   187 lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==>
   188 X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)"
   189 by (erule analz.induct, auto)
   190 
   191 lemma analz_needs_only_finite: "X:analz H ==> EX G. G <= H & finite G"
   192 by (erule analz.induct, auto)
   193 
   194 lemma notin_analz_insert: "X ~:analz (insert Y G) ==> X ~:analz G"
   195 by auto
   196 
   197 subsubsection{*lemmas on parts, synth and analz*}
   198 
   199 lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
   200 X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
   201 by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
   202 
   203 lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
   204 by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
   205 
   206 lemmas in_analz_subset_parts = analz_subset_parts [THEN subsetD]
   207 
   208 lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
   209 Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
   210 apply (drule parts_insert_substD, clarify)
   211 apply (frule in_sub)
   212 apply (frule parts_mono)
   213 apply auto
   214 done
   215 
   216 subsubsection{*greatest nonce used in a message*}
   217 
   218 fun greatest_msg :: "msg => nat"
   219 where
   220   "greatest_msg (Nonce n) = n"
   221 | "greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)"
   222 | "greatest_msg (Crypt K X) = greatest_msg X"
   223 | "greatest_msg other = 0"
   224 
   225 lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
   226 by (induct X, auto)
   227 
   228 subsubsection{*sets of keys*}
   229 
   230 definition keyset :: "msg set => bool" where
   231 "keyset G == ALL X. X:G --> (EX K. X = Key K)"
   232 
   233 lemma keyset_in [dest]: "[| keyset G; X:G |] ==> EX K. X = Key K"
   234 by (auto simp: keyset_def)
   235 
   236 lemma MPair_notin_keyset [simp]: "keyset G ==> {|X,Y|} ~:G"
   237 by auto
   238 
   239 lemma Crypt_notin_keyset [simp]: "keyset G ==> Crypt K X ~:G"
   240 by auto
   241 
   242 lemma Nonce_notin_keyset [simp]: "keyset G ==> Nonce n ~:G"
   243 by auto
   244 
   245 lemma parts_keyset [simp]: "keyset G ==> parts G = G"
   246 by (auto, erule parts.induct, auto)
   247 
   248 subsubsection{*keys a priori necessary for decrypting the messages of G*}
   249 
   250 definition keysfor :: "msg set => msg set" where
   251 "keysfor G == Key ` keysFor (parts G)"
   252 
   253 lemma keyset_keysfor [iff]: "keyset (keysfor G)"
   254 by (simp add: keyset_def keysfor_def, blast)
   255 
   256 lemma keyset_Diff_keysfor [simp]: "keyset H ==> keyset (H - keysfor G)"
   257 by (auto simp: keyset_def)
   258 
   259 lemma keysfor_Crypt: "Crypt K X:parts G ==> Key (invKey K):keysfor G"
   260 by (auto simp: keysfor_def Crypt_imp_invKey_keysFor)
   261 
   262 lemma no_key_no_Crypt: "Key K ~:keysfor G ==> Crypt (invKey K) X ~:parts G"
   263 by (auto dest: keysfor_Crypt)
   264 
   265 lemma finite_keysfor [intro]: "finite G ==> finite (keysfor G)"
   266 by (auto simp: keysfor_def intro: finite_UN_I)
   267 
   268 subsubsection{*only the keys necessary for G are useful in analz*}
   269 
   270 lemma analz_keyset: "keyset H ==>
   271 analz (G Un H) = H - keysfor G Un (analz (G Un (H Int keysfor G)))"
   272 apply (rule eq)
   273 apply (erule analz.induct, blast)
   274 apply (simp, blast)
   275 apply (simp, blast)
   276 apply (case_tac "Key (invKey K):H - keysfor G", clarsimp)
   277 apply (drule_tac X=X in no_key_no_Crypt)
   278 by (auto intro: analz_sub)
   279 
   280 lemmas analz_keyset_substD = analz_keyset [THEN sym, THEN ssubst]
   281 
   282 
   283 subsection{*Extensions to Theory @{text Event}*}
   284 
   285 
   286 subsubsection{*general protocol properties*}
   287 
   288 definition is_Says :: "event => bool" where
   289 "is_Says ev == (EX A B X. ev = Says A B X)"
   290 
   291 lemma is_Says_Says [iff]: "is_Says (Says A B X)"
   292 by (simp add: is_Says_def)
   293 
   294 (* one could also require that Gets occurs after Says
   295 but this is sufficient for our purpose *)
   296 definition Gets_correct :: "event list set => bool" where
   297 "Gets_correct p == ALL evs B X. evs:p --> Gets B X:set evs
   298 --> (EX A. Says A B X:set evs)"
   299 
   300 lemma Gets_correct_Says: "[| Gets_correct p; Gets B X # evs:p |]
   301 ==> EX A. Says A B X:set evs"
   302 apply (simp add: Gets_correct_def)
   303 by (drule_tac x="Gets B X # evs" in spec, auto)
   304 
   305 definition one_step :: "event list set => bool" where
   306 "one_step p == ALL evs ev. ev#evs:p --> evs:p"
   307 
   308 lemma one_step_Cons [dest]: "[| one_step p; ev#evs:p |] ==> evs:p"
   309 by (unfold one_step_def, blast)
   310 
   311 lemma one_step_app: "[| evs@evs':p; one_step p; []:p |] ==> evs':p"
   312 by (induct evs, auto)
   313 
   314 lemma trunc: "[| evs @ evs':p; one_step p |] ==> evs':p"
   315 by (induct evs, auto)
   316 
   317 definition has_only_Says :: "event list set => bool" where
   318 "has_only_Says p == ALL evs ev. evs:p --> ev:set evs
   319 --> (EX A B X. ev = Says A B X)"
   320 
   321 lemma has_only_SaysD: "[| ev:set evs; evs:p; has_only_Says p |]
   322 ==> EX A B X. ev = Says A B X"
   323 by (unfold has_only_Says_def, blast)
   324 
   325 lemma in_has_only_Says [dest]: "[| has_only_Says p; evs:p; ev:set evs |]
   326 ==> EX A B X. ev = Says A B X"
   327 by (auto simp: has_only_Says_def)
   328 
   329 lemma has_only_Says_imp_Gets_correct [simp]: "has_only_Says p
   330 ==> Gets_correct p"
   331 by (auto simp: has_only_Says_def Gets_correct_def)
   332 
   333 subsubsection{*lemma on knows*}
   334 
   335 lemma Says_imp_spies2: "Says A B {|X,Y|}:set evs ==> Y:parts (spies evs)"
   336 by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp)
   337 
   338 lemma Says_not_parts: "[| Says A B X:set evs; Y ~:parts (spies evs) |]
   339 ==> Y ~:parts {X}"
   340 by (auto dest: Says_imp_spies parts_parts)
   341 
   342 subsubsection{*knows without initState*}
   343 
   344 primrec knows' :: "agent => event list => msg set" where
   345   knows'_Nil: "knows' A [] = {}" |
   346   knows'_Cons0:
   347  "knows' A (ev # evs) = (
   348    if A = Spy then (
   349      case ev of
   350        Says A' B X => insert X (knows' A evs)
   351      | Gets A' X => knows' A evs
   352      | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs
   353    ) else (
   354      case ev of
   355        Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs
   356      | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs
   357      | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
   358    ))"
   359 
   360 abbreviation
   361   spies' :: "event list => msg set" where
   362   "spies' == knows' Spy"
   363 
   364 subsubsection{*decomposition of knows into knows' and initState*}
   365 
   366 lemma knows_decomp: "knows A evs = knows' A evs Un (initState A)"
   367 by (induct evs, auto split: event.split simp: knows.simps)
   368 
   369 lemmas knows_decomp_substI = knows_decomp [THEN ssubst]
   370 lemmas knows_decomp_substD = knows_decomp [THEN sym, THEN ssubst]
   371 
   372 lemma knows'_sub_knows: "knows' A evs <= knows A evs"
   373 by (auto simp: knows_decomp)
   374 
   375 lemma knows'_Cons: "knows' A (ev#evs) = knows' A [ev] Un knows' A evs"
   376 by (induct ev, auto)
   377 
   378 lemmas knows'_Cons_substI = knows'_Cons [THEN ssubst]
   379 lemmas knows'_Cons_substD = knows'_Cons [THEN sym, THEN ssubst]
   380 
   381 lemma knows_Cons: "knows A (ev#evs) = initState A Un knows' A [ev]
   382 Un knows A evs"
   383 apply (simp only: knows_decomp)
   384 apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans)
   385 apply (simp only: knows'_Cons [of A ev evs] Un_ac)
   386 apply blast
   387 done
   388 
   389 
   390 lemmas knows_Cons_substI = knows_Cons [THEN ssubst]
   391 lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst]
   392 
   393 lemma knows'_sub_spies': "[| evs:p; has_only_Says p; one_step p |]
   394 ==> knows' A evs <= spies' evs"
   395 by (induct evs, auto split: event.splits)
   396 
   397 subsubsection{*knows' is finite*}
   398 
   399 lemma finite_knows' [iff]: "finite (knows' A evs)"
   400 by (induct evs, auto split: event.split simp: knows.simps)
   401 
   402 subsubsection{*monotonicity of knows*}
   403 
   404 lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)"
   405 by(cases A, induct evs, auto simp: knows.simps split:event.split)
   406 
   407 lemma knows_ConsI: "X:knows A evs ==> X:knows A (ev#evs)"
   408 by (auto dest: knows_sub_Cons [THEN subsetD])
   409 
   410 lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')"
   411 apply (induct evs, auto)
   412 apply (simp add: knows_decomp)
   413 apply (rename_tac a b c)
   414 by (case_tac a, auto simp: knows.simps)
   415 
   416 subsubsection{*maximum knowledge an agent can have
   417 includes messages sent to the agent*}
   418 
   419 primrec knows_max' :: "agent => event list => msg set" where
   420 knows_max'_def_Nil: "knows_max' A [] = {}" |
   421 knows_max'_def_Cons: "knows_max' A (ev # evs) = (
   422   if A=Spy then (
   423     case ev of
   424       Says A' B X => insert X (knows_max' A evs)
   425     | Gets A' X => knows_max' A evs
   426     | Notes A' X =>
   427       if A':bad then insert X (knows_max' A evs) else knows_max' A evs
   428   ) else (
   429     case ev of
   430       Says A' B X =>
   431       if A=A' | A=B then insert X (knows_max' A evs) else knows_max' A evs
   432     | Gets A' X =>
   433       if A=A' then insert X (knows_max' A evs) else knows_max' A evs
   434     | Notes A' X =>
   435       if A=A' then insert X (knows_max' A evs) else knows_max' A evs
   436   ))"
   437 
   438 definition knows_max :: "agent => event list => msg set" where
   439 "knows_max A evs == knows_max' A evs Un initState A"
   440 
   441 abbreviation
   442   spies_max :: "event list => msg set" where
   443   "spies_max evs == knows_max Spy evs"
   444 
   445 subsubsection{*basic facts about @{term knows_max}*}
   446 
   447 lemma spies_max_spies [iff]: "spies_max evs = spies evs"
   448 by (induct evs, auto simp: knows_max_def split: event.splits)
   449 
   450 lemma knows_max'_Cons: "knows_max' A (ev#evs)
   451 = knows_max' A [ev] Un knows_max' A evs"
   452 by (auto split: event.splits)
   453 
   454 lemmas knows_max'_Cons_substI = knows_max'_Cons [THEN ssubst]
   455 lemmas knows_max'_Cons_substD = knows_max'_Cons [THEN sym, THEN ssubst]
   456 
   457 lemma knows_max_Cons: "knows_max A (ev#evs)
   458 = knows_max' A [ev] Un knows_max A evs"
   459 apply (simp add: knows_max_def del: knows_max'_def_Cons)
   460 apply (rule_tac evs=evs in knows_max'_Cons_substI)
   461 by blast
   462 
   463 lemmas knows_max_Cons_substI = knows_max_Cons [THEN ssubst]
   464 lemmas knows_max_Cons_substD = knows_max_Cons [THEN sym, THEN ssubst]
   465 
   466 lemma finite_knows_max' [iff]: "finite (knows_max' A evs)"
   467 by (induct evs, auto split: event.split)
   468 
   469 lemma knows_max'_sub_spies': "[| evs:p; has_only_Says p; one_step p |]
   470 ==> knows_max' A evs <= spies' evs"
   471 by (induct evs, auto split: event.splits)
   472 
   473 lemma knows_max'_in_spies' [dest]: "[| evs:p; X:knows_max' A evs;
   474 has_only_Says p; one_step p |] ==> X:spies' evs"
   475 by (rule knows_max'_sub_spies' [THEN subsetD], auto)
   476 
   477 lemma knows_max'_app: "knows_max' A (evs @ evs')
   478 = knows_max' A evs Un knows_max' A evs'"
   479 by (induct evs, auto split: event.splits)
   480 
   481 lemma Says_to_knows_max': "Says A B X:set evs ==> X:knows_max' B evs"
   482 by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app)
   483 
   484 lemma Says_from_knows_max': "Says A B X:set evs ==> X:knows_max' A evs"
   485 by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app)
   486 
   487 subsubsection{*used without initState*}
   488 
   489 primrec used' :: "event list => msg set" where
   490 "used' [] = {}" |
   491 "used' (ev # evs) = (
   492   case ev of
   493     Says A B X => parts {X} Un used' evs
   494     | Gets A X => used' evs
   495     | Notes A X => parts {X} Un used' evs
   496   )"
   497 
   498 definition init :: "msg set" where
   499 "init == used []"
   500 
   501 lemma used_decomp: "used evs = init Un used' evs"
   502 by (induct evs, auto simp: init_def split: event.split)
   503 
   504 lemma used'_sub_app: "used' evs <= used' (evs@evs')"
   505 by (induct evs, auto split: event.split)
   506 
   507 lemma used'_parts [rule_format]: "X:used' evs ==> Y:parts {X} --> Y:used' evs"
   508 apply (induct evs, simp)
   509 apply (rename_tac a b)
   510 apply (case_tac a, simp_all) 
   511 apply (blast dest: parts_trans)+ 
   512 done
   513 
   514 subsubsection{*monotonicity of used*}
   515 
   516 lemma used_sub_Cons: "used evs <= used (ev#evs)"
   517 by (induct evs, (induct ev, auto)+)
   518 
   519 lemma used_ConsI: "X:used evs ==> X:used (ev#evs)"
   520 by (auto dest: used_sub_Cons [THEN subsetD])
   521 
   522 lemma notin_used_ConsD: "X ~:used (ev#evs) ==> X ~:used evs"
   523 by (auto dest: used_sub_Cons [THEN subsetD])
   524 
   525 lemma used_appD [dest]: "X:used (evs @ evs') ==> X:used evs | X:used evs'"
   526 by (induct evs, auto, rename_tac a b, case_tac a, auto)
   527 
   528 lemma used_ConsD: "X:used (ev#evs) ==> X:used [ev] | X:used evs"
   529 by (case_tac ev, auto)
   530 
   531 lemma used_sub_app: "used evs <= used (evs@evs')"
   532 by (auto simp: used_decomp dest: used'_sub_app [THEN subsetD])
   533 
   534 lemma used_appIL: "X:used evs ==> X:used (evs' @ evs)"
   535 by (induct evs', auto intro: used_ConsI)
   536 
   537 lemma used_appIR: "X:used evs ==> X:used (evs @ evs')"
   538 by (erule used_sub_app [THEN subsetD])
   539 
   540 lemma used_parts: "[| X:parts {Y}; Y:used evs |] ==> X:used evs"
   541 apply (auto simp: used_decomp dest: used'_parts)
   542 by (auto simp: init_def used_Nil dest: parts_trans)
   543 
   544 lemma parts_Says_used: "[| Says A B X:set evs; Y:parts {X} |] ==> Y:used evs"
   545 by (induct evs, simp_all, safe, auto intro: used_ConsI)
   546 
   547 lemma parts_used_app: "X:parts {Y} ==> X:used (evs @ Says A B Y # evs')"
   548 apply (drule_tac evs="[Says A B Y]" in used_parts, simp, blast)
   549 apply (drule_tac evs'=evs' in used_appIR)
   550 apply (drule_tac evs'=evs in used_appIL)
   551 by simp
   552 
   553 subsubsection{*lemmas on used and knows*}
   554 
   555 lemma initState_used: "X:parts (initState A) ==> X:used evs"
   556 by (induct evs, auto simp: used.simps split: event.split)
   557 
   558 lemma Says_imp_used: "Says A B X:set evs ==> parts {X} <= used evs"
   559 by (induct evs, auto intro: used_ConsI)
   560 
   561 lemma not_used_not_spied: "X ~:used evs ==> X ~:parts (spies evs)"
   562 by (induct evs, auto simp: used_Nil)
   563 
   564 lemma not_used_not_parts: "[| Y ~:used evs; Says A B X:set evs |]
   565 ==> Y ~:parts {X}"
   566 by (induct evs, auto intro: used_ConsI)
   567 
   568 lemma not_used_parts_false: "[| X ~:used evs; Y:parts (spies evs) |]
   569 ==> X ~:parts {Y}"
   570 by (auto dest: parts_parts)
   571 
   572 lemma known_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
   573 ==> X:parts (knows A evs) --> X:used evs"
   574 apply (case_tac "A=Spy", blast)
   575 apply (induct evs)
   576 apply (simp add: used.simps, blast)
   577 apply (rename_tac a evs)
   578 apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
   579 apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
   580 apply (erule initState_used)
   581 apply (case_tac a, auto)
   582 apply (rename_tac msg)
   583 apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
   584 by (auto dest: Says_imp_used intro: used_ConsI)
   585 
   586 lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
   587 ==> X:parts (knows_max A evs) --> X:used evs"
   588 apply (case_tac "A=Spy")
   589 apply force
   590 apply (induct evs)
   591 apply (simp add: knows_max_def used.simps, blast)
   592 apply (rename_tac a evs)
   593 apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
   594 apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
   595 apply (case_tac a, auto)
   596 apply (rename_tac msg)
   597 apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
   598 by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
   599 
   600 lemma not_used_not_known: "[| evs:p; X ~:used evs;
   601 Gets_correct p; one_step p |] ==> X ~:parts (knows A evs)"
   602 by (case_tac "A=Spy", auto dest: not_used_not_spied known_used)
   603 
   604 lemma not_used_not_known_max: "[| evs:p; X ~:used evs;
   605 Gets_correct p; one_step p |] ==> X ~:parts (knows_max A evs)"
   606 by (case_tac "A=Spy", auto dest: not_used_not_spied known_max_used)
   607 
   608 subsubsection{*a nonce or key in a message cannot equal a fresh nonce or key*}
   609 
   610 lemma Nonce_neq [dest]: "[| Nonce n' ~:used evs;
   611 Says A B X:set evs; Nonce n:parts {X} |] ==> n ~= n'"
   612 by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)
   613 
   614 lemma Key_neq [dest]: "[| Key n' ~:used evs;
   615 Says A B X:set evs; Key n:parts {X} |] ==> n ~= n'"
   616 by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)
   617 
   618 subsubsection{*message of an event*}
   619 
   620 primrec msg :: "event => msg"
   621 where
   622   "msg (Says A B X) = X"
   623 | "msg (Gets A X) = X"
   624 | "msg (Notes A X) = X"
   625 
   626 lemma used_sub_parts_used: "X:used (ev # evs) ==> X:parts {msg ev} Un used evs"
   627 by (induct ev, auto)
   628 
   629 end