src/HOL/Auth/Event.ML
author paulson
Wed Aug 21 13:22:23 1996 +0200 (1996-08-21)
changeset 1933 8b24773de6db
parent 1930 cdf9bcd53749
child 1942 6c9c1a42a869
permissions -rw-r--r--
Addition of message NS5
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
Datatype of events;
paulson@1839
     7
inductive relation "traces" for Needham-Schroeder (shared keys)
paulson@1852
     8
paulson@1852
     9
Rewrites should not refer to	 initState (Friend i)    -- not in normal form
paulson@1839
    10
*)
paulson@1839
    11
paulson@1929
    12
Addsimps [parts_cut_eq];
paulson@1929
    13
paulson@1929
    14
paulson@1929
    15
(*INSTALLED ON NAT.ML*)
paulson@1929
    16
goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)";
paulson@1929
    17
by (rtac not_less_eq 1);
paulson@1929
    18
qed "le_eq_less_Suc";
paulson@1839
    19
paulson@1885
    20
proof_timing:=true;
paulson@1885
    21
paulson@1885
    22
(*FOR LIST.ML??*)
paulson@1913
    23
goal List.thy "x : set_of_list (x#xs)";
paulson@1885
    24
by (Simp_tac 1);
paulson@1913
    25
qed "set_of_list_I1";
paulson@1885
    26
paulson@1913
    27
goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs";
paulson@1885
    28
by (Asm_simp_tac 1);
paulson@1913
    29
qed "set_of_list_eqI1";
paulson@1885
    30
paulson@1913
    31
goal List.thy "set_of_list l <= set_of_list (x#l)";
paulson@1893
    32
by (Simp_tac 1);
paulson@1893
    33
by (Fast_tac 1);
paulson@1913
    34
qed "set_of_list_subset_Cons";
paulson@1893
    35
paulson@1885
    36
(*Not for Addsimps -- it can cause goals to blow up!*)
paulson@1885
    37
goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
paulson@1885
    38
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@1885
    39
qed "mem_if";
paulson@1885
    40
paulson@1913
    41
(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
paulson@1885
    42
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
paulson@1885
    43
by (fast_tac (!claset addEs [equalityE]) 1);
paulson@1885
    44
val subset_range_iff = result();
paulson@1885
    45
paulson@1885
    46
paulson@1839
    47
open Event;
paulson@1839
    48
paulson@1885
    49
Addsimps [Un_insert_left, Un_insert_right];
paulson@1885
    50
paulson@1885
    51
(*By default only o_apply is built-in.  But in the presence of eta-expansion
paulson@1885
    52
  this means that some terms displayed as (f o g) will be rewritten, and others
paulson@1885
    53
  will not!*)
paulson@1885
    54
Addsimps [o_def];
paulson@1852
    55
paulson@1852
    56
(*** Basic properties of serverKey and newK ***)
paulson@1852
    57
paulson@1839
    58
(* invKey (serverKey A) = serverKey A *)
paulson@1839
    59
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
paulson@1839
    60
paulson@1852
    61
(* invKey (newK evs) = newK evs *)
paulson@1839
    62
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
paulson@1839
    63
Addsimps [invKey_serverKey, invKey_newK];
paulson@1839
    64
paulson@1839
    65
paulson@1839
    66
(*New keys and nonces are fresh*)
paulson@1839
    67
val serverKey_inject = inj_serverKey RS injD;
paulson@1852
    68
val newN_inject = inj_newN RS injD
paulson@1852
    69
and newK_inject = inj_newK RS injD;
paulson@1839
    70
AddSEs [serverKey_inject, newN_inject, newK_inject,
paulson@1839
    71
	fresh_newK RS notE, fresh_newN RS notE];
paulson@1839
    72
Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
paulson@1839
    73
Addsimps [fresh_newN, fresh_newK];
paulson@1839
    74
paulson@1852
    75
goal thy "newK evs ~= serverKey B";
paulson@1852
    76
by (subgoal_tac "newK evs = serverKey B --> \
paulson@1852
    77
\                Key (newK evs) : parts (initState B)" 1);
paulson@1839
    78
by (Fast_tac 1);
paulson@1839
    79
by (agent.induct_tac "B" 1);
paulson@1839
    80
by (auto_tac (!claset addIs [range_eqI], !simpset));
paulson@1839
    81
qed "newK_neq_serverKey";
paulson@1839
    82
paulson@1839
    83
Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
paulson@1839
    84
paulson@1839
    85
(*Good for talking about Server's initial state*)
paulson@1885
    86
goal thy "!!H. H <= Key``E ==> parts H = H";
paulson@1885
    87
by (Auto_tac ());
paulson@1839
    88
be parts.induct 1;
paulson@1839
    89
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
paulson@1885
    90
qed "parts_image_subset";
paulson@1839
    91
paulson@1885
    92
bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
paulson@1885
    93
paulson@1913
    94
goal thy "!!H. H <= Key``E ==> analz H = H";
paulson@1885
    95
by (Auto_tac ());
paulson@1913
    96
be analz.induct 1;
paulson@1839
    97
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
paulson@1913
    98
qed "analz_image_subset";
paulson@1839
    99
paulson@1913
   100
bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
paulson@1885
   101
paulson@1913
   102
Addsimps [parts_image_Key, analz_image_Key];
paulson@1839
   103
paulson@1839
   104
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
paulson@1839
   105
by (agent.induct_tac "C" 1);
paulson@1929
   106
by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset));
paulson@1839
   107
qed "keysFor_parts_initState";
paulson@1839
   108
Addsimps [keysFor_parts_initState];
paulson@1839
   109
paulson@1885
   110
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
paulson@1885
   111
by (Auto_tac ());
paulson@1885
   112
qed "keysFor_image_Key";
paulson@1885
   113
Addsimps [keysFor_image_Key];
paulson@1885
   114
paulson@1885
   115
goal thy "serverKey A ~: newK``E";
paulson@1885
   116
by (agent.induct_tac "A" 1);
paulson@1885
   117
by (Auto_tac ());
paulson@1885
   118
qed "serverKey_notin_image_newK";
paulson@1885
   119
Addsimps [serverKey_notin_image_newK];
paulson@1885
   120
paulson@1885
   121
paulson@1885
   122
(*Agents see their own serverKeys!*)
paulson@1913
   123
goal thy "Key (serverKey A) : analz (sees A evs)";
paulson@1885
   124
by (list.induct_tac "evs" 1);
paulson@1913
   125
by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
paulson@1885
   126
by (agent.induct_tac "A" 1);
paulson@1885
   127
by (auto_tac (!claset addIs [range_eqI], !simpset));
paulson@1913
   128
qed "analz_own_serverKey";
paulson@1885
   129
paulson@1885
   130
bind_thm ("parts_own_serverKey",
paulson@1913
   131
	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
paulson@1885
   132
paulson@1913
   133
Addsimps [analz_own_serverKey, parts_own_serverKey];
paulson@1885
   134
paulson@1885
   135
paulson@1839
   136
paulson@1839
   137
(**** Inductive relation "traces" -- basic properties ****)
paulson@1839
   138
paulson@1839
   139
val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps);
paulson@1839
   140
paulson@1839
   141
val Says_tracesE        = mk_cases "Says A B X # evs: traces";
paulson@1839
   142
val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
paulson@1839
   143
val Says_Enemy_tracesE  = mk_cases "Says Enemy B X # evs: traces";
paulson@1839
   144
val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
paulson@1839
   145
val Notes_tracesE       = mk_cases "Notes A X # evs: traces";
paulson@1839
   146
paulson@1839
   147
(*The tail of a trace is a trace*)
paulson@1839
   148
goal thy "!!ev evs. ev#evs : traces ==> evs : traces";
paulson@1839
   149
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
paulson@1839
   150
qed "traces_ConsE";
paulson@1839
   151
paulson@1885
   152
goal thy "!!ev evs. [| evs = ev#evs'; evs : traces |] ==> evs' : traces";
paulson@1885
   153
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
paulson@1885
   154
qed "traces_eq_ConsE";
paulson@1885
   155
paulson@1885
   156
paulson@1839
   157
(** Specialized rewrite rules for (sees A (Says...#evs)) **)
paulson@1839
   158
paulson@1839
   159
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
paulson@1839
   160
by (Simp_tac 1);
paulson@1839
   161
qed "sees_own";
paulson@1839
   162
paulson@1839
   163
goal thy "!!A. Server ~= A ==> \
paulson@1839
   164
\              sees Server (Says A B X # evs) = sees Server evs";
paulson@1839
   165
by (Asm_simp_tac 1);
paulson@1839
   166
qed "sees_Server";
paulson@1839
   167
paulson@1839
   168
goal thy "!!A. Friend i ~= A ==> \
paulson@1839
   169
\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
paulson@1839
   170
by (Asm_simp_tac 1);
paulson@1839
   171
qed "sees_Friend";
paulson@1839
   172
paulson@1839
   173
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
paulson@1839
   174
by (Simp_tac 1);
paulson@1839
   175
qed "sees_Enemy";
paulson@1839
   176
paulson@1839
   177
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
paulson@1839
   178
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@1839
   179
by (Fast_tac 1);
paulson@1852
   180
qed "sees_Says_subset_insert";
paulson@1852
   181
paulson@1852
   182
goal thy "sees A evs <= sees A (Says A' B X # evs)";
paulson@1852
   183
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@1852
   184
by (Fast_tac 1);
paulson@1852
   185
qed "sees_subset_sees_Says";
paulson@1839
   186
paulson@1839
   187
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
paulson@1839
   188
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
paulson@1839
   189
\         parts {Y} Un (UN A. parts (sees A evs))";
paulson@1839
   190
by (Step_tac 1);
paulson@1839
   191
be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
paulson@1839
   192
val ss = (!simpset addsimps [parts_Un, sees_Cons] 
paulson@1839
   193
	           setloop split_tac [expand_if]);
paulson@1839
   194
by (ALLGOALS (fast_tac (!claset addss ss)));
paulson@1839
   195
qed "UN_parts_sees_Says";
paulson@1839
   196
paulson@1913
   197
goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
paulson@1885
   198
by (list.induct_tac "evs" 1);
paulson@1885
   199
by (Auto_tac ());
paulson@1885
   200
qed_spec_mp "Says_imp_sees_Enemy";
paulson@1885
   201
paulson@1885
   202
Addsimps [Says_imp_sees_Enemy];
paulson@1885
   203
AddIs    [Says_imp_sees_Enemy];
paulson@1839
   204
paulson@1893
   205
goal thy "initState C <= Key `` range serverKey";
paulson@1893
   206
by (agent.induct_tac "C" 1);
paulson@1893
   207
by (Auto_tac ());
paulson@1893
   208
qed "initState_subset";
paulson@1893
   209
paulson@1893
   210
goal thy "X : sees C evs --> \
paulson@1913
   211
\          (EX A B. Says A B X : set_of_list evs) | \
paulson@1913
   212
\          (EX A. Notes A X : set_of_list evs) | \
paulson@1893
   213
\          (EX A. X = Key (serverKey A))";
paulson@1893
   214
by (list.induct_tac "evs" 1);
paulson@1893
   215
by (ALLGOALS Asm_simp_tac);
paulson@1893
   216
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
paulson@1893
   217
br conjI 1;
paulson@1893
   218
by (Fast_tac 2);
paulson@1893
   219
by (event.induct_tac "a" 1);
paulson@1893
   220
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
paulson@1893
   221
by (ALLGOALS Fast_tac);
paulson@1893
   222
qed_spec_mp "seesD";
paulson@1893
   223
paulson@1893
   224
paulson@1839
   225
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
paulson@1852
   226
Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
paulson@1839
   227
paulson@1839
   228
paulson@1839
   229
(**** Inductive proofs about traces ****)
paulson@1839
   230
paulson@1839
   231
(*The Enemy can see more than anybody else, except for their initial state*)
paulson@1839
   232
goal thy 
paulson@1839
   233
 "!!evs. evs : traces ==> \
paulson@1839
   234
\     sees A evs <= initState A Un sees Enemy evs";
paulson@1839
   235
be traces.induct 1;
paulson@1852
   236
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
paulson@1839
   237
			        addss (!simpset))));
paulson@1839
   238
qed "sees_agent_subset_sees_Enemy";
paulson@1839
   239
paulson@1839
   240
paulson@1885
   241
(*Nobody sends themselves messages*)
paulson@1913
   242
goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs";
paulson@1852
   243
be traces.induct 1;
paulson@1852
   244
by (Auto_tac());
paulson@1852
   245
qed_spec_mp "not_Says_to_self";
paulson@1852
   246
Addsimps [not_Says_to_self];
paulson@1852
   247
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@1852
   248
paulson@1913
   249
goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs";
paulson@1893
   250
be traces.induct 1;
paulson@1893
   251
by (Auto_tac());
paulson@1893
   252
qed "not_Notes";
paulson@1893
   253
Addsimps [not_Notes];
paulson@1893
   254
AddSEs   [not_Notes RSN (2, rev_notE)];
paulson@1893
   255
paulson@1852
   256
paulson@1929
   257
goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
paulson@1929
   258
\                X : parts (sees Enemy evs)";
paulson@1929
   259
by (fast_tac (!claset addSEs partsEs
paulson@1929
   260
	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
paulson@1929
   261
qed "NS3_msg_in_parts_sees_Enemy";
paulson@1929
   262
			      
paulson@1929
   263
paulson@1839
   264
(*** Server keys are not betrayed ***)
paulson@1839
   265
paulson@1852
   266
(*Enemy never sees another agent's server key!*)
paulson@1839
   267
goal thy 
paulson@1852
   268
 "!!evs. [| evs : traces; A ~= Enemy |] ==> \
paulson@1852
   269
\        Key (serverKey A) ~: parts (sees Enemy evs)";
paulson@1839
   270
be traces.induct 1;
paulson@1929
   271
bd NS3_msg_in_parts_sees_Enemy 5;
paulson@1929
   272
by (Auto_tac());
paulson@1929
   273
(*Deals with Fake message*)
paulson@1913
   274
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@1929
   275
			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
paulson@1839
   276
qed "Enemy_not_see_serverKey";
paulson@1839
   277
paulson@1913
   278
bind_thm ("Enemy_not_analz_serverKey",
paulson@1913
   279
	  [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
paulson@1852
   280
paulson@1885
   281
Addsimps [Enemy_not_see_serverKey, 
paulson@1885
   282
	  not_sym RSN (2, Enemy_not_see_serverKey), 
paulson@1913
   283
	  Enemy_not_analz_serverKey, 
paulson@1913
   284
	  not_sym RSN (2, Enemy_not_analz_serverKey)];
paulson@1852
   285
paulson@1893
   286
(*We go to some trouble to preserve R in the 3rd subgoal*)
paulson@1893
   287
val major::prems = 
paulson@1893
   288
goal thy  "[| Key (serverKey A) : parts (sees Enemy evs);    \
paulson@1893
   289
\             evs : traces;                                  \
paulson@1893
   290
\             A=Enemy ==> R                                  \
paulson@1893
   291
\           |] ==> R";
paulson@1893
   292
br ccontr 1;
paulson@1893
   293
br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1;
paulson@1893
   294
by (swap_res_tac prems 2);
paulson@1893
   295
by (ALLGOALS (fast_tac (!claset addIs prems)));
paulson@1893
   296
qed "Enemy_see_serverKey_E";
paulson@1893
   297
paulson@1913
   298
bind_thm ("Enemy_analz_serverKey_E", 
paulson@1913
   299
	  analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
paulson@1893
   300
paulson@1893
   301
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
paulson@1913
   302
AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
paulson@1893
   303
paulson@1839
   304
paulson@1852
   305
(*No Friend will ever see another agent's server key 
paulson@1885
   306
  (excluding the Enemy, who might transmit his).
paulson@1885
   307
  The Server, of course, knows all server keys.*)
paulson@1839
   308
goal thy 
paulson@1852
   309
 "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
paulson@1852
   310
\        Key (serverKey A) ~: parts (sees (Friend j) evs)";
paulson@1852
   311
br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
paulson@1852
   312
by (ALLGOALS Asm_simp_tac);
paulson@1852
   313
qed "Friend_not_see_serverKey";
paulson@1839
   314
paulson@1839
   315
paulson@1885
   316
(*Not for Addsimps -- it can cause goals to blow up!*)
paulson@1885
   317
goal thy  
paulson@1885
   318
 "!!evs. evs : traces ==>                                  \
paulson@1885
   319
\        (Key (serverKey A) \
paulson@1913
   320
\           : analz (insert (Key (serverKey B)) (sees Enemy evs))) =  \
paulson@1885
   321
\        (A=B | A=Enemy)";
paulson@1913
   322
by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
paulson@1913
   323
		      addIs [impOfSubs (subset_insertI RS analz_mono)]
paulson@1885
   324
	              addss (!simpset)) 1);
paulson@1913
   325
qed "serverKey_mem_analz";
paulson@1885
   326
paulson@1885
   327
paulson@1885
   328
paulson@1885
   329
paulson@1839
   330
(*** Future keys can't be seen or used! ***)
paulson@1839
   331
paulson@1839
   332
(*Nobody can have SEEN keys that will be generated in the future.
paulson@1839
   333
  This has to be proved anew for each protocol description,
paulson@1839
   334
  but should go by similar reasoning every time.  Hardest case is the
paulson@1839
   335
  standard Fake rule.  
paulson@1839
   336
      The length comparison, and Union over C, are essential for the 
paulson@1839
   337
  induction! *)
paulson@1839
   338
goal thy "!!evs. evs : traces ==> \
paulson@1839
   339
\                length evs <= length evs' --> \
paulson@1852
   340
\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
paulson@1839
   341
be traces.induct 1;
paulson@1929
   342
bd NS3_msg_in_parts_sees_Enemy 5;
paulson@1929
   343
(*auto_tac does not work here, as it performs safe_tac first*)
paulson@1929
   344
by (ALLGOALS Asm_simp_tac);
paulson@1929
   345
by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@1929
   346
				       impOfSubs parts_insert_subset_Un,
paulson@1929
   347
				       Suc_leD]
paulson@1929
   348
			        addss (!simpset))));
paulson@1839
   349
val lemma = result();
paulson@1839
   350
paulson@1839
   351
(*Variant needed for the main theorem below*)
paulson@1839
   352
goal thy 
paulson@1839
   353
 "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
paulson@1852
   354
\        Key (newK evs') ~: parts (sees C evs)";
paulson@1839
   355
by (fast_tac (!claset addDs [lemma]) 1);
paulson@1839
   356
qed "new_keys_not_seen";
paulson@1893
   357
Addsimps [new_keys_not_seen];
paulson@1839
   358
paulson@1893
   359
(*Another variant: old messages must contain old keys!*)
paulson@1893
   360
goal thy 
paulson@1913
   361
 "!!evs. [| Says A B X : set_of_list evs;  \
paulson@1893
   362
\           Key (newK evt) : parts {X};    \
paulson@1893
   363
\           evs : traces                 \
paulson@1893
   364
\        |] ==> length evt < length evs";
paulson@1893
   365
br ccontr 1;
paulson@1893
   366
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
paulson@1893
   367
	              addIs [impOfSubs parts_mono, leI]) 1);
paulson@1893
   368
qed "Says_imp_old_keys";
paulson@1893
   369
paulson@1885
   370
paulson@1852
   371
goal thy "!!K. newK evs = invKey K ==> newK evs = K";
paulson@1839
   372
br (invKey_eq RS iffD1) 1;
paulson@1839
   373
by (Simp_tac 1);
paulson@1839
   374
val newK_invKey = result();
paulson@1839
   375
paulson@1852
   376
paulson@1852
   377
val keysFor_parts_mono = parts_mono RS keysFor_mono;
paulson@1852
   378
paulson@1839
   379
(*Nobody can have USED keys that will be generated in the future.
paulson@1839
   380
  ...very like new_keys_not_seen*)
paulson@1839
   381
goal thy "!!evs. evs : traces ==> \
paulson@1839
   382
\                length evs <= length evs' --> \
paulson@1852
   383
\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
paulson@1839
   384
be traces.induct 1;
paulson@1929
   385
bd NS3_msg_in_parts_sees_Enemy 5;
paulson@1929
   386
by (ALLGOALS Asm_simp_tac);
paulson@1930
   387
(*NS1 and NS2*)
paulson@1930
   388
map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
paulson@1930
   389
(*Fake and NS3*)
paulson@1930
   390
map (by o best_tac
paulson@1929
   391
     (!claset addSDs [newK_invKey]
paulson@1929
   392
	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
paulson@1929
   393
		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
paulson@1929
   394
		     Suc_leD]
paulson@1929
   395
	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
paulson@1930
   396
	      addss (!simpset)))
paulson@1930
   397
    [2,1];
paulson@1933
   398
(*NS4 and NS5: nonce exchange*)
paulson@1933
   399
by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
paulson@1933
   400
	                          addIs  [less_SucI, impOfSubs keysFor_mono]
paulson@1933
   401
		                  addss (!simpset addsimps [le_def])) 0));
paulson@1839
   402
val lemma = result();
paulson@1839
   403
paulson@1839
   404
goal thy 
paulson@1839
   405
 "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
paulson@1852
   406
\        newK evs' ~: keysFor (parts (sees C evs))";
paulson@1839
   407
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
paulson@1839
   408
qed "new_keys_not_used";
paulson@1839
   409
paulson@1913
   410
bind_thm ("new_keys_not_analzd",
paulson@1913
   411
	  [analz_subset_parts RS keysFor_mono,
paulson@1839
   412
	   new_keys_not_used] MRS contra_subsetD);
paulson@1839
   413
paulson@1913
   414
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@1852
   415
paulson@1852
   416
paulson@1885
   417
(** Rewrites to push in Key and Crypt messages, so that other messages can
paulson@1913
   418
    be pulled out using the analz_insert rules **)
paulson@1885
   419
paulson@1885
   420
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
paulson@1885
   421
                      insert_commute;
paulson@1839
   422
paulson@1885
   423
val pushKeys = map (insComm "Key ?K") 
paulson@1885
   424
                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
paulson@1885
   425
paulson@1885
   426
val pushCrypts = map (insComm "Crypt ?X ?K") 
paulson@1885
   427
                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
paulson@1885
   428
paulson@1885
   429
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
paulson@1885
   430
val pushes = pushKeys@pushCrypts;
paulson@1885
   431
paulson@1885
   432
val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
paulson@1839
   433
paulson@1852
   434
paulson@1839
   435
(** Lemmas concerning the form of items passed in messages **)
paulson@1839
   436
paulson@1885
   437
(*Describes the form *and age* of K, and the form of X,
paulson@1885
   438
  when the following message is sent*)
paulson@1839
   439
goal thy 
paulson@1913
   440
 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
paulson@1885
   441
\           evs : traces    \
paulson@1893
   442
\        |] ==> (EX evt:traces. \
paulson@1893
   443
\                         K = Key(newK evt) & \
paulson@1893
   444
\                         X = (Crypt {|K, Agent A|} (serverKey B)) & \
paulson@1893
   445
\                         K' = serverKey A & \
paulson@1893
   446
\                         length evt < length evs)";
paulson@1839
   447
be rev_mp 1;
paulson@1839
   448
be traces.induct 1;
paulson@1839
   449
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
paulson@1885
   450
qed "Says_Server_message_form";
paulson@1839
   451
paulson@1913
   452
(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *)
paulson@1913
   453
bind_thm ("not_parts_not_keysFor_analz", 
paulson@1913
   454
	  analz_subset_parts RS keysFor_mono RS contra_subsetD);
paulson@1852
   455
paulson@1852
   456
paulson@1885
   457
paulson@1885
   458
(*USELESS for NS3, case 1, as the ind hyp says the same thing!
paulson@1885
   459
goal thy 
paulson@1885
   460
 "!!evs. [| evs = Says Server (Friend i) \
paulson@1885
   461
\                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
paulson@1885
   462
\           evs : traces;  i~=k                                    \
paulson@1885
   463
\        |] ==>                                                    \
paulson@1913
   464
\     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
paulson@1885
   465
be rev_mp 1;
paulson@1885
   466
be traces.induct 1;
paulson@1885
   467
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
paulson@1885
   468
by (Step_tac 1);
paulson@1913
   469
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
paulson@1885
   470
val Enemy_not_see_encrypted_key_lemma = result();
paulson@1885
   471
*)
paulson@1885
   472
paulson@1885
   473
paulson@1885
   474
(*Describes the form of X when the following message is sent*)
paulson@1885
   475
goal thy
paulson@1885
   476
 "!!evs. evs : traces ==>                             \
paulson@1885
   477
\        ALL A NA B K X.                            \
paulson@1885
   478
\            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
paulson@1885
   479
\            : parts (sees Enemy evs) & A ~= Enemy  -->   \
paulson@1885
   480
\          (EX evt:traces. K = newK evt & \
paulson@1885
   481
\                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
paulson@1885
   482
be traces.induct 1;
paulson@1929
   483
bd NS3_msg_in_parts_sees_Enemy 5;
paulson@1885
   484
by (Step_tac 1);
paulson@1885
   485
by (ALLGOALS Asm_full_simp_tac);
paulson@1929
   486
(*Remaining cases are Fake and NS2*)
paulson@1885
   487
by (fast_tac (!claset addSDs [spec]) 2);
paulson@1885
   488
(*Now for the Fake case*)
paulson@1929
   489
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@1929
   490
			     impOfSubs synth_analz_parts_insert_subset_Un]
paulson@1885
   491
	              addss (!simpset)) 1);
paulson@1929
   492
qed_spec_mp "encrypted_form";
paulson@1885
   493
paulson@1885
   494
paulson@1885
   495
(*For eliminating the A ~= Enemy condition from the previous result*)
paulson@1885
   496
goal thy 
paulson@1885
   497
 "!!evs. evs : traces ==>                             \
paulson@1885
   498
\        ALL S A NA B K X.                            \
paulson@1885
   499
\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
paulson@1913
   500
\            : set_of_list evs  -->   \
paulson@1885
   501
\        S = Server | S = Enemy";
paulson@1885
   502
be traces.induct 1;
paulson@1893
   503
by (ALLGOALS Asm_simp_tac);
paulson@1885
   504
(*We are left with NS3*)
paulson@1885
   505
by (subgoal_tac "S = Server | S = Enemy" 1);
paulson@1885
   506
(*First justify this assumption!*)
paulson@1885
   507
by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
paulson@1885
   508
by (Step_tac 1);
paulson@1929
   509
bd Says_Server_message_form 1;
paulson@1885
   510
by (ALLGOALS Full_simp_tac);
paulson@1885
   511
(*Final case.  Clear out needless quantifiers to speed the following step*)
paulson@1885
   512
by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
paulson@1929
   513
bd encrypted_form 1;
paulson@1885
   514
br (parts.Inj RS conjI) 1;
paulson@1885
   515
auto();
paulson@1885
   516
qed_spec_mp "Server_or_Enemy";
paulson@1885
   517
paulson@1885
   518
paulson@1885
   519
(*Describes the form of X when the following message is sent;
paulson@1885
   520
  use Says_Server_message_form if applicable*)
paulson@1885
   521
goal thy 
paulson@1885
   522
 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
paulson@1913
   523
\            : set_of_list evs;                              \
paulson@1885
   524
\           evs : traces               \
paulson@1893
   525
\        |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
paulson@1885
   526
\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
paulson@1885
   527
by (forward_tac [Server_or_Enemy] 1);
paulson@1885
   528
ba 1;
paulson@1885
   529
by (Step_tac 1);
paulson@1885
   530
by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
paulson@1929
   531
by (forward_tac [encrypted_form] 1);
paulson@1885
   532
br (parts.Inj RS conjI) 1;
paulson@1893
   533
by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
paulson@1885
   534
qed "Says_S_message_form";
paulson@1885
   535
paulson@1930
   536
(*Currently unused.  Needed only to reason about the VERY LAST message.*)
paulson@1885
   537
goal thy 
paulson@1885
   538
 "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}   \
paulson@1885
   539
\                           (serverKey A)) # evs';                  \
paulson@1885
   540
\           evs : traces                                           \
paulson@1893
   541
\        |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \
paulson@1885
   542
\                               K = newK evt & \
paulson@1885
   543
\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
paulson@1885
   544
by (forward_tac [traces_eq_ConsE] 1);
paulson@1913
   545
by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
paulson@1885
   546
by (Auto_tac());	
paulson@1885
   547
qed "Says_S_message_form_eq";
paulson@1885
   548
paulson@1885
   549
paulson@1885
   550
paulson@1885
   551
(****
paulson@1885
   552
 The following is to prove theorems of the form
paulson@1885
   553
paulson@1913
   554
          Key K : analz (insert (Key (newK evt)) 
paulson@1885
   555
	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
paulson@1913
   556
          Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
paulson@1885
   557
paulson@1885
   558
 A more general formula must be proved inductively.
paulson@1885
   559
paulson@1885
   560
****)
paulson@1885
   561
paulson@1885
   562
paulson@1933
   563
(*NOT useful in this form, but it says that session keys are not used
paulson@1885
   564
  to encrypt messages containing other keys, in the actual protocol.
paulson@1885
   565
  We require that agents should behave like this subsequently also.*)
paulson@1885
   566
goal thy 
paulson@1885
   567
 "!!evs. evs : traces ==> \
paulson@1885
   568
\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
paulson@1885
   569
\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
paulson@1885
   570
be traces.induct 1;
paulson@1929
   571
bd NS3_msg_in_parts_sees_Enemy 5;
paulson@1893
   572
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
paulson@1885
   573
(*Deals with Faked messages*)
paulson@1929
   574
by (best_tac (!claset addSEs partsEs
paulson@1929
   575
		      addDs [impOfSubs analz_subset_parts,
paulson@1929
   576
                             impOfSubs parts_insert_subset_Un]
paulson@1929
   577
                      addss (!simpset)) 1);
paulson@1933
   578
(*NS4 and NS5*)
paulson@1933
   579
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
paulson@1885
   580
result();
paulson@1885
   581
paulson@1885
   582
paulson@1893
   583
(** Specialized rewriting for this proof **)
paulson@1885
   584
paulson@1885
   585
Delsimps [image_insert];
paulson@1885
   586
Addsimps [image_insert RS sym];
paulson@1885
   587
paulson@1885
   588
goal thy "insert (Key (newK x)) (sees A evs) = \
paulson@1885
   589
\         Key `` (newK``{x}) Un (sees A evs)";
paulson@1885
   590
by (Fast_tac 1);
paulson@1885
   591
val insert_Key_singleton = result();
paulson@1885
   592
paulson@1885
   593
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
paulson@1885
   594
\         Key `` (f `` (insert x E)) Un C";
paulson@1885
   595
by (Fast_tac 1);
paulson@1885
   596
val insert_Key_image = result();
paulson@1885
   597
paulson@1885
   598
paulson@1893
   599
(** Session keys are not used to encrypt other session keys **)
paulson@1893
   600
paulson@1885
   601
goal thy  
paulson@1885
   602
 "!!evs. evs : traces ==> \
paulson@1913
   603
\  ALL K E. (Key K : analz (insert (Key (serverKey C)) \
paulson@1885
   604
\                             (Key``(newK``E) Un (sees Enemy evs)))) = \
paulson@1885
   605
\           (K : newK``E |  \
paulson@1913
   606
\            Key K : analz (insert (Key (serverKey C)) \
paulson@1885
   607
\                             (sees Enemy evs)))";
paulson@1885
   608
be traces.induct 1;
paulson@1929
   609
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
paulson@1885
   610
by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
paulson@1885
   611
by (ALLGOALS 
paulson@1893
   612
    (asm_simp_tac 
paulson@1885
   613
     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
paulson@1885
   614
			 @ pushes)
paulson@1885
   615
               setloop split_tac [expand_if])));
paulson@1885
   616
(*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
paulson@1885
   617
by (REPEAT (Fast_tac 3));
paulson@1885
   618
(*Base case*)
paulson@1885
   619
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
paulson@1885
   620
(** LEVEL 7 **)
paulson@1885
   621
(*Fake case*)
paulson@1885
   622
by (REPEAT (Safe_step_tac 1));
paulson@1929
   623
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2);
paulson@1885
   624
by (subgoal_tac 
paulson@1913
   625
    "Key K : analz \
paulson@1913
   626
\             (synth \
paulson@1913
   627
\              (analz (insert (Key (serverKey C)) \
paulson@1885
   628
\                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
paulson@1885
   629
(*First, justify this subgoal*)
paulson@1929
   630
(*Discard formulae for better speed*)
paulson@1885
   631
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
paulson@1885
   632
by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
paulson@1913
   633
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
paulson@1913
   634
                      addSEs [impOfSubs analz_mono]) 2);
paulson@1885
   635
by (Asm_full_simp_tac 1);
paulson@1913
   636
by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
paulson@1913
   637
qed_spec_mp "analz_image_newK";
paulson@1885
   638
paulson@1885
   639
paulson@1885
   640
goal thy  
paulson@1885
   641
 "!!evs. evs : traces ==>                                  \
paulson@1929
   642
\        Key K : analz (insert (Key (newK evt))            \
paulson@1885
   643
\                         (insert (Key (serverKey C))      \
paulson@1885
   644
\                          (sees Enemy evs))) =            \
paulson@1885
   645
\             (K = newK evt |                              \
paulson@1929
   646
\              Key K : analz (insert (Key (serverKey C))   \
paulson@1885
   647
\                               (sees Enemy evs)))";
paulson@1913
   648
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
paulson@1885
   649
				   insert_Key_singleton]) 1);
paulson@1885
   650
by (Fast_tac 1);
paulson@1913
   651
qed "analz_insert_Key_newK";
paulson@1885
   652
paulson@1885
   653
paulson@1885
   654
paulson@1929
   655
(*This says that the Key, K, uniquely identifies the message.
paulson@1929
   656
    But if C=Enemy then he could send all sorts of nonsense.*)
paulson@1893
   657
goal thy 
paulson@1893
   658
 "!!evs. evs : traces ==>                      \
paulson@1893
   659
\      EX X'. ALL C S A Y N B X.               \
paulson@1893
   660
\         C ~= Enemy -->                       \
paulson@1929
   661
\         Says S A Y : set_of_list evs -->     \
paulson@1893
   662
\         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
paulson@1893
   663
\       (X = X'))";
paulson@1893
   664
be traces.induct 1;
paulson@1929
   665
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
paulson@1893
   666
by (ALLGOALS 
paulson@1893
   667
    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
paulson@1893
   668
(*NS2: Case split propagates some context to other subgoal...*)
paulson@1893
   669
by (excluded_middle_tac "K = newK evsa" 2);
paulson@1893
   670
by (Asm_simp_tac 2);
paulson@1893
   671
(*...we assume X is a very new message, and handle this case by contradiction*)
paulson@1893
   672
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
paulson@1929
   673
		      addSEs partsEs
paulson@1893
   674
		      addEs [Says_imp_old_keys RS less_irrefl]
paulson@1893
   675
	              addss (!simpset)) 2);
paulson@1893
   676
(*NS3: No relevant messages*)
paulson@1893
   677
by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2);
paulson@1893
   678
(*Fake*)
paulson@1893
   679
by (Step_tac 1);
paulson@1893
   680
br exI 1;
paulson@1893
   681
br conjI 1;
paulson@1893
   682
ba 2;
paulson@1893
   683
by (Step_tac 1);
paulson@1929
   684
(** LEVEL 12 **)
paulson@1893
   685
by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
paulson@1893
   686
\                  : parts (sees Enemy evsa)" 1);
paulson@1893
   687
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
paulson@1913
   688
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
paulson@1893
   689
	              addDs [impOfSubs parts_insert_subset_Un]
paulson@1893
   690
                      addss (!simpset)) 2);
paulson@1893
   691
by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
paulson@1893
   692
bd parts_singleton 1;
paulson@1893
   693
by (Step_tac 1);
paulson@1893
   694
bd seesD 1;
paulson@1893
   695
by (Step_tac 1);
paulson@1893
   696
by (Full_simp_tac 2);
paulson@1893
   697
by (fast_tac (!claset addSDs [spec]) 1);
paulson@1893
   698
val lemma = result();
paulson@1885
   699
paulson@1885
   700
paulson@1893
   701
(*In messages of this form, the session key uniquely identifies the rest*)
paulson@1885
   702
goal thy 
paulson@1885
   703
 "!!evs. [| Says S A          \
paulson@1929
   704
\             (Crypt {|N, Agent B, Key K, X|} (serverKey C))     \
paulson@1929
   705
\                  : set_of_list evs; \
paulson@1929
   706
 \          Says S' A'                                         \
paulson@1929
   707
\             (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
paulson@1929
   708
\                  : set_of_list evs;                         \
paulson@1929
   709
\           evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
paulson@1893
   710
bd lemma 1;
paulson@1893
   711
be exE 1;
paulson@1893
   712
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
paulson@1893
   713
by (Fast_tac 1);
paulson@1893
   714
qed "unique_session_keys";
paulson@1885
   715
paulson@1885
   716
paulson@1885
   717
paulson@1885
   718
(*Crucial security property: Enemy does not see the keys sent in msg NS2
paulson@1885
   719
   -- even if another key is compromised*)
paulson@1885
   720
goal thy 
paulson@1885
   721
 "!!evs. [| Says Server (Friend i) \
paulson@1913
   722
\            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
paulson@1885
   723
\           evs : traces;  Friend i ~= C;  Friend j ~= C              \
paulson@1885
   724
\        |] ==>                                                       \
paulson@1913
   725
\     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
paulson@1885
   726
be rev_mp 1;
paulson@1885
   727
be traces.induct 1;
paulson@1893
   728
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
paulson@1885
   729
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
paulson@1885
   730
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
paulson@1885
   731
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
paulson@1885
   732
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
paulson@1885
   733
by (ALLGOALS 
paulson@1885
   734
    (asm_full_simp_tac 
paulson@1913
   735
     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
paulson@1913
   736
			  analz_insert_Key_newK] @ pushes)
paulson@1885
   737
               setloop split_tac [expand_if])));
paulson@1885
   738
(*NS2*)
paulson@1893
   739
by (fast_tac (!claset addSEs [less_irrefl]) 2);
paulson@1929
   740
(** LEVEL 8 **)
paulson@1885
   741
(*Now for the Fake case*)
paulson@1885
   742
br notI 1;
paulson@1885
   743
by (subgoal_tac 
paulson@1893
   744
    "Key (newK evt) : \
paulson@1913
   745
\    analz (synth (analz (insert (Key (serverKey C)) \
paulson@1885
   746
\                                  (sees Enemy evsa))))" 1);
paulson@1913
   747
be (impOfSubs analz_mono) 2;
paulson@1929
   748
by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
paulson@1929
   749
			       impOfSubs synth_increasing,
paulson@1929
   750
			       impOfSubs analz_increasing]) 0 2);
paulson@1885
   751
(*Proves the Fake goal*)
paulson@1885
   752
by (fast_tac (!claset addss (!simpset)) 1);
paulson@1885
   753
paulson@1929
   754
(**LEVEL 13**)
paulson@1929
   755
(*NS3: that message from the Server was sent earlier*)
paulson@1929
   756
by (mp_tac 1);
paulson@1929
   757
by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
paulson@1885
   758
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
paulson@1893
   759
by (asm_full_simp_tac
paulson@1913
   760
    (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
paulson@1929
   761
by (Step_tac 1);
paulson@1929
   762
(**LEVEL 18 **)
paulson@1929
   763
bd unique_session_keys 1;
paulson@1929
   764
by (REPEAT_FIRST assume_tac);
paulson@1893
   765
by (ALLGOALS Full_simp_tac);
paulson@1929
   766
by (Step_tac 1);
paulson@1913
   767
by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
paulson@1893
   768
qed "Enemy_not_see_encrypted_key";
paulson@1885
   769
paulson@1885
   770
paulson@1885
   771
paulson@1885
   772
paulson@1893
   773
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
paulson@1885
   774
paulson@1885
   775
paulson@1893
   776
goals_limit:=4;
paulson@1885
   777
paulson@1885
   778
paulson@1885
   779
paulson@1893
   780
goal thy 
paulson@1893
   781
 "!!evs. [| Says Server (Friend i) \
paulson@1913
   782
\             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
paulson@1893
   783
\           evs : traces;  i~=j    \
paulson@1913
   784
\         |] ==> K ~: analz (sees (Friend j) evs)";
paulson@1913
   785
br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1;
paulson@1893
   786
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
paulson@1893
   787
qed "Friend_not_see_encrypted_key";
paulson@1885
   788
paulson@1893
   789
goal thy 
paulson@1893
   790
 "!!evs. [| Says Server (Friend i) \
paulson@1913
   791
\             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
paulson@1893
   792
\           A ~: {Friend i, Server};  \
paulson@1893
   793
\           evs : traces    \
paulson@1913
   794
\        |] ==>  K ~: analz (sees A evs)";
paulson@1893
   795
by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
paulson@1893
   796
by (agent.induct_tac "A" 1);
paulson@1893
   797
by (ALLGOALS Simp_tac);
paulson@1893
   798
by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
paulson@1893
   799
				     Friend_not_see_encrypted_key]) 1);
paulson@1913
   800
br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
paulson@1893
   801
(*  hyp_subst_tac would deletes the equality assumption... *)
paulson@1893
   802
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
paulson@1893
   803
qed "Agent_not_see_encrypted_key";
paulson@1885
   804
paulson@1885
   805
paulson@1893
   806
(*Neatly packaged, perhaps in a useless form*)
paulson@1893
   807
goalw thy [knownBy_def]
paulson@1893
   808
 "!!evs. [| Says Server (Friend i) \
paulson@1913
   809
\             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
paulson@1893
   810
\           evs : traces    \
paulson@1893
   811
\        |] ==>  knownBy evs K <= {Friend i, Server}";
paulson@1885
   812
paulson@1893
   813
by (Step_tac 1);
paulson@1893
   814
br ccontr 1;
paulson@1893
   815
by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
paulson@1893
   816
qed "knownBy_encrypted_key";
paulson@1885
   817
paulson@1885
   818
paulson@1885
   819
paulson@1885
   820
paulson@1885
   821
paulson@1885
   822
paulson@1885
   823
paulson@1885
   824
push_proof();
paulson@1885
   825
goal thy 
paulson@1885
   826
 "!!evs. [| evs = Says S (Friend i) \
paulson@1885
   827
\                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
paulson@1885
   828
\           evs : traces;  i~=k                                    \
paulson@1885
   829
\        |] ==>                                                    \
paulson@1913
   830
\     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
paulson@1885
   831
be rev_mp 1;
paulson@1885
   832
be traces.induct 1;
paulson@1885
   833
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
paulson@1885
   834
by (Step_tac 1);
paulson@1913
   835
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
paulson@1885
   836
val Enemy_not_see_encrypted_key_lemma = result();
paulson@1885
   837
paulson@1885
   838
paulson@1885
   839
paulson@1885
   840
paulson@1885
   841
paulson@1885
   842
paulson@1885
   843
paulson@1913
   844
(*Precisely formulated as needed below.  Perhaps redundant, as simplification
paulson@1913
   845
  with the aid of  analz_subset_parts RS contra_subsetD  might do the
paulson@1913
   846
  same thing.*)
paulson@1913
   847
goal thy 
paulson@1913
   848
 "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
paulson@1913
   849
\        Key (serverKey A) ~:                               \
paulson@1913
   850
\          analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
paulson@1913
   851
br (analz_subset_parts RS contra_subsetD) 1;
paulson@1913
   852
by (Asm_simp_tac 1);
paulson@1913
   853
qed "insert_not_analz_serverKey";
paulson@1885
   854
paulson@1885
   855
paulson@1885
   856
paulson@1885
   857
paulson@1885
   858
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
paulson@1885
   859
proof_timing:=true;
paulson@1885
   860
paulson@1852
   861
paulson@1852
   862
paulson@1852
   863
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
paulson@1852
   864
paulson@1852
   865
paulson@1852
   866
paulson@1852
   867
(*If a message is sent, encrypted with a Friend's server key, then either
paulson@1852
   868
  that Friend or the Server originally sent it.*)
paulson@1852
   869
goal thy 
paulson@1852
   870
 "!!evs. evs : traces ==>                             \
paulson@1852
   871
\    ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
paulson@1913
   872
\        : set_of_list evs  -->   \
paulson@1913
   873
\    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \
paulson@1913
   874
\            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)";
paulson@1852
   875
be traces.induct 1;
paulson@1852
   876
by (Step_tac 1);
paulson@1852
   877
by (ALLGOALS Asm_full_simp_tac);
paulson@1852
   878
(*Remaining cases are Fake, NS2 and NS3*)
paulson@1852
   879
by (Fast_tac 2);	(*Proves the NS2 case*)
paulson@1852
   880
paulson@1852
   881
by (REPEAT (dtac spec 2));
paulson@1852
   882
fe conjE;
paulson@1852
   883
bd mp 2;
paulson@1852
   884
paulson@1852
   885
by (REPEAT (resolve_tac [refl, conjI] 2));
paulson@1852
   886
by (ALLGOALS Asm_full_simp_tac);
paulson@1852
   887
paulson@1852
   888
paulson@1852
   889
paulson@1852
   890
paulson@1852
   891
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
paulson@1852
   892
be conjE 2;
paulson@1852
   893
by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
paulson@1852
   894
paulson@1852
   895
(*The NS3 case needs the induction hypothesis twice!
paulson@1852
   896
    One application is to the X component of the most recent message.*)
paulson@1852
   897
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
paulson@1852
   898
by (Fast_tac 3);
paulson@1852
   899
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
paulson@1852
   900
be conjE 2;
paulson@1852
   901
(*DELETE the first quantified formula: it's now useless*)
paulson@1852
   902
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
paulson@1852
   903
by (fast_tac (!claset addss (!simpset)) 2);
paulson@1852
   904
(*Now for the Fake case*)
paulson@1852
   905
be disjE 1;
paulson@1852
   906
(*The subcase of Fake, where the message in question is NOT the most recent*)
paulson@1852
   907
by (Best_tac 2);
paulson@1852
   908
paulson@1852
   909
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
paulson@1913
   910
be Crypt_synth 1;
paulson@1913
   911
be Key_synth 2;
paulson@1852
   912
paulson@1913
   913
(*Split up the possibilities of that message being synthd...*)
paulson@1852
   914
by (Step_tac 1);
paulson@1852
   915
by (Best_tac 6);
paulson@1852
   916
paulson@1852
   917
paulson@1852
   918
paulson@1852
   919
paulson@1852
   920
paulson@1839
   921
(*NEEDED??*)
paulson@1839
   922
paulson@1839
   923
goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)";
paulson@1839
   924
by (asm_simp_tac (!simpset addsimps [sees_Cons] 
paulson@1839
   925
                           setloop split_tac [expand_if]) 1); 
paulson@1839
   926
qed "in_sees_Says";
paulson@1839
   927
paulson@1839
   928
goal thy "!!A. X ~: parts {Y} ==> \
paulson@1839
   929
\              (X : parts (sees A (Says B C Y # evs))) = \
paulson@1839
   930
\              (X : parts (sees A evs))";
paulson@1839
   931
by (asm_simp_tac (!simpset addsimps [sees_Cons] 
paulson@1839
   932
                           setloop split_tac [expand_if]) 1); 
paulson@1839
   933
by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); 
paulson@1839
   934
qed "in_parts_sees_Says";
paulson@1839
   935
paulson@1852
   936
goal thy "!!evs. length evs < length evs' ==> newK  evs ~= newK (A',evs')";
paulson@1839
   937
by (fast_tac (!claset addSEs [less_irrefl]) 1);
paulson@1839
   938
qed "length_less_newK_neq";
paulson@1839
   939
paulson@1839
   940
paulson@1839
   941
paulson@1839
   942
paulson@1839
   943
paulson@1839
   944
paulson@1839
   945
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
paulson@1839
   946
paulson@1839
   947
goalw thy [keysFor_def]
paulson@1839
   948
    "!!X. Crypt X K: H ==> invKey K : keysFor H";
paulson@1839
   949
by (Fast_tac 1);
paulson@1839
   950
qed "keysFor_I";
paulson@1839
   951
AddSIs [keysFor_I];
paulson@1839
   952
paulson@1839
   953
goalw thy [keysFor_def]
paulson@1839
   954
    "!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H";
paulson@1839
   955
by (Fast_tac 1);
paulson@1839
   956
qed "keysFor_D";
paulson@1839
   957
AddSDs [keysFor_D];
paulson@1839
   958
paulson@1839
   959