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