src/HOL/Auth/Shared.ML
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3479 2aacd6f10654
child 3512 9dcb4daa15e8
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
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@3472
     8
Server keys; initial states of agents; freshness; 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@3472
    27
(*** Basic properties of shrK ***)
paulson@1934
    28
paulson@3472
    29
(*Injectiveness: Agents' long-term keys are distinct.*)
paulson@3472
    30
AddIffs [inj_shrK RS inj_eq];
paulson@2376
    31
paulson@3472
    32
(* invKey(shrK A) = shrK A *)
paulson@3472
    33
Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
paulson@2320
    34
paulson@1934
    35
(** Rewrites should not refer to  initState(Friend i) 
paulson@1934
    36
    -- not in normal form! **)
paulson@1934
    37
paulson@2032
    38
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
paulson@1934
    39
by (agent.induct_tac "C" 1);
paulson@3121
    40
by (Auto_tac ());
paulson@1934
    41
qed "keysFor_parts_initState";
paulson@1934
    42
Addsimps [keysFor_parts_initState];
paulson@1934
    43
paulson@1934
    44
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
paulson@1934
    45
by (Auto_tac ());
paulson@1934
    46
qed "keysFor_image_Key";
paulson@1934
    47
Addsimps [keysFor_image_Key];
paulson@1934
    48
paulson@2032
    49
paulson@2032
    50
(*** Function "sees" ***)
paulson@2032
    51
paulson@2032
    52
goal thy
paulson@2032
    53
    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
paulson@2032
    54
by (list.induct_tac "evs" 1);
paulson@2032
    55
by (agent.induct_tac "A" 1);
paulson@2032
    56
by (event.induct_tac "a" 2);
paulson@2032
    57
by (Auto_tac ());
paulson@2032
    58
qed "sees_mono";
paulson@2032
    59
paulson@1964
    60
(*Agents see their own shared keys!*)
paulson@2032
    61
goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
paulson@1934
    62
by (list.induct_tac "evs" 1);
paulson@1934
    63
by (agent.induct_tac "A" 1);
paulson@2032
    64
by (Auto_tac ());
paulson@2032
    65
qed_spec_mp "sees_own_shrK";
paulson@1934
    66
paulson@2032
    67
(*Spy sees shared keys of lost agents!*)
paulson@2045
    68
goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
paulson@2032
    69
by (list.induct_tac "evs" 1);
paulson@2032
    70
by (Auto_tac());
paulson@2045
    71
qed "Spy_sees_lost";
paulson@1934
    72
paulson@2045
    73
AddSIs [sees_own_shrK, Spy_sees_lost];
paulson@2032
    74
paulson@2032
    75
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
paulson@2026
    76
paulson@2078
    77
goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
paulson@1934
    78
by (Simp_tac 1);
paulson@1934
    79
qed "sees_own";
paulson@1934
    80
paulson@2078
    81
goal thy "!!A. Server ~= B ==> \
paulson@2078
    82
\          sees lost Server (Says A B X # evs) = sees lost Server evs";
paulson@1934
    83
by (Asm_simp_tac 1);
paulson@1934
    84
qed "sees_Server";
paulson@1934
    85
paulson@2078
    86
goal thy "!!A. Friend i ~= B ==> \
paulson@2078
    87
\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
paulson@1934
    88
by (Asm_simp_tac 1);
paulson@1934
    89
qed "sees_Friend";
paulson@1934
    90
paulson@2032
    91
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
paulson@1934
    92
by (Simp_tac 1);
paulson@2032
    93
qed "sees_Spy";
paulson@1934
    94
paulson@2032
    95
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
paulson@1934
    96
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@2891
    97
by (Blast_tac 1);
paulson@1934
    98
qed "sees_Says_subset_insert";
paulson@1934
    99
paulson@2032
   100
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
paulson@1934
   101
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@2891
   102
by (Blast_tac 1);
paulson@1934
   103
qed "sees_subset_sees_Says";
paulson@1934
   104
paulson@2132
   105
(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
paulson@2160
   106
  Once used to prove new_keys_not_seen; now obsolete.*)
paulson@2032
   107
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
paulson@2032
   108
\         parts {Y} Un (UN A. parts (sees lost A evs))";
paulson@1934
   109
by (Step_tac 1);
paulson@2132
   110
by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
paulson@2132
   111
by (ALLGOALS
oheimb@3207
   112
    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
paulson@2891
   113
				            setloop split_tac [expand_if]))));
paulson@1934
   114
qed "UN_parts_sees_Says";
paulson@1934
   115
nipkow@3465
   116
goal thy "Says A B X : set evs --> X : sees lost Spy evs";
paulson@1934
   117
by (list.induct_tac "evs" 1);
paulson@1934
   118
by (Auto_tac ());
paulson@2032
   119
qed_spec_mp "Says_imp_sees_Spy";
paulson@1934
   120
paulson@2516
   121
(*Use with addSEs to derive contradictions from old Says events containing
paulson@2516
   122
  items known to be fresh*)
paulson@2516
   123
val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
paulson@2516
   124
paulson@3443
   125
(*For not_lost_tac*)
paulson@3443
   126
goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs);  A: lost |] \
paulson@3443
   127
\              ==> X : analz (sees lost Spy evs)";
paulson@3443
   128
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
paulson@3443
   129
qed "Crypt_Spy_analz_lost";
paulson@2072
   130
paulson@3443
   131
(*Prove that the agent is uncompromised by the confidentiality of 
paulson@3443
   132
  a component of a message she's said.*)
paulson@3443
   133
fun not_lost_tac s =
paulson@3443
   134
    case_tac ("(" ^ s ^ ") : lost") THEN'
paulson@3443
   135
    SELECT_GOAL 
paulson@3443
   136
      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
paulson@3443
   137
       REPEAT_DETERM (etac MPair_analz 1) THEN
paulson@3443
   138
       THEN_BEST_FIRST 
paulson@3443
   139
         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
paulson@3443
   140
         (has_fewer_prems 1, size_of_thm)
paulson@3443
   141
         (Step_tac 1));
paulson@1934
   142
paulson@2160
   143
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
paulson@2032
   144
Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
paulson@1934
   145
paulson@1934
   146
paulson@2516
   147
(*** Fresh nonces ***)
paulson@2516
   148
paulson@2516
   149
goal thy "Nonce N ~: parts (initState lost B)";
paulson@2516
   150
by (agent.induct_tac "B" 1);
paulson@2516
   151
by (Auto_tac ());
paulson@2516
   152
qed "Nonce_notin_initState";
paulson@2516
   153
paulson@2516
   154
AddIffs [Nonce_notin_initState];
paulson@2516
   155
paulson@2516
   156
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
paulson@2516
   157
by (etac (impOfSubs parts_mono) 1);
paulson@2891
   158
by (Blast_tac 1);
paulson@2516
   159
qed "usedI";
paulson@2516
   160
paulson@2516
   161
AddIs [usedI];
paulson@2516
   162
paulson@2516
   163
(** Fresh keys never clash with long-term shared keys **)
paulson@2516
   164
paulson@2516
   165
goal thy "Key (shrK A) : used evs";
paulson@3121
   166
by (Blast_tac 1);
paulson@2516
   167
qed "shrK_in_used";
paulson@2516
   168
AddIffs [shrK_in_used];
paulson@2516
   169
paulson@3121
   170
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@2516
   171
  from long-term shared keys*)
paulson@2516
   172
goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
paulson@3121
   173
by (Blast_tac 1);
paulson@2516
   174
qed "Key_not_used";
paulson@2516
   175
paulson@2516
   176
(*A session key cannot clash with a long-term shared key*)
paulson@2516
   177
goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
paulson@2891
   178
by (Blast_tac 1);
paulson@2516
   179
qed "shrK_neq";
paulson@2516
   180
paulson@2516
   181
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
paulson@2516
   182
paulson@2516
   183
paulson@2516
   184
goal thy "used (Says A B X # evs) = parts{X} Un used evs";
paulson@2516
   185
by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
paulson@2516
   186
qed "used_Says";
paulson@2516
   187
Addsimps [used_Says];
paulson@2516
   188
paulson@2516
   189
goal thy "used [] <= used l";
paulson@2516
   190
by (list.induct_tac "l" 1);
paulson@2516
   191
by (event.induct_tac "a" 2);
paulson@2516
   192
by (ALLGOALS Asm_simp_tac);
paulson@3121
   193
by (Blast_tac 1);
paulson@2516
   194
qed "used_nil_subset";
paulson@2516
   195
paulson@2516
   196
goal thy "used l <= used (l@l')";
paulson@2516
   197
by (list.induct_tac "l" 1);
paulson@2516
   198
by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
paulson@2516
   199
by (event.induct_tac "a" 1);
paulson@2516
   200
by (Asm_simp_tac 1);
paulson@3121
   201
by (Blast_tac 1);
paulson@2516
   202
qed "used_subset_append";
paulson@2516
   203
paulson@2516
   204
paulson@2516
   205
(*** Supply fresh nonces for possibility theorems. ***)
paulson@2516
   206
paulson@2516
   207
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
paulson@2516
   208
by (list.induct_tac "evs" 1);
paulson@2516
   209
by (res_inst_tac [("x","0")] exI 1);
paulson@2516
   210
by (Step_tac 1);
paulson@2516
   211
by (Full_simp_tac 1);
paulson@2516
   212
(*Inductive step*)
paulson@2516
   213
by (event.induct_tac "a" 1);
paulson@2516
   214
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
paulson@2516
   215
by (msg.induct_tac "msg" 1);
paulson@2516
   216
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
paulson@2516
   217
by (Step_tac 1);
paulson@2516
   218
(*MPair case*)
paulson@2516
   219
by (res_inst_tac [("x","Na+Nb")] exI 2);
paulson@2891
   220
by (blast_tac (!claset addSEs [add_leE]) 2);
paulson@2516
   221
(*Nonce case*)
paulson@2516
   222
by (res_inst_tac [("x","N + Suc nat")] exI 1);
oheimb@2637
   223
by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
paulson@2516
   224
val lemma = result();
paulson@2516
   225
paulson@2516
   226
goal thy "EX N. Nonce N ~: used evs";
paulson@2516
   227
by (rtac (lemma RS exE) 1);
paulson@2891
   228
by (Blast_tac 1);
paulson@2516
   229
qed "Nonce_supply1";
paulson@2516
   230
paulson@2516
   231
goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
paulson@2516
   232
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   233
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   234
by (Step_tac 1);
paulson@2516
   235
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   236
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   237
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   238
				     le_add2, le_add1, 
paulson@2516
   239
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   240
qed "Nonce_supply2";
paulson@2516
   241
paulson@2516
   242
goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
paulson@2516
   243
\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
paulson@2516
   244
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   245
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   246
by (cut_inst_tac [("evs","evs''")] lemma 1);
paulson@2516
   247
by (Step_tac 1);
paulson@2516
   248
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   249
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   250
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
paulson@2516
   251
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   252
				     le_add2, le_add1, 
paulson@2516
   253
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   254
by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
paulson@2516
   255
by (stac (le_eq_less_Suc RS sym) 1);
paulson@2516
   256
by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
paulson@2516
   257
by (REPEAT (rtac le_add1 1));
paulson@2516
   258
qed "Nonce_supply3";
paulson@2516
   259
paulson@2516
   260
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
paulson@2516
   261
by (rtac (lemma RS exE) 1);
paulson@2516
   262
by (rtac selectI 1);
paulson@2891
   263
by (Blast_tac 1);
paulson@2516
   264
qed "Nonce_supply";
paulson@2516
   265
paulson@2516
   266
(*** Supply fresh keys for possibility theorems. ***)
paulson@2516
   267
paulson@2516
   268
goal thy "EX K. Key K ~: used evs";
nipkow@3414
   269
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
paulson@2891
   270
by (Blast_tac 1);
paulson@2516
   271
qed "Key_supply1";
paulson@2516
   272
paulson@2516
   273
goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
nipkow@3414
   274
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
paulson@2516
   275
by (etac exE 1);
paulson@2516
   276
by (cut_inst_tac [("evs","evs'")] 
nipkow@3414
   277
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
paulson@2516
   278
by (Auto_tac());
paulson@2516
   279
qed "Key_supply2";
paulson@2516
   280
paulson@2516
   281
goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
paulson@2516
   282
\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
nipkow@3414
   283
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
paulson@2516
   284
by (etac exE 1);
paulson@2516
   285
by (cut_inst_tac [("evs","evs'")] 
nipkow@3414
   286
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
paulson@2516
   287
by (etac exE 1);
paulson@2516
   288
by (cut_inst_tac [("evs","evs''")] 
nipkow@3414
   289
    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
paulson@2516
   290
by (Step_tac 1);
paulson@2516
   291
by (Full_simp_tac 1);
paulson@2516
   292
by (fast_tac (!claset addSEs [allE]) 1);
paulson@2516
   293
qed "Key_supply3";
paulson@2516
   294
paulson@2516
   295
goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
nipkow@3414
   296
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
paulson@2516
   297
by (rtac selectI 1);
paulson@2891
   298
by (Blast_tac 1);
paulson@2516
   299
qed "Key_supply";
paulson@2516
   300
paulson@2516
   301
(*** Tactics for possibility theorems ***)
paulson@2516
   302
paulson@2516
   303
val possibility_tac =
paulson@2516
   304
    REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
paulson@2516
   305
    (ALLGOALS (simp_tac 
oheimb@2637
   306
               (!simpset delsimps [used_Says] setSolver safe_solver))
paulson@2516
   307
     THEN
paulson@2516
   308
     REPEAT_FIRST (eq_assume_tac ORELSE' 
paulson@2516
   309
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
paulson@2516
   310
paulson@2516
   311
(*For harder protocols (such as Recur) where we have to set up some
paulson@2516
   312
  nonces and keys initially*)
paulson@2516
   313
val basic_possibility_tac =
paulson@2516
   314
    REPEAT 
oheimb@2637
   315
    (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
paulson@2516
   316
     THEN
paulson@2516
   317
     REPEAT_FIRST (resolve_tac [refl, conjI]));
paulson@2516
   318
paulson@2516
   319
paulson@2049
   320
(** Power of the Spy **)
paulson@1934
   321
paulson@2049
   322
(*The Spy can see more than anybody else, except for their initial state*)
paulson@2049
   323
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
paulson@2049
   324
by (list.induct_tac "evs" 1);
paulson@2049
   325
by (event.induct_tac "a" 2);
paulson@3121
   326
by (ALLGOALS Asm_simp_tac);
paulson@3121
   327
by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
paulson@2049
   328
qed "sees_agent_subset_sees_Spy";
paulson@2049
   329
paulson@2049
   330
(*The Spy can see more than anybody else who's lost their key!*)
paulson@2049
   331
goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
paulson@2049
   332
by (list.induct_tac "evs" 1);
paulson@2049
   333
by (event.induct_tac "a" 2);
paulson@2049
   334
by (agent.induct_tac "A" 1);
paulson@3121
   335
by (ALLGOALS Asm_simp_tac);
paulson@3121
   336
by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD])));
paulson@2049
   337
qed_spec_mp "sees_lost_agent_subset_sees_Spy";
paulson@2049
   338
paulson@1934
   339
paulson@2032
   340
(** Simplifying   parts (insert X (sees lost A evs))
paulson@2045
   341
      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
paulson@2012
   342
paulson@2012
   343
val parts_insert_sees = 
paulson@2045
   344
    parts_insert |> read_instantiate_sg (sign_of thy)
paulson@2045
   345
                                        [("H", "sees lost A evs")]
paulson@2012
   346
                 |> standard;
paulson@2045
   347
paulson@2045
   348
paulson@3472
   349
(*** Specialized rewriting for analz_insert_freshK ***)
paulson@2320
   350
paulson@2516
   351
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
paulson@2891
   352
by (Blast_tac 1);
paulson@2516
   353
qed "subset_Compl_range";
paulson@2045
   354
paulson@2516
   355
goal thy "insert (Key K) H = Key `` {K} Un H";
paulson@2891
   356
by (Blast_tac 1);
paulson@2516
   357
qed "insert_Key_singleton";
paulson@2516
   358
paulson@2516
   359
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
paulson@2891
   360
by (Blast_tac 1);
paulson@2891
   361
qed "insert_Key_image";
paulson@2516
   362
paulson@3451
   363
(*Reverse the normal simplification of "image" to build up (not break down)
paulson@3451
   364
  the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
paulson@3451
   365
  erase occurrences of forwarded message components (X).*)
paulson@2516
   366
val analz_image_freshK_ss = 
paulson@2516
   367
     !simpset delsimps [image_insert, image_Un]
paulson@3479
   368
              addsimps ([image_insert RS sym, image_Un RS sym,
paulson@3479
   369
                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
paulson@2516
   370
                         insert_Key_singleton, subset_Compl_range,
paulson@3479
   371
                         Key_not_used, insert_Key_image, Un_assoc RS sym]
paulson@2516
   372
                        @disj_comms)
paulson@2516
   373
              setloop split_tac [expand_if];
paulson@2045
   374
paulson@2045
   375
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@2045
   376
goal thy  
paulson@2045
   377
 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
paulson@2045
   378
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
paulson@2922
   379
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
paulson@2516
   380
qed "analz_image_freshK_lemma";