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