src/HOL/Auth/Message.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7057 b9ddbb925939
child 8054 2ce57ef2a4aa
permissions -rw-r--r--
tidied; added lemma restrict_to_left
paulson@1839
     1
(*  Title:      HOL/Auth/Message
paulson@1839
     2
    ID:         $Id$
paulson@1839
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1839
     4
    Copyright   1996  University of Cambridge
paulson@1839
     5
paulson@1839
     6
Datatypes of agents and messages;
paulson@1913
     7
Inductive relations "parts", "analz" and "synth"
paulson@1839
     8
*)
paulson@1839
     9
paulson@3702
    10
paulson@3702
    11
(*Eliminates a commonly-occurring expression*)
paulson@3702
    12
goal HOL.thy "~ (ALL x. x~=y)";
paulson@3702
    13
by (Blast_tac 1);
paulson@3702
    14
Addsimps [result()];
paulson@3702
    15
paulson@3668
    16
AddIffs msg.inject;
paulson@1839
    17
paulson@4422
    18
(*Equations hold because constructors are injective; cannot prove for all f*)
paulson@5076
    19
Goal "(Friend x : Friend``A) = (x:A)";
paulson@4477
    20
by Auto_tac;
paulson@3514
    21
qed "Friend_image_eq";
paulson@4422
    22
paulson@5076
    23
Goal "(Key x : Key``A) = (x:A)";
paulson@4477
    24
by Auto_tac;
paulson@4422
    25
qed "Key_image_eq";
paulson@4422
    26
paulson@5076
    27
Goal "(Nonce x ~: Key``A)";
paulson@4477
    28
by Auto_tac;
paulson@4422
    29
qed "Nonce_Key_image_eq";
paulson@4422
    30
Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
paulson@3514
    31
paulson@3514
    32
paulson@1839
    33
(** Inverse of keys **)
paulson@1839
    34
paulson@5493
    35
Goal "(invKey K = invKey K') = (K=K')";
paulson@3730
    36
by Safe_tac;
paulson@2032
    37
by (rtac box_equals 1);
paulson@1839
    38
by (REPEAT (rtac invKey 2));
paulson@1839
    39
by (Asm_simp_tac 1);
paulson@1839
    40
qed "invKey_eq";
paulson@1839
    41
paulson@1839
    42
Addsimps [invKey, invKey_eq];
paulson@1839
    43
paulson@1839
    44
paulson@1839
    45
(**** keysFor operator ****)
paulson@1839
    46
paulson@5076
    47
Goalw [keysFor_def] "keysFor {} = {}";
paulson@2891
    48
by (Blast_tac 1);
paulson@1839
    49
qed "keysFor_empty";
paulson@1839
    50
paulson@5076
    51
Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
paulson@2891
    52
by (Blast_tac 1);
paulson@1839
    53
qed "keysFor_Un";
paulson@1839
    54
paulson@5076
    55
Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
paulson@2891
    56
by (Blast_tac 1);
paulson@4157
    57
qed "keysFor_UN";
paulson@1839
    58
paulson@1839
    59
(*Monotonicity*)
paulson@5114
    60
Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)";
paulson@2891
    61
by (Blast_tac 1);
paulson@1839
    62
qed "keysFor_mono";
paulson@1839
    63
paulson@5076
    64
Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
paulson@7057
    65
by Auto_tac;
paulson@1839
    66
qed "keysFor_insert_Agent";
paulson@1839
    67
paulson@5076
    68
Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
paulson@7057
    69
by Auto_tac;
paulson@1839
    70
qed "keysFor_insert_Nonce";
paulson@1839
    71
paulson@5076
    72
Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
paulson@7057
    73
by Auto_tac;
paulson@3668
    74
qed "keysFor_insert_Number";
paulson@3668
    75
paulson@5076
    76
Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
paulson@7057
    77
by Auto_tac;
paulson@1839
    78
qed "keysFor_insert_Key";
paulson@1839
    79
paulson@5076
    80
Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
paulson@7057
    81
by Auto_tac;
paulson@2373
    82
qed "keysFor_insert_Hash";
paulson@2373
    83
paulson@5076
    84
Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
paulson@7057
    85
by Auto_tac;
paulson@1839
    86
qed "keysFor_insert_MPair";
paulson@1839
    87
paulson@5076
    88
Goalw [keysFor_def]
paulson@2284
    89
    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
paulson@4477
    90
by Auto_tac;
paulson@1839
    91
qed "keysFor_insert_Crypt";
paulson@1839
    92
paulson@4157
    93
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
paulson@3668
    94
          keysFor_insert_Agent, keysFor_insert_Nonce, 
paulson@3668
    95
	  keysFor_insert_Number, keysFor_insert_Key, 
paulson@2516
    96
          keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
paulson@3121
    97
AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
paulson@4157
    98
	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
paulson@1839
    99
paulson@5076
   100
Goalw [keysFor_def] "keysFor (Key``E) = {}";
paulson@4477
   101
by Auto_tac;
paulson@3514
   102
qed "keysFor_image_Key";
paulson@3514
   103
Addsimps [keysFor_image_Key];
paulson@3514
   104
paulson@5114
   105
Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H";
paulson@2891
   106
by (Blast_tac 1);
paulson@2068
   107
qed "Crypt_imp_invKey_keysFor";
paulson@2068
   108
paulson@1839
   109
paulson@1839
   110
(**** Inductive relation "parts" ****)
paulson@1839
   111
paulson@1839
   112
val major::prems = 
paulson@5076
   113
Goal "[| {|X,Y|} : parts H;       \
paulson@1839
   114
\            [| X : parts H; Y : parts H |] ==> P  \
paulson@1839
   115
\         |] ==> P";
paulson@1839
   116
by (cut_facts_tac [major] 1);
paulson@2032
   117
by (resolve_tac prems 1);
paulson@1839
   118
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
paulson@1839
   119
qed "MPair_parts";
paulson@1839
   120
paulson@1839
   121
AddIs  [parts.Inj];
paulson@1929
   122
paulson@1929
   123
val partsEs = [MPair_parts, make_elim parts.Body];
paulson@1929
   124
paulson@1929
   125
AddSEs partsEs;
paulson@1929
   126
(*NB These two rules are UNSAFE in the formal sense, as they discard the
paulson@1929
   127
     compound message.  They work well on THIS FILE, perhaps because its
paulson@1929
   128
     proofs concern only atomic messages.*)
paulson@1839
   129
paulson@5076
   130
Goal "H <= parts(H)";
paulson@2891
   131
by (Blast_tac 1);
paulson@1839
   132
qed "parts_increasing";
paulson@1839
   133
paulson@1839
   134
(*Monotonicity*)
paulson@5114
   135
Goalw parts.defs "G<=H ==> parts(G) <= parts(H)";
paulson@1839
   136
by (rtac lfp_mono 1);
paulson@1839
   137
by (REPEAT (ares_tac basic_monos 1));
paulson@1839
   138
qed "parts_mono";
paulson@1839
   139
paulson@2373
   140
val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
paulson@2373
   141
paulson@5076
   142
Goal "parts{} = {}";
paulson@3730
   143
by Safe_tac;
paulson@2032
   144
by (etac parts.induct 1);
paulson@2891
   145
by (ALLGOALS Blast_tac);
paulson@1839
   146
qed "parts_empty";
paulson@1839
   147
Addsimps [parts_empty];
paulson@1839
   148
paulson@5114
   149
Goal "X: parts{} ==> P";
paulson@1839
   150
by (Asm_full_simp_tac 1);
paulson@1839
   151
qed "parts_emptyE";
paulson@1839
   152
AddSEs [parts_emptyE];
paulson@1839
   153
paulson@1893
   154
(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
paulson@5114
   155
Goal "X: parts H ==> EX Y:H. X: parts {Y}";
paulson@2032
   156
by (etac parts.induct 1);
paulson@2891
   157
by (ALLGOALS Blast_tac);
paulson@1893
   158
qed "parts_singleton";
paulson@1893
   159
paulson@1839
   160
paulson@1839
   161
(** Unions **)
paulson@1839
   162
paulson@5076
   163
Goal "parts(G) Un parts(H) <= parts(G Un H)";
paulson@1839
   164
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
paulson@1839
   165
val parts_Un_subset1 = result();
paulson@1839
   166
paulson@5076
   167
Goal "parts(G Un H) <= parts(G) Un parts(H)";
paulson@2032
   168
by (rtac subsetI 1);
paulson@2032
   169
by (etac parts.induct 1);
paulson@2891
   170
by (ALLGOALS Blast_tac);
paulson@1839
   171
val parts_Un_subset2 = result();
paulson@1839
   172
paulson@5076
   173
Goal "parts(G Un H) = parts(G) Un parts(H)";
paulson@1839
   174
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
paulson@1839
   175
qed "parts_Un";
paulson@1839
   176
paulson@5076
   177
Goal "parts (insert X H) = parts {X} Un parts H";
paulson@1852
   178
by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
paulson@2011
   179
by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
paulson@2011
   180
qed "parts_insert";
paulson@2011
   181
paulson@2011
   182
(*TWO inserts to avoid looping.  This rewrite is better than nothing.
paulson@2011
   183
  Not suitable for Addsimps: its behaviour can be strange.*)
paulson@5076
   184
Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
wenzelm@4091
   185
by (simp_tac (simpset() addsimps [Un_assoc]) 1);
wenzelm@4091
   186
by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
paulson@1852
   187
qed "parts_insert2";
paulson@1852
   188
paulson@5076
   189
Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
paulson@1839
   190
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
paulson@1839
   191
val parts_UN_subset1 = result();
paulson@1839
   192
paulson@5076
   193
Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
paulson@2032
   194
by (rtac subsetI 1);
paulson@2032
   195
by (etac parts.induct 1);
paulson@2891
   196
by (ALLGOALS Blast_tac);
paulson@1839
   197
val parts_UN_subset2 = result();
paulson@1839
   198
paulson@5076
   199
Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))";
paulson@1839
   200
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
paulson@1839
   201
qed "parts_UN";
paulson@1839
   202
paulson@3121
   203
(*Added to simplify arguments to parts, analz and synth.
paulson@3121
   204
  NOTE: the UN versions are no longer used!*)
paulson@4157
   205
Addsimps [parts_Un, parts_UN];
paulson@3121
   206
AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
paulson@4157
   207
	parts_UN RS equalityD1 RS subsetD RS UN_E];
paulson@1839
   208
paulson@5076
   209
Goal "insert X (parts H) <= parts(insert X H)";
wenzelm@4091
   210
by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
paulson@1839
   211
qed "parts_insert_subset";
paulson@1839
   212
paulson@1839
   213
(** Idempotence and transitivity **)
paulson@1839
   214
paulson@5114
   215
Goal "X: parts (parts H) ==> X: parts H";
paulson@2032
   216
by (etac parts.induct 1);
paulson@2891
   217
by (ALLGOALS Blast_tac);
paulson@2922
   218
qed "parts_partsD";
paulson@2922
   219
AddSDs [parts_partsD];
paulson@1839
   220
paulson@5076
   221
Goal "parts (parts H) = parts H";
paulson@2891
   222
by (Blast_tac 1);
paulson@1839
   223
qed "parts_idem";
paulson@1839
   224
Addsimps [parts_idem];
paulson@1839
   225
paulson@5114
   226
Goal "[| X: parts G;  G <= parts H |] ==> X: parts H";
paulson@1839
   227
by (dtac parts_mono 1);
paulson@2891
   228
by (Blast_tac 1);
paulson@1839
   229
qed "parts_trans";
paulson@1839
   230
paulson@1839
   231
(*Cut*)
paulson@5114
   232
Goal "[| Y: parts (insert X G);  X: parts H |] \
paulson@2373
   233
\              ==> Y: parts (G Un H)";
paulson@2032
   234
by (etac parts_trans 1);
paulson@4477
   235
by Auto_tac;
paulson@1839
   236
qed "parts_cut";
paulson@1839
   237
paulson@5114
   238
Goal "X: parts H ==> parts (insert X H) = parts H";
wenzelm@4091
   239
by (fast_tac (claset() addSDs [parts_cut]
paulson@4556
   240
                       addIs  [parts_insertI] 
paulson@4556
   241
                       addss (simpset())) 1);
paulson@1929
   242
qed "parts_cut_eq";
paulson@1929
   243
paulson@2028
   244
Addsimps [parts_cut_eq];
paulson@2028
   245
paulson@1839
   246
paulson@1839
   247
(** Rewrite rules for pulling out atomic messages **)
paulson@1839
   248
paulson@2373
   249
fun parts_tac i =
paulson@2373
   250
  EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
paulson@2516
   251
         etac parts.induct i,
paulson@7057
   252
         Auto_tac];
paulson@2373
   253
paulson@5076
   254
Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
paulson@2373
   255
by (parts_tac 1);
paulson@1839
   256
qed "parts_insert_Agent";
paulson@1839
   257
paulson@5076
   258
Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
paulson@2373
   259
by (parts_tac 1);
paulson@1839
   260
qed "parts_insert_Nonce";
paulson@1839
   261
paulson@5076
   262
Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
paulson@3668
   263
by (parts_tac 1);
paulson@3668
   264
qed "parts_insert_Number";
paulson@3668
   265
paulson@5076
   266
Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
paulson@2373
   267
by (parts_tac 1);
paulson@1839
   268
qed "parts_insert_Key";
paulson@1839
   269
paulson@5076
   270
Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
paulson@2373
   271
by (parts_tac 1);
paulson@2373
   272
qed "parts_insert_Hash";
paulson@2373
   273
paulson@5076
   274
Goal "parts (insert (Crypt K X) H) = \
paulson@2284
   275
\         insert (Crypt K X) (parts (insert X H))";
paulson@2032
   276
by (rtac equalityI 1);
paulson@2032
   277
by (rtac subsetI 1);
paulson@2032
   278
by (etac parts.induct 1);
paulson@4477
   279
by Auto_tac;
paulson@2032
   280
by (etac parts.induct 1);
wenzelm@4091
   281
by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
paulson@1839
   282
qed "parts_insert_Crypt";
paulson@1839
   283
paulson@5076
   284
Goal "parts (insert {|X,Y|} H) = \
paulson@1839
   285
\         insert {|X,Y|} (parts (insert X (insert Y H)))";
paulson@2032
   286
by (rtac equalityI 1);
paulson@2032
   287
by (rtac subsetI 1);
paulson@2032
   288
by (etac parts.induct 1);
paulson@4477
   289
by Auto_tac;
paulson@2032
   290
by (etac parts.induct 1);
wenzelm@4091
   291
by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
paulson@1839
   292
qed "parts_insert_MPair";
paulson@1839
   293
paulson@3668
   294
Addsimps [parts_insert_Agent, parts_insert_Nonce, 
paulson@3668
   295
	  parts_insert_Number, parts_insert_Key, 
paulson@2373
   296
          parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
paulson@1839
   297
paulson@1839
   298
paulson@5076
   299
Goal "parts (Key``N) = Key``N";
paulson@4477
   300
by Auto_tac;
paulson@2032
   301
by (etac parts.induct 1);
paulson@4477
   302
by Auto_tac;
paulson@2026
   303
qed "parts_image_Key";
paulson@3514
   304
Addsimps [parts_image_Key];
paulson@2026
   305
paulson@3514
   306
paulson@3514
   307
(*In any message, there is an upper bound N on its greatest nonce.*)
paulson@5076
   308
Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
paulson@3668
   309
by (induct_tac "msg" 1);
wenzelm@4091
   310
by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
paulson@3514
   311
(*MPair case: blast_tac works out the necessary sum itself!*)
wenzelm@4091
   312
by (blast_tac (claset() addSEs [add_leE]) 2);
paulson@3514
   313
(*Nonce case*)
paulson@3514
   314
by (res_inst_tac [("x","N + Suc nat")] exI 1);
nipkow@5983
   315
by (auto_tac (claset() addSEs [add_leE], simpset()));
paulson@3514
   316
qed "msg_Nonce_supply";
paulson@2026
   317
paulson@2026
   318
paulson@1913
   319
(**** Inductive relation "analz" ****)
paulson@1839
   320
paulson@1839
   321
val major::prems = 
paulson@5076
   322
Goal "[| {|X,Y|} : analz H;       \
paulson@1913
   323
\            [| X : analz H; Y : analz H |] ==> P  \
paulson@1839
   324
\         |] ==> P";
paulson@1839
   325
by (cut_facts_tac [major] 1);
paulson@2032
   326
by (resolve_tac prems 1);
paulson@1913
   327
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
paulson@1913
   328
qed "MPair_analz";
paulson@1839
   329
paulson@1913
   330
AddIs  [analz.Inj];
paulson@2011
   331
AddSEs [MPair_analz];      (*Perhaps it should NOT be deemed safe!*)
paulson@1913
   332
AddDs  [analz.Decrypt];
paulson@1839
   333
paulson@1913
   334
Addsimps [analz.Inj];
paulson@1885
   335
paulson@5076
   336
Goal "H <= analz(H)";
paulson@2891
   337
by (Blast_tac 1);
paulson@1913
   338
qed "analz_increasing";
paulson@1839
   339
paulson@5076
   340
Goal "analz H <= parts H";
paulson@1839
   341
by (rtac subsetI 1);
paulson@2032
   342
by (etac analz.induct 1);
paulson@2891
   343
by (ALLGOALS Blast_tac);
paulson@1913
   344
qed "analz_subset_parts";
paulson@1839
   345
paulson@1913
   346
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
paulson@1839
   347
paulson@1839
   348
paulson@5076
   349
Goal "parts (analz H) = parts H";
paulson@2032
   350
by (rtac equalityI 1);
paulson@2032
   351
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
paulson@1839
   352
by (Simp_tac 1);
wenzelm@4091
   353
by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1);
paulson@1913
   354
qed "parts_analz";
paulson@1913
   355
Addsimps [parts_analz];
paulson@1839
   356
paulson@5076
   357
Goal "analz (parts H) = parts H";
paulson@4477
   358
by Auto_tac;
paulson@2032
   359
by (etac analz.induct 1);
paulson@4477
   360
by Auto_tac;
paulson@1913
   361
qed "analz_parts";
paulson@1913
   362
Addsimps [analz_parts];
paulson@1885
   363
paulson@1839
   364
(*Monotonicity; Lemma 1 of Lowe*)
paulson@5114
   365
Goalw analz.defs "G<=H ==> analz(G) <= analz(H)";
paulson@1839
   366
by (rtac lfp_mono 1);
paulson@1839
   367
by (REPEAT (ares_tac basic_monos 1));
paulson@1913
   368
qed "analz_mono";
paulson@1839
   369
paulson@2373
   370
val analz_insertI = impOfSubs (subset_insertI RS analz_mono);
paulson@2373
   371
paulson@1839
   372
(** General equational properties **)
paulson@1839
   373
paulson@5076
   374
Goal "analz{} = {}";
paulson@3730
   375
by Safe_tac;
paulson@2032
   376
by (etac analz.induct 1);
paulson@2891
   377
by (ALLGOALS Blast_tac);
paulson@1913
   378
qed "analz_empty";
paulson@1913
   379
Addsimps [analz_empty];
paulson@1839
   380
paulson@1913
   381
(*Converse fails: we can analz more from the union than from the 
paulson@1839
   382
  separate parts, as a key in one might decrypt a message in the other*)
paulson@5076
   383
Goal "analz(G) Un analz(H) <= analz(G Un H)";
paulson@1913
   384
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
paulson@1913
   385
qed "analz_Un";
paulson@1839
   386
paulson@5076
   387
Goal "insert X (analz H) <= analz(insert X H)";
wenzelm@4091
   388
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
paulson@1913
   389
qed "analz_insert";
paulson@1839
   390
paulson@1839
   391
(** Rewrite rules for pulling out atomic messages **)
paulson@1839
   392
paulson@2373
   393
fun analz_tac i =
paulson@2373
   394
  EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
paulson@2516
   395
         etac analz.induct i,
paulson@7057
   396
         Auto_tac];
paulson@2373
   397
paulson@5076
   398
Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
paulson@2373
   399
by (analz_tac 1);
paulson@1913
   400
qed "analz_insert_Agent";
paulson@1839
   401
paulson@5076
   402
Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
paulson@2373
   403
by (analz_tac 1);
paulson@1913
   404
qed "analz_insert_Nonce";
paulson@1839
   405
paulson@5076
   406
Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
paulson@3668
   407
by (analz_tac 1);
paulson@3668
   408
qed "analz_insert_Number";
paulson@3668
   409
paulson@5076
   410
Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
paulson@2373
   411
by (analz_tac 1);
paulson@2373
   412
qed "analz_insert_Hash";
paulson@2373
   413
paulson@1839
   414
(*Can only pull out Keys if they are not needed to decrypt the rest*)
paulson@5076
   415
Goalw [keysFor_def]
paulson@5114
   416
    "K ~: keysFor (analz H) ==>  \
paulson@1913
   417
\         analz (insert (Key K) H) = insert (Key K) (analz H)";
paulson@2373
   418
by (analz_tac 1);
paulson@1913
   419
qed "analz_insert_Key";
paulson@1839
   420
paulson@5076
   421
Goal "analz (insert {|X,Y|} H) = \
paulson@1913
   422
\         insert {|X,Y|} (analz (insert X (insert Y H)))";
paulson@2032
   423
by (rtac equalityI 1);
paulson@2032
   424
by (rtac subsetI 1);
paulson@2032
   425
by (etac analz.induct 1);
paulson@4477
   426
by Auto_tac;
paulson@2032
   427
by (etac analz.induct 1);
wenzelm@4091
   428
by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
paulson@1913
   429
qed "analz_insert_MPair";
paulson@1885
   430
paulson@1885
   431
(*Can pull out enCrypted message if the Key is not known*)
paulson@5114
   432
Goal "Key (invKey K) ~: analz H ==>  \
paulson@2284
   433
\              analz (insert (Crypt K X) H) = \
paulson@2284
   434
\              insert (Crypt K X) (analz H)";
paulson@2373
   435
by (analz_tac 1);
paulson@1913
   436
qed "analz_insert_Crypt";
paulson@1839
   437
paulson@5114
   438
Goal "Key (invKey K) : analz H ==>  \
paulson@2284
   439
\              analz (insert (Crypt K X) H) <= \
paulson@2284
   440
\              insert (Crypt K X) (analz (insert X H))";
paulson@2032
   441
by (rtac subsetI 1);
berghofe@5102
   442
by (eres_inst_tac [("xa","x")] analz.induct 1);
paulson@7057
   443
by Auto_tac;
paulson@1839
   444
val lemma1 = result();
paulson@1839
   445
paulson@5114
   446
Goal "Key (invKey K) : analz H ==>  \
paulson@2284
   447
\              insert (Crypt K X) (analz (insert X H)) <= \
paulson@2284
   448
\              analz (insert (Crypt K X) H)";
paulson@4477
   449
by Auto_tac;
berghofe@5102
   450
by (eres_inst_tac [("xa","x")] analz.induct 1);
paulson@4477
   451
by Auto_tac;
wenzelm@4091
   452
by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
paulson@1839
   453
val lemma2 = result();
paulson@1839
   454
paulson@5114
   455
Goal "Key (invKey K) : analz H ==>  \
paulson@2284
   456
\              analz (insert (Crypt K X) H) = \
paulson@2284
   457
\              insert (Crypt K X) (analz (insert X H))";
paulson@1839
   458
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
paulson@1913
   459
qed "analz_insert_Decrypt";
paulson@1839
   460
paulson@1885
   461
(*Case analysis: either the message is secure, or it is not!
paulson@1946
   462
  Effective, but can cause subgoals to blow up!
paulson@5055
   463
  Use with split_if;  apparently split_tac does not cope with patterns
paulson@2284
   464
  such as "analz (insert (Crypt K X) H)" *)
paulson@5076
   465
Goal "analz (insert (Crypt K X) H) =                \
paulson@2154
   466
\         (if (Key (invKey K) : analz H)                \
paulson@2284
   467
\          then insert (Crypt K X) (analz (insert X H)) \
paulson@2284
   468
\          else insert (Crypt K X) (analz H))";
paulson@2102
   469
by (case_tac "Key (invKey K)  : analz H " 1);
wenzelm@4091
   470
by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, 
paulson@4556
   471
						analz_insert_Decrypt])));
paulson@1913
   472
qed "analz_Crypt_if";
paulson@1885
   473
paulson@3668
   474
Addsimps [analz_insert_Agent, analz_insert_Nonce, 
paulson@3668
   475
	  analz_insert_Number, analz_insert_Key, 
paulson@2516
   476
          analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
paulson@1839
   477
paulson@1839
   478
(*This rule supposes "for the sake of argument" that we have the key.*)
paulson@5076
   479
Goal  "analz (insert (Crypt K X) H) <=  \
paulson@2284
   480
\          insert (Crypt K X) (analz (insert X H))";
paulson@2032
   481
by (rtac subsetI 1);
paulson@2032
   482
by (etac analz.induct 1);
paulson@4477
   483
by Auto_tac;
paulson@1913
   484
qed "analz_insert_Crypt_subset";
paulson@1839
   485
paulson@1839
   486
paulson@5076
   487
Goal "analz (Key``N) = Key``N";
paulson@4477
   488
by Auto_tac;
paulson@2032
   489
by (etac analz.induct 1);
paulson@4477
   490
by Auto_tac;
paulson@2026
   491
qed "analz_image_Key";
paulson@2026
   492
paulson@2026
   493
Addsimps [analz_image_Key];
paulson@2026
   494
paulson@2026
   495
paulson@1839
   496
(** Idempotence and transitivity **)
paulson@1839
   497
paulson@5114
   498
Goal "X: analz (analz H) ==> X: analz H";
paulson@2032
   499
by (etac analz.induct 1);
paulson@2891
   500
by (ALLGOALS Blast_tac);
paulson@2922
   501
qed "analz_analzD";
paulson@2922
   502
AddSDs [analz_analzD];
paulson@1839
   503
paulson@5076
   504
Goal "analz (analz H) = analz H";
paulson@2891
   505
by (Blast_tac 1);
paulson@1913
   506
qed "analz_idem";
paulson@1913
   507
Addsimps [analz_idem];
paulson@1839
   508
paulson@5114
   509
Goal "[| X: analz G;  G <= analz H |] ==> X: analz H";
paulson@1913
   510
by (dtac analz_mono 1);
paulson@2891
   511
by (Blast_tac 1);
paulson@1913
   512
qed "analz_trans";
paulson@1839
   513
paulson@1839
   514
(*Cut; Lemma 2 of Lowe*)
paulson@5114
   515
Goal "[| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
paulson@2032
   516
by (etac analz_trans 1);
paulson@2891
   517
by (Blast_tac 1);
paulson@1913
   518
qed "analz_cut";
paulson@1839
   519
paulson@1839
   520
(*Cut can be proved easily by induction on
paulson@5114
   521
   "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
paulson@1839
   522
*)
paulson@1839
   523
paulson@3449
   524
(*This rewrite rule helps in the simplification of messages that involve
paulson@3449
   525
  the forwarding of unknown components (X).  Without it, removing occurrences
paulson@3449
   526
  of X can be very complicated. *)
paulson@5114
   527
Goal "X: analz H ==> analz (insert X H) = analz H";
wenzelm@4091
   528
by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
paulson@3431
   529
qed "analz_insert_eq";
paulson@3431
   530
paulson@1885
   531
paulson@1913
   532
(** A congruence rule for "analz" **)
paulson@1885
   533
paulson@5114
   534
Goal "[| analz G <= analz G'; analz H <= analz H' \
paulson@1913
   535
\              |] ==> analz (G Un H) <= analz (G' Un H')";
paulson@3714
   536
by (Clarify_tac 1);
paulson@2032
   537
by (etac analz.induct 1);
wenzelm@4091
   538
by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
paulson@1913
   539
qed "analz_subset_cong";
paulson@1885
   540
paulson@5114
   541
Goal "[| analz G = analz G'; analz H = analz H' \
paulson@1913
   542
\              |] ==> analz (G Un H) = analz (G' Un H')";
paulson@1913
   543
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
paulson@2032
   544
          ORELSE' etac equalityE));
paulson@1913
   545
qed "analz_cong";
paulson@1885
   546
paulson@1885
   547
paulson@5114
   548
Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
wenzelm@4091
   549
by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
paulson@4556
   550
                            setloop (rtac analz_cong)) 1);
paulson@1913
   551
qed "analz_insert_cong";
paulson@1885
   552
paulson@1913
   553
(*If there are no pairs or encryptions then analz does nothing*)
paulson@5114
   554
Goal "[| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
paulson@1913
   555
\         analz H = H";
paulson@3730
   556
by Safe_tac;
paulson@2032
   557
by (etac analz.induct 1);
paulson@2891
   558
by (ALLGOALS Blast_tac);
paulson@1913
   559
qed "analz_trivial";
paulson@1839
   560
paulson@4157
   561
(*These two are obsolete (with a single Spy) but cost little to prove...*)
paulson@5114
   562
Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
paulson@2032
   563
by (etac analz.induct 1);
wenzelm@4091
   564
by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
paulson@1839
   565
val lemma = result();
paulson@1839
   566
paulson@5076
   567
Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
wenzelm@4091
   568
by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
paulson@1913
   569
qed "analz_UN_analz";
paulson@1913
   570
Addsimps [analz_UN_analz];
paulson@1839
   571
paulson@1839
   572
paulson@1913
   573
(**** Inductive relation "synth" ****)
paulson@1839
   574
paulson@1913
   575
AddIs  synth.intrs;
paulson@1839
   576
paulson@3668
   577
(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
paulson@6141
   578
val Nonce_synth = synth.mk_cases "Nonce n : synth H";
paulson@6141
   579
val Key_synth   = synth.mk_cases "Key K : synth H";
paulson@6141
   580
val Hash_synth  = synth.mk_cases "Hash X : synth H";
paulson@6141
   581
val MPair_synth = synth.mk_cases "{|X,Y|} : synth H";
paulson@6141
   582
val Crypt_synth = synth.mk_cases "Crypt K X : synth H";
paulson@2011
   583
paulson@2373
   584
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
paulson@2011
   585
paulson@5076
   586
Goal "H <= synth(H)";
paulson@2891
   587
by (Blast_tac 1);
paulson@1913
   588
qed "synth_increasing";
paulson@1839
   589
paulson@1839
   590
(*Monotonicity*)
paulson@5114
   591
Goalw synth.defs "G<=H ==> synth(G) <= synth(H)";
paulson@1839
   592
by (rtac lfp_mono 1);
paulson@1839
   593
by (REPEAT (ares_tac basic_monos 1));
paulson@1913
   594
qed "synth_mono";
paulson@1839
   595
paulson@1839
   596
(** Unions **)
paulson@1839
   597
paulson@1913
   598
(*Converse fails: we can synth more from the union than from the 
paulson@1839
   599
  separate parts, building a compound message using elements of each.*)
paulson@5076
   600
Goal "synth(G) Un synth(H) <= synth(G Un H)";
paulson@1913
   601
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
paulson@1913
   602
qed "synth_Un";
paulson@1839
   603
paulson@5076
   604
Goal "insert X (synth H) <= synth(insert X H)";
wenzelm@4091
   605
by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
paulson@1913
   606
qed "synth_insert";
paulson@1885
   607
paulson@1839
   608
(** Idempotence and transitivity **)
paulson@1839
   609
paulson@5114
   610
Goal "X: synth (synth H) ==> X: synth H";
paulson@2032
   611
by (etac synth.induct 1);
paulson@2891
   612
by (ALLGOALS Blast_tac);
paulson@2922
   613
qed "synth_synthD";
paulson@2922
   614
AddSDs [synth_synthD];
paulson@1839
   615
paulson@5076
   616
Goal "synth (synth H) = synth H";
paulson@2891
   617
by (Blast_tac 1);
paulson@1913
   618
qed "synth_idem";
paulson@1839
   619
paulson@5114
   620
Goal "[| X: synth G;  G <= synth H |] ==> X: synth H";
paulson@1913
   621
by (dtac synth_mono 1);
paulson@2891
   622
by (Blast_tac 1);
paulson@1913
   623
qed "synth_trans";
paulson@1839
   624
paulson@1839
   625
(*Cut; Lemma 2 of Lowe*)
paulson@5114
   626
Goal "[| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
paulson@2032
   627
by (etac synth_trans 1);
paulson@2891
   628
by (Blast_tac 1);
paulson@1913
   629
qed "synth_cut";
paulson@1839
   630
paulson@5076
   631
Goal "Agent A : synth H";
paulson@2891
   632
by (Blast_tac 1);
paulson@1946
   633
qed "Agent_synth";
paulson@1946
   634
paulson@5076
   635
Goal "Number n : synth H";
paulson@3668
   636
by (Blast_tac 1);
paulson@3668
   637
qed "Number_synth";
paulson@3668
   638
paulson@5076
   639
Goal "(Nonce N : synth H) = (Nonce N : H)";
paulson@2891
   640
by (Blast_tac 1);
paulson@1913
   641
qed "Nonce_synth_eq";
paulson@1839
   642
paulson@5076
   643
Goal "(Key K : synth H) = (Key K : H)";
paulson@2891
   644
by (Blast_tac 1);
paulson@1913
   645
qed "Key_synth_eq";
paulson@1839
   646
paulson@5114
   647
Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
paulson@2891
   648
by (Blast_tac 1);
paulson@2011
   649
qed "Crypt_synth_eq";
paulson@2011
   650
paulson@3668
   651
Addsimps [Agent_synth, Number_synth, 
paulson@3668
   652
	  Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
paulson@1839
   653
paulson@1839
   654
paulson@5076
   655
Goalw [keysFor_def]
paulson@1913
   656
    "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
paulson@2891
   657
by (Blast_tac 1);
paulson@1913
   658
qed "keysFor_synth";
paulson@1913
   659
Addsimps [keysFor_synth];
paulson@1839
   660
paulson@1839
   661
paulson@1913
   662
(*** Combinations of parts, analz and synth ***)
paulson@1839
   663
paulson@5076
   664
Goal "parts (synth H) = parts H Un synth H";
paulson@2032
   665
by (rtac equalityI 1);
paulson@2032
   666
by (rtac subsetI 1);
paulson@2032
   667
by (etac parts.induct 1);
paulson@1839
   668
by (ALLGOALS
wenzelm@4091
   669
    (blast_tac (claset() addIs ((synth_increasing RS parts_mono RS subsetD)
paulson@4556
   670
				::parts.intrs))));
paulson@1913
   671
qed "parts_synth";
paulson@1913
   672
Addsimps [parts_synth];
paulson@1839
   673
paulson@5076
   674
Goal "analz (analz G Un H) = analz (G Un H)";
paulson@2373
   675
by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
paulson@2373
   676
by (ALLGOALS Simp_tac);
paulson@2373
   677
qed "analz_analz_Un";
paulson@2373
   678
paulson@5076
   679
Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
paulson@2032
   680
by (rtac equalityI 1);
paulson@2032
   681
by (rtac subsetI 1);
paulson@2032
   682
by (etac analz.induct 1);
wenzelm@4091
   683
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5);
wenzelm@4091
   684
by (ALLGOALS (blast_tac (claset() addIs analz.intrs)));
paulson@2373
   685
qed "analz_synth_Un";
paulson@2373
   686
paulson@5076
   687
Goal "analz (synth H) = analz H Un synth H";
paulson@2373
   688
by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
paulson@2373
   689
by (Full_simp_tac 1);
paulson@1913
   690
qed "analz_synth";
paulson@2373
   691
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
paulson@1839
   692
paulson@1946
   693
paulson@1946
   694
(** For reasoning about the Fake rule in traces **)
paulson@1946
   695
paulson@5114
   696
Goal "X: G ==> parts(insert X H) <= parts G Un parts H";
paulson@2032
   697
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
paulson@2891
   698
by (Blast_tac 1);
paulson@1929
   699
qed "parts_insert_subset_Un";
paulson@1929
   700
paulson@4556
   701
(*More specifically for Fake.  Very occasionally we could do with a version
paulson@4556
   702
  of the form  parts{X} <= synth (analz H) Un parts H *)
paulson@5114
   703
Goal "X: synth (analz H) ==> \
paulson@5114
   704
\     parts (insert X H) <= synth (analz H) Un parts H";
paulson@2032
   705
by (dtac parts_insert_subset_Un 1);
paulson@1946
   706
by (Full_simp_tac 1);
paulson@2891
   707
by (Blast_tac 1);
paulson@1946
   708
qed "Fake_parts_insert";
paulson@1946
   709
paulson@4556
   710
(*H is sometimes (Key `` KK Un spies evs), so can't put G=H*)
paulson@5114
   711
Goal "X: synth (analz G) ==> \
paulson@5114
   712
\     analz (insert X H) <= synth (analz G) Un analz (G Un H)";
paulson@2373
   713
by (rtac subsetI 1);
paulson@2373
   714
by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
wenzelm@4091
   715
by (blast_tac (claset() addIs [impOfSubs analz_mono,
paulson@4556
   716
			       impOfSubs (analz_mono RS synth_mono)]) 2);
paulson@2373
   717
by (Full_simp_tac 1);
paulson@2891
   718
by (Blast_tac 1);
paulson@2373
   719
qed "Fake_analz_insert";
paulson@2373
   720
paulson@5076
   721
Goal "(X: analz H & X: parts H) = (X: analz H)";
wenzelm@4091
   722
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
paulson@2011
   723
val analz_conj_parts = result();
paulson@2011
   724
paulson@5076
   725
Goal "(X: analz H | X: parts H) = (X: parts H)";
wenzelm@4091
   726
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
paulson@2011
   727
val analz_disj_parts = result();
paulson@2011
   728
paulson@2011
   729
AddIffs [analz_conj_parts, analz_disj_parts];
paulson@2011
   730
paulson@1998
   731
(*Without this equation, other rules for synth and analz would yield
paulson@1998
   732
  redundant cases*)
paulson@5076
   733
Goal "({|X,Y|} : synth (analz H)) = \
paulson@5114
   734
\     (X : synth (analz H) & Y : synth (analz H))";
paulson@2891
   735
by (Blast_tac 1);
paulson@1998
   736
qed "MPair_synth_analz";
paulson@1998
   737
paulson@1998
   738
AddIffs [MPair_synth_analz];
paulson@1929
   739
paulson@5114
   740
Goal "[| Key K : analz H;  Key (invKey K) : analz H |] \
paulson@5114
   741
\      ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
paulson@2891
   742
by (Blast_tac 1);
paulson@2154
   743
qed "Crypt_synth_analz";
paulson@2154
   744
paulson@1929
   745
paulson@5114
   746
Goal "X ~: synth (analz H) \
paulson@5114
   747
\     ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
paulson@2891
   748
by (Blast_tac 1);
paulson@2373
   749
qed "Hash_synth_analz";
paulson@2373
   750
Addsimps [Hash_synth_analz];
paulson@2373
   751
paulson@2373
   752
paulson@2484
   753
(**** HPair: a combination of Hash and MPair ****)
paulson@2484
   754
paulson@2484
   755
(*** Freeness ***)
paulson@2484
   756
paulson@5076
   757
Goalw [HPair_def] "Agent A ~= Hash[X] Y";
paulson@2484
   758
by (Simp_tac 1);
paulson@2484
   759
qed "Agent_neq_HPair";
paulson@2484
   760
paulson@5076
   761
Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
paulson@2484
   762
by (Simp_tac 1);
paulson@2484
   763
qed "Nonce_neq_HPair";
paulson@2484
   764
paulson@5076
   765
Goalw [HPair_def] "Number N ~= Hash[X] Y";
paulson@3668
   766
by (Simp_tac 1);
paulson@3668
   767
qed "Number_neq_HPair";
paulson@3668
   768
paulson@5076
   769
Goalw [HPair_def] "Key K ~= Hash[X] Y";
paulson@2484
   770
by (Simp_tac 1);
paulson@2484
   771
qed "Key_neq_HPair";
paulson@2484
   772
paulson@5076
   773
Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
paulson@2484
   774
by (Simp_tac 1);
paulson@2484
   775
qed "Hash_neq_HPair";
paulson@2484
   776
paulson@5076
   777
Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
paulson@2484
   778
by (Simp_tac 1);
paulson@2484
   779
qed "Crypt_neq_HPair";
paulson@2484
   780
paulson@3668
   781
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, 
paulson@2516
   782
                  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
paulson@2484
   783
paulson@2484
   784
AddIffs HPair_neqs;
paulson@2484
   785
AddIffs (HPair_neqs RL [not_sym]);
paulson@2484
   786
paulson@5076
   787
Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
paulson@2484
   788
by (Simp_tac 1);
paulson@2484
   789
qed "HPair_eq";
paulson@2484
   790
paulson@5076
   791
Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
paulson@2484
   792
by (Simp_tac 1);
paulson@2484
   793
qed "MPair_eq_HPair";
paulson@2484
   794
paulson@5076
   795
Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
paulson@4477
   796
by Auto_tac;
paulson@2484
   797
qed "HPair_eq_MPair";
paulson@2484
   798
paulson@2484
   799
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
paulson@2484
   800
paulson@2484
   801
paulson@2484
   802
(*** Specialized laws, proved in terms of those for Hash and MPair ***)
paulson@2484
   803
paulson@5076
   804
Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
paulson@2484
   805
by (Simp_tac 1);
paulson@2484
   806
qed "keysFor_insert_HPair";
paulson@2484
   807
paulson@5076
   808
Goalw [HPair_def]
paulson@2516
   809
    "parts (insert (Hash[X] Y) H) = \
paulson@2516
   810
\    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
paulson@2484
   811
by (Simp_tac 1);
paulson@2484
   812
qed "parts_insert_HPair";
paulson@2484
   813
paulson@5076
   814
Goalw [HPair_def]
paulson@2516
   815
    "analz (insert (Hash[X] Y) H) = \
paulson@2516
   816
\    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
paulson@2484
   817
by (Simp_tac 1);
paulson@2484
   818
qed "analz_insert_HPair";
paulson@2484
   819
paulson@5114
   820
Goalw [HPair_def] "X ~: synth (analz H) \
paulson@2516
   821
\   ==> (Hash[X] Y : synth (analz H)) = \
paulson@2484
   822
\       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
paulson@2484
   823
by (Simp_tac 1);
paulson@2891
   824
by (Blast_tac 1);
paulson@2484
   825
qed "HPair_synth_analz";
paulson@2484
   826
paulson@2484
   827
Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
paulson@2516
   828
          HPair_synth_analz, HPair_synth_analz];
paulson@2484
   829
paulson@2484
   830
paulson@1929
   831
(*We do NOT want Crypt... messages broken up in protocols!!*)
paulson@1929
   832
Delrules partsEs;
paulson@1929
   833
paulson@2327
   834
paulson@2327
   835
(** Rewrites to push in Key and Crypt messages, so that other messages can
paulson@2327
   836
    be pulled out using the analz_insert rules **)
paulson@2327
   837
paulson@2327
   838
fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
paulson@2327
   839
                          insert_commute;
paulson@2327
   840
paulson@2327
   841
val pushKeys = map (insComm thy "Key ?K") 
paulson@3668
   842
                   ["Agent ?C", "Nonce ?N", "Number ?N", 
paulson@3668
   843
		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
paulson@2327
   844
paulson@2327
   845
val pushCrypts = map (insComm thy "Crypt ?X ?K") 
paulson@3668
   846
                     ["Agent ?C", "Nonce ?N", "Number ?N", 
paulson@3668
   847
		      "Hash ?X'", "MPair ?X' ?Y"];
paulson@2327
   848
paulson@2327
   849
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
paulson@2327
   850
val pushes = pushKeys@pushCrypts;
paulson@2327
   851
paulson@3121
   852
paulson@3121
   853
(*** Tactics useful for many protocol proofs ***)
paulson@3121
   854
paulson@3470
   855
(*Prove base case (subgoal i) and simplify others.  A typical base case
paulson@3683
   856
  concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
paulson@3470
   857
  alone.*)
paulson@3121
   858
fun prove_simple_subgoals_tac i = 
paulson@5421
   859
    Force_tac i THEN ALLGOALS Asm_simp_tac;
paulson@3121
   860
paulson@3121
   861
fun Fake_parts_insert_tac i = 
paulson@4556
   862
    blast_tac (claset() addIs [parts_insertI]
paulson@4556
   863
			addDs [impOfSubs analz_subset_parts,
paulson@4556
   864
			       impOfSubs Fake_parts_insert]) i;
paulson@3121
   865
paulson@3121
   866
(*Apply rules to break down assumptions of the form
paulson@3121
   867
  Y : parts(insert X H)  and  Y : analz(insert X H)
paulson@3121
   868
*)
paulson@2373
   869
val Fake_insert_tac = 
paulson@2373
   870
    dresolve_tac [impOfSubs Fake_analz_insert,
paulson@2516
   871
                  impOfSubs Fake_parts_insert] THEN'
paulson@2373
   872
    eresolve_tac [asm_rl, synth.Inj];
paulson@2373
   873
paulson@3702
   874
fun Fake_insert_simp_tac i = 
paulson@3702
   875
    REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i;
paulson@3702
   876
paulson@3702
   877
paulson@3449
   878
(*Analysis of Fake cases.  Also works for messages that forward unknown parts,
paulson@3449
   879
  but this application is no longer necessary if analz_insert_eq is used.
paulson@2327
   880
  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
paulson@2327
   881
  DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
paulson@4735
   882
paulson@4735
   883
val atomic_spy_analz_tac = SELECT_GOAL
paulson@4735
   884
    (Fake_insert_simp_tac 1
paulson@4735
   885
     THEN
paulson@4735
   886
     IF_UNSOLVED (Blast.depth_tac
paulson@4735
   887
		  (claset() addIs [analz_insertI,
paulson@4735
   888
				   impOfSubs analz_subset_parts]) 4 1));
paulson@4735
   889
paulson@2327
   890
fun spy_analz_tac i =
paulson@2373
   891
  DETERM
paulson@2373
   892
   (SELECT_GOAL
paulson@2373
   893
     (EVERY 
paulson@2373
   894
      [  (*push in occurrences of X...*)
paulson@2373
   895
       (REPEAT o CHANGED)
paulson@2373
   896
           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
paulson@2373
   897
       (*...allowing further simplifications*)
nipkow@4686
   898
       Simp_tac 1,
paulson@3476
   899
       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
paulson@4735
   900
       DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
paulson@4735
   901
paulson@2327
   902
paulson@2415
   903
(** Useful in many uniqueness proofs **)
paulson@2327
   904
fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
paulson@2327
   905
                     assume_tac (i+1);
paulson@2327
   906
paulson@6915
   907
(*Apply the EX-ALL quantification to prove uniqueness theorems in 
paulson@2415
   908
  their standard form*)
paulson@2415
   909
fun prove_unique_tac lemma = 
paulson@2415
   910
  EVERY' [dtac lemma,
paulson@2516
   911
          REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
paulson@2516
   912
          (*Duplicate the assumption*)
paulson@2516
   913
          forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
wenzelm@4091
   914
          Blast.depth_tac (claset() addSDs [spec]) 0];
paulson@2415
   915
paulson@2373
   916
paulson@2373
   917
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
paulson@2373
   918
goal Set.thy "A Un (B Un A) = B Un A";
paulson@2891
   919
by (Blast_tac 1);
paulson@2373
   920
val Un_absorb3 = result();
paulson@2373
   921
Addsimps [Un_absorb3];
paulson@3514
   922
paulson@3514
   923
(*By default only o_apply is built-in.  But in the presence of eta-expansion
paulson@3514
   924
  this means that some terms displayed as (f o g) will be rewritten, and others
paulson@3514
   925
  will not!*)
paulson@3514
   926
Addsimps [o_def];