src/HOL/Auth/Shared.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2891 d8f254ad1ab9
child 2922 580647a879cf
permissions -rw-r--r--
Dep. on Provers/nat_transitive
paulson@2320
     1
(*  Title:      HOL/Auth/Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Theory of Shared Keys (common to all symmetric-key protocols)
paulson@1934
     7
paulson@1934
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
paulson@2032
     9
*)
paulson@2032
    10
paulson@1934
    11
paulson@1934
    12
open Shared;
paulson@1934
    13
paulson@1964
    14
(*Holds because Friend is injective: thus cannot prove for all f*)
paulson@1964
    15
goal thy "(Friend x : Friend``A) = (x:A)";
paulson@1964
    16
by (Auto_tac());
paulson@1964
    17
qed "Friend_image_eq";
paulson@1964
    18
Addsimps [Friend_image_eq];
paulson@1964
    19
paulson@1934
    20
Addsimps [Un_insert_left, Un_insert_right];
paulson@1934
    21
paulson@1934
    22
(*By default only o_apply is built-in.  But in the presence of eta-expansion
paulson@1934
    23
  this means that some terms displayed as (f o g) will be rewritten, and others
paulson@1934
    24
  will not!*)
paulson@1934
    25
Addsimps [o_def];
paulson@1934
    26
paulson@1943
    27
(*** Basic properties of shrK and newK ***)
paulson@1934
    28
paulson@2451
    29
(*Injectiveness and freshness of new keys and nonces*)
paulson@2451
    30
AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, 
paulson@2516
    31
         inj_newK RS inj_eq, inj_nPair RS inj_eq];
paulson@2376
    32
paulson@1943
    33
(* invKey (shrK A) = shrK A *)
paulson@2516
    34
bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys);
paulson@1934
    35
paulson@2516
    36
Addsimps [invKey_id];
paulson@2376
    37
paulson@2451
    38
goal thy "!!K. newK i = invKey K ==> newK i = K";
paulson@2376
    39
by (rtac (invKey_eq RS iffD1) 1);
paulson@2516
    40
by (Full_simp_tac 1);
paulson@2376
    41
val newK_invKey = result();
paulson@2376
    42
paulson@2376
    43
AddSDs [newK_invKey, sym RS newK_invKey];
paulson@1934
    44
paulson@2451
    45
Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
paulson@2320
    46
paulson@1934
    47
(** Rewrites should not refer to  initState(Friend i) 
paulson@1934
    48
    -- not in normal form! **)
paulson@1934
    49
paulson@2451
    50
goal thy "Key (newK i) ~: parts (initState lost B)";
paulson@2032
    51
by (agent.induct_tac "B" 1);
paulson@1934
    52
by (Auto_tac ());
paulson@2032
    53
qed "newK_notin_initState";
paulson@1934
    54
paulson@2516
    55
AddIffs [newK_notin_initState];
paulson@1934
    56
paulson@2032
    57
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
paulson@1934
    58
by (agent.induct_tac "C" 1);
paulson@1993
    59
by (auto_tac (!claset addIs [range_eqI], !simpset));
paulson@1934
    60
qed "keysFor_parts_initState";
paulson@1934
    61
Addsimps [keysFor_parts_initState];
paulson@1934
    62
paulson@1934
    63
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
paulson@1934
    64
by (Auto_tac ());
paulson@1934
    65
qed "keysFor_image_Key";
paulson@1934
    66
Addsimps [keysFor_image_Key];
paulson@1934
    67
paulson@1943
    68
goal thy "shrK A ~: newK``E";
paulson@1934
    69
by (agent.induct_tac "A" 1);
paulson@1934
    70
by (Auto_tac ());
paulson@1943
    71
qed "shrK_notin_image_newK";
paulson@1943
    72
Addsimps [shrK_notin_image_newK];
paulson@1934
    73
paulson@2032
    74
paulson@2032
    75
(*** Function "sees" ***)
paulson@2032
    76
paulson@2032
    77
goal thy
paulson@2032
    78
    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
paulson@2032
    79
by (list.induct_tac "evs" 1);
paulson@2032
    80
by (agent.induct_tac "A" 1);
paulson@2032
    81
by (event.induct_tac "a" 2);
paulson@2032
    82
by (Auto_tac ());
paulson@2032
    83
qed "sees_mono";
paulson@2032
    84
paulson@1964
    85
(*Agents see their own shared keys!*)
paulson@2032
    86
goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
paulson@1934
    87
by (list.induct_tac "evs" 1);
paulson@1934
    88
by (agent.induct_tac "A" 1);
paulson@2032
    89
by (Auto_tac ());
paulson@2032
    90
qed_spec_mp "sees_own_shrK";
paulson@1934
    91
paulson@2032
    92
(*Spy sees shared keys of lost agents!*)
paulson@2045
    93
goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
paulson@2032
    94
by (list.induct_tac "evs" 1);
paulson@2032
    95
by (Auto_tac());
paulson@2045
    96
qed "Spy_sees_lost";
paulson@1934
    97
paulson@2045
    98
AddSIs [sees_own_shrK, Spy_sees_lost];
paulson@2032
    99
paulson@2124
   100
(*Added for Yahalom/lost_tac*)
paulson@2284
   101
goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs);  A: lost |] \
paulson@2124
   102
\              ==> X : analz (sees lost Spy evs)";
paulson@2124
   103
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
paulson@2124
   104
qed "Crypt_Spy_analz_lost";
paulson@2124
   105
paulson@2032
   106
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
paulson@2026
   107
paulson@2078
   108
goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
paulson@1934
   109
by (Simp_tac 1);
paulson@1934
   110
qed "sees_own";
paulson@1934
   111
paulson@2078
   112
goal thy "!!A. Server ~= B ==> \
paulson@2078
   113
\          sees lost Server (Says A B X # evs) = sees lost Server evs";
paulson@1934
   114
by (Asm_simp_tac 1);
paulson@1934
   115
qed "sees_Server";
paulson@1934
   116
paulson@2078
   117
goal thy "!!A. Friend i ~= B ==> \
paulson@2078
   118
\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
paulson@1934
   119
by (Asm_simp_tac 1);
paulson@1934
   120
qed "sees_Friend";
paulson@1934
   121
paulson@2032
   122
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
paulson@1934
   123
by (Simp_tac 1);
paulson@2032
   124
qed "sees_Spy";
paulson@1934
   125
paulson@2032
   126
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
paulson@1934
   127
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@2891
   128
by (Blast_tac 1);
paulson@1934
   129
qed "sees_Says_subset_insert";
paulson@1934
   130
paulson@2032
   131
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
paulson@1934
   132
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@2891
   133
by (Blast_tac 1);
paulson@1934
   134
qed "sees_subset_sees_Says";
paulson@1934
   135
paulson@2132
   136
(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
paulson@2160
   137
  Once used to prove new_keys_not_seen; now obsolete.*)
paulson@2032
   138
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
paulson@2032
   139
\         parts {Y} Un (UN A. parts (sees lost A evs))";
paulson@1934
   140
by (Step_tac 1);
paulson@2132
   141
by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
paulson@2132
   142
by (ALLGOALS
oheimb@2637
   143
    (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
paulson@2891
   144
				            setloop split_tac [expand_if]))));
paulson@1934
   145
qed "UN_parts_sees_Says";
paulson@1934
   146
paulson@2032
   147
goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
paulson@1934
   148
by (list.induct_tac "evs" 1);
paulson@1934
   149
by (Auto_tac ());
paulson@2032
   150
qed_spec_mp "Says_imp_sees_Spy";
paulson@1934
   151
paulson@2516
   152
(*Use with addSEs to derive contradictions from old Says events containing
paulson@2516
   153
  items known to be fresh*)
paulson@2516
   154
val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
paulson@2516
   155
paulson@2064
   156
goal thy  
paulson@2284
   157
 "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
paulson@2064
   158
\        ==> X : analz (sees lost Spy evs)";
paulson@2064
   159
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
oheimb@2637
   160
                      unsafe_addss (!simpset)) 1);
paulson@2064
   161
qed "Says_Crypt_lost";
paulson@2064
   162
paulson@2072
   163
goal thy  
paulson@2284
   164
 "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;        \
paulson@2072
   165
\           X ~: analz (sees lost Spy evs) |]                     \
paulson@2072
   166
\        ==> C ~: lost";
paulson@2072
   167
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
oheimb@2637
   168
                      unsafe_addss (!simpset)) 1);
paulson@2072
   169
qed "Says_Crypt_not_lost";
paulson@2072
   170
paulson@2320
   171
(*NEEDED??*)
paulson@2032
   172
goal thy "initState lost C <= Key `` range shrK";
paulson@1934
   173
by (agent.induct_tac "C" 1);
paulson@1934
   174
by (Auto_tac ());
paulson@1934
   175
qed "initState_subset";
paulson@1934
   176
paulson@2320
   177
(*NEEDED??*)
paulson@2032
   178
goal thy "X : sees lost C evs --> \
paulson@2078
   179
\          (EX A B. Says A B X : set_of_list evs) | (EX A. X = Key (shrK A))";
paulson@1934
   180
by (list.induct_tac "evs" 1);
paulson@1934
   181
by (ALLGOALS Asm_simp_tac);
paulson@2891
   182
by (blast_tac (!claset addDs [impOfSubs initState_subset]) 1);
paulson@2032
   183
by (rtac conjI 1);
paulson@2891
   184
by (Blast_tac 2);
paulson@1934
   185
by (event.induct_tac "a" 1);
paulson@1934
   186
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
paulson@2891
   187
by (ALLGOALS Blast_tac);
paulson@1934
   188
qed_spec_mp "seesD";
paulson@1934
   189
paulson@2160
   190
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
paulson@2032
   191
Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
paulson@1934
   192
paulson@1934
   193
paulson@2516
   194
(*** Fresh nonces ***)
paulson@2516
   195
paulson@2516
   196
goal thy "Nonce N ~: parts (initState lost B)";
paulson@2516
   197
by (agent.induct_tac "B" 1);
paulson@2516
   198
by (Auto_tac ());
paulson@2516
   199
qed "Nonce_notin_initState";
paulson@2516
   200
paulson@2516
   201
AddIffs [Nonce_notin_initState];
paulson@2516
   202
paulson@2516
   203
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
paulson@2516
   204
by (etac (impOfSubs parts_mono) 1);
paulson@2891
   205
by (Blast_tac 1);
paulson@2516
   206
qed "usedI";
paulson@2516
   207
paulson@2516
   208
AddIs [usedI];
paulson@2516
   209
paulson@2516
   210
(** Fresh keys never clash with long-term shared keys **)
paulson@2516
   211
paulson@2516
   212
goal thy "Key (shrK A) : used evs";
paulson@2516
   213
by (Best_tac 1);
paulson@2516
   214
qed "shrK_in_used";
paulson@2516
   215
AddIffs [shrK_in_used];
paulson@2516
   216
paulson@2516
   217
(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys
paulson@2516
   218
  from long-term shared keys*)
paulson@2516
   219
goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
paulson@2516
   220
by (Best_tac 1);
paulson@2516
   221
qed "Key_not_used";
paulson@2516
   222
paulson@2516
   223
(*A session key cannot clash with a long-term shared key*)
paulson@2516
   224
goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
paulson@2891
   225
by (Blast_tac 1);
paulson@2516
   226
qed "shrK_neq";
paulson@2516
   227
paulson@2516
   228
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
paulson@2516
   229
paulson@2516
   230
paulson@2516
   231
goal thy "used (Says A B X # evs) = parts{X} Un used evs";
paulson@2516
   232
by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
paulson@2516
   233
qed "used_Says";
paulson@2516
   234
Addsimps [used_Says];
paulson@2516
   235
paulson@2516
   236
goal thy "used [] <= used l";
paulson@2516
   237
by (list.induct_tac "l" 1);
paulson@2516
   238
by (event.induct_tac "a" 2);
paulson@2516
   239
by (ALLGOALS Asm_simp_tac);
paulson@2516
   240
by (Best_tac 1);
paulson@2516
   241
qed "used_nil_subset";
paulson@2516
   242
paulson@2516
   243
goal thy "used l <= used (l@l')";
paulson@2516
   244
by (list.induct_tac "l" 1);
paulson@2516
   245
by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
paulson@2516
   246
by (event.induct_tac "a" 1);
paulson@2516
   247
by (Asm_simp_tac 1);
paulson@2516
   248
by (Best_tac 1);
paulson@2516
   249
qed "used_subset_append";
paulson@2516
   250
paulson@2516
   251
paulson@2516
   252
(*** Supply fresh nonces for possibility theorems. ***)
paulson@2516
   253
paulson@2516
   254
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
paulson@2516
   255
by (list.induct_tac "evs" 1);
paulson@2516
   256
by (res_inst_tac [("x","0")] exI 1);
paulson@2516
   257
by (Step_tac 1);
paulson@2516
   258
by (Full_simp_tac 1);
paulson@2516
   259
(*Inductive step*)
paulson@2516
   260
by (event.induct_tac "a" 1);
paulson@2516
   261
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
paulson@2516
   262
by (msg.induct_tac "msg" 1);
paulson@2516
   263
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
paulson@2516
   264
by (Step_tac 1);
paulson@2516
   265
(*MPair case*)
paulson@2516
   266
by (res_inst_tac [("x","Na+Nb")] exI 2);
paulson@2891
   267
by (blast_tac (!claset addSEs [add_leE]) 2);
paulson@2516
   268
(*Nonce case*)
paulson@2516
   269
by (res_inst_tac [("x","N + Suc nat")] exI 1);
oheimb@2637
   270
by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
paulson@2516
   271
val lemma = result();
paulson@2516
   272
paulson@2516
   273
goal thy "EX N. Nonce N ~: used evs";
paulson@2516
   274
by (rtac (lemma RS exE) 1);
paulson@2891
   275
by (Blast_tac 1);
paulson@2516
   276
qed "Nonce_supply1";
paulson@2516
   277
paulson@2516
   278
goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
paulson@2516
   279
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   280
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   281
by (Step_tac 1);
paulson@2516
   282
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   283
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   284
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   285
				     le_add2, le_add1, 
paulson@2516
   286
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   287
qed "Nonce_supply2";
paulson@2516
   288
paulson@2516
   289
goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
paulson@2516
   290
\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
paulson@2516
   291
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   292
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   293
by (cut_inst_tac [("evs","evs''")] lemma 1);
paulson@2516
   294
by (Step_tac 1);
paulson@2516
   295
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   296
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   297
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
paulson@2516
   298
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   299
				     le_add2, le_add1, 
paulson@2516
   300
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   301
by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
paulson@2516
   302
by (stac (le_eq_less_Suc RS sym) 1);
paulson@2516
   303
by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
paulson@2516
   304
by (REPEAT (rtac le_add1 1));
paulson@2516
   305
qed "Nonce_supply3";
paulson@2516
   306
paulson@2516
   307
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
paulson@2516
   308
by (rtac (lemma RS exE) 1);
paulson@2516
   309
by (rtac selectI 1);
paulson@2891
   310
by (Blast_tac 1);
paulson@2516
   311
qed "Nonce_supply";
paulson@2516
   312
paulson@2516
   313
(*** Supply fresh keys for possibility theorems. ***)
paulson@2516
   314
paulson@2516
   315
goal thy "EX K. Key K ~: used evs";
paulson@2516
   316
by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
paulson@2891
   317
by (Blast_tac 1);
paulson@2516
   318
qed "Key_supply1";
paulson@2516
   319
paulson@2516
   320
val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
paulson@2516
   321
paulson@2516
   322
goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
paulson@2516
   323
by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
paulson@2516
   324
by (etac exE 1);
paulson@2516
   325
by (cut_inst_tac [("evs","evs'")] 
paulson@2516
   326
    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
paulson@2516
   327
by (Auto_tac());
paulson@2516
   328
qed "Key_supply2";
paulson@2516
   329
paulson@2516
   330
goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
paulson@2516
   331
\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
paulson@2516
   332
by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1);
paulson@2516
   333
by (etac exE 1);
paulson@2516
   334
by (cut_inst_tac [("evs","evs'")] 
paulson@2516
   335
    (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
paulson@2516
   336
by (etac exE 1);
paulson@2516
   337
by (cut_inst_tac [("evs","evs''")] 
paulson@2516
   338
    (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1);
paulson@2516
   339
by (Step_tac 1);
paulson@2516
   340
by (Full_simp_tac 1);
paulson@2516
   341
by (fast_tac (!claset addSEs [allE]) 1);
paulson@2516
   342
qed "Key_supply3";
paulson@2516
   343
paulson@2516
   344
goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
paulson@2516
   345
by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
paulson@2516
   346
by (rtac selectI 1);
paulson@2891
   347
by (Blast_tac 1);
paulson@2516
   348
qed "Key_supply";
paulson@2516
   349
paulson@2516
   350
(*** Tactics for possibility theorems ***)
paulson@2516
   351
paulson@2516
   352
val possibility_tac =
paulson@2516
   353
    REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
paulson@2516
   354
    (ALLGOALS (simp_tac 
oheimb@2637
   355
               (!simpset delsimps [used_Says] setSolver safe_solver))
paulson@2516
   356
     THEN
paulson@2516
   357
     REPEAT_FIRST (eq_assume_tac ORELSE' 
paulson@2516
   358
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
paulson@2516
   359
paulson@2516
   360
(*For harder protocols (such as Recur) where we have to set up some
paulson@2516
   361
  nonces and keys initially*)
paulson@2516
   362
val basic_possibility_tac =
paulson@2516
   363
    REPEAT 
oheimb@2637
   364
    (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
paulson@2516
   365
     THEN
paulson@2516
   366
     REPEAT_FIRST (resolve_tac [refl, conjI]));
paulson@2516
   367
paulson@2516
   368
paulson@2049
   369
(** Power of the Spy **)
paulson@1934
   370
paulson@2049
   371
(*The Spy can see more than anybody else, except for their initial state*)
paulson@2049
   372
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
paulson@2049
   373
by (list.induct_tac "evs" 1);
paulson@2049
   374
by (event.induct_tac "a" 2);
paulson@2049
   375
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
paulson@2049
   376
                                addss (!simpset))));
paulson@2049
   377
qed "sees_agent_subset_sees_Spy";
paulson@2049
   378
paulson@2049
   379
(*The Spy can see more than anybody else who's lost their key!*)
paulson@2049
   380
goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
paulson@2049
   381
by (list.induct_tac "evs" 1);
paulson@2049
   382
by (event.induct_tac "a" 2);
paulson@2049
   383
by (agent.induct_tac "A" 1);
paulson@2049
   384
by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
paulson@2049
   385
qed_spec_mp "sees_lost_agent_subset_sees_Spy";
paulson@2049
   386
paulson@1934
   387
paulson@2032
   388
(** Simplifying   parts (insert X (sees lost A evs))
paulson@2045
   389
      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
paulson@2012
   390
paulson@2012
   391
val parts_insert_sees = 
paulson@2045
   392
    parts_insert |> read_instantiate_sg (sign_of thy)
paulson@2045
   393
                                        [("H", "sees lost A evs")]
paulson@2012
   394
                 |> standard;
paulson@2045
   395
paulson@2045
   396
paulson@2049
   397
(*** Specialized rewriting for analz_insert_Key_newK ***)
paulson@2049
   398
paulson@2320
   399
(*Push newK applications in, allowing other keys to be pulled out*)
paulson@2320
   400
val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
paulson@2320
   401
paulson@2516
   402
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
paulson@2891
   403
by (Blast_tac 1);
paulson@2516
   404
qed "subset_Compl_range";
paulson@2045
   405
paulson@2516
   406
goal thy "insert (Key K) H = Key `` {K} Un H";
paulson@2891
   407
by (Blast_tac 1);
paulson@2516
   408
qed "insert_Key_singleton";
paulson@2516
   409
paulson@2516
   410
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
paulson@2891
   411
by (Blast_tac 1);
paulson@2891
   412
qed "insert_Key_image";
paulson@2516
   413
paulson@2516
   414
val analz_image_freshK_ss = 
paulson@2516
   415
     !simpset delsimps [image_insert, image_Un]
paulson@2516
   416
              addsimps ([image_insert RS sym, image_Un RS sym,
paulson@2516
   417
                         Key_not_used, 
paulson@2516
   418
                         insert_Key_singleton, subset_Compl_range,
paulson@2891
   419
                         insert_Key_image, Un_assoc RS sym]
paulson@2516
   420
                        @disj_comms)
paulson@2516
   421
              setloop split_tac [expand_if];
paulson@2045
   422
paulson@2045
   423
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@2045
   424
goal thy  
paulson@2045
   425
 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
paulson@2045
   426
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
paulson@2045
   427
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
paulson@2516
   428
qed "analz_image_freshK_lemma";