src/HOL/Auth/OtwayRees.ML
author paulson
Tue Sep 03 19:06:00 1996 +0200 (1996-09-03)
changeset 1945 20ca9cf90e69
parent 1941 f97a6e5b6375
child 1964 d551e68b7a36
permissions -rw-r--r--
A further tidying
paulson@1941
     1
(*  Title:      HOL/Auth/OtwayRees
paulson@1941
     2
    ID:         $Id$
paulson@1941
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1941
     4
    Copyright   1996  University of Cambridge
paulson@1941
     5
paulson@1941
     6
Inductive relation "otway" for the Otway-Rees protocol.
paulson@1941
     7
paulson@1941
     8
From page 244 of
paulson@1941
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@1941
    10
  Proc. Royal Soc. 426 (1989)
paulson@1941
    11
*)
paulson@1941
    12
paulson@1941
    13
open OtwayRees;
paulson@1941
    14
paulson@1941
    15
proof_timing:=true;
paulson@1941
    16
HOL_quantifiers := false;
paulson@1941
    17
paulson@1941
    18
(**** Inductive proofs about otway ****)
paulson@1941
    19
paulson@1941
    20
(*The Enemy can see more than anybody else, except for their initial state*)
paulson@1941
    21
goal thy 
paulson@1941
    22
 "!!evs. evs : otway ==> \
paulson@1941
    23
\     sees A evs <= initState A Un sees Enemy evs";
paulson@1941
    24
be otway.induct 1;
paulson@1941
    25
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
paulson@1941
    26
			        addss (!simpset))));
paulson@1941
    27
qed "sees_agent_subset_sees_Enemy";
paulson@1941
    28
paulson@1941
    29
paulson@1941
    30
(*Nobody sends themselves messages*)
paulson@1941
    31
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
paulson@1941
    32
be otway.induct 1;
paulson@1941
    33
by (Auto_tac());
paulson@1941
    34
qed_spec_mp "not_Says_to_self";
paulson@1941
    35
Addsimps [not_Says_to_self];
paulson@1941
    36
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@1941
    37
paulson@1941
    38
goal thy "!!evs. evs : otway ==> Notes A X ~: set_of_list evs";
paulson@1941
    39
be otway.induct 1;
paulson@1941
    40
by (Auto_tac());
paulson@1941
    41
qed "not_Notes";
paulson@1941
    42
Addsimps [not_Notes];
paulson@1941
    43
AddSEs   [not_Notes RSN (2, rev_notE)];
paulson@1941
    44
paulson@1941
    45
paulson@1941
    46
(** For reasoning about the encrypted portion of messages **)
paulson@1941
    47
paulson@1941
    48
goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
paulson@1941
    49
\                X : analz (sees Enemy evs)";
paulson@1941
    50
by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
paulson@1941
    51
qed "OR2_analz_sees_Enemy";
paulson@1941
    52
paulson@1941
    53
goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
paulson@1941
    54
\                X : analz (sees Enemy evs)";
paulson@1941
    55
by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
paulson@1941
    56
qed "OR4_analz_sees_Enemy";
paulson@1941
    57
paulson@1941
    58
goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
paulson@1941
    59
\                K : parts (sees Enemy evs)";
paulson@1941
    60
by (fast_tac (!claset addSEs partsEs
paulson@1941
    61
	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
paulson@1941
    62
qed "OR5_parts_sees_Enemy";
paulson@1941
    63
paulson@1941
    64
(*OR2_analz... and OR4_analz... let us treat those cases using the same 
paulson@1941
    65
  argument as for the Fake case.*)
paulson@1941
    66
val OR2_OR4_tac = 
paulson@1941
    67
    dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
paulson@1941
    68
    dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
paulson@1941
    69
paulson@1941
    70
paulson@1941
    71
(*** Shared keys are not betrayed ***)
paulson@1941
    72
paulson@1941
    73
(*Enemy never sees another agent's shared key!*)
paulson@1941
    74
goal thy 
paulson@1941
    75
 "!!evs. [| evs : otway; A ~= Enemy |] ==> \
paulson@1941
    76
\        Key (shrK A) ~: parts (sees Enemy evs)";
paulson@1941
    77
be otway.induct 1;
paulson@1941
    78
by OR2_OR4_tac;
paulson@1941
    79
by (Auto_tac());
paulson@1941
    80
(*Deals with Fake message*)
paulson@1941
    81
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@1941
    82
			     impOfSubs Fake_parts_insert]) 1);
paulson@1941
    83
qed "Enemy_not_see_shrK";
paulson@1941
    84
paulson@1941
    85
bind_thm ("Enemy_not_analz_shrK",
paulson@1941
    86
	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
paulson@1941
    87
paulson@1941
    88
Addsimps [Enemy_not_see_shrK, 
paulson@1941
    89
	  not_sym RSN (2, Enemy_not_see_shrK), 
paulson@1941
    90
	  Enemy_not_analz_shrK, 
paulson@1941
    91
	  not_sym RSN (2, Enemy_not_analz_shrK)];
paulson@1941
    92
paulson@1941
    93
(*We go to some trouble to preserve R in the 3rd subgoal*)
paulson@1941
    94
val major::prems = 
paulson@1941
    95
goal thy  "[| Key (shrK A) : parts (sees Enemy evs);    \
paulson@1941
    96
\             evs : otway;                                  \
paulson@1941
    97
\             A=Enemy ==> R                                  \
paulson@1941
    98
\           |] ==> R";
paulson@1941
    99
br ccontr 1;
paulson@1941
   100
br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
paulson@1941
   101
by (swap_res_tac prems 2);
paulson@1941
   102
by (ALLGOALS (fast_tac (!claset addIs prems)));
paulson@1941
   103
qed "Enemy_see_shrK_E";
paulson@1941
   104
paulson@1941
   105
bind_thm ("Enemy_analz_shrK_E", 
paulson@1941
   106
	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
paulson@1941
   107
paulson@1941
   108
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
paulson@1941
   109
AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
paulson@1941
   110
paulson@1941
   111
paulson@1941
   112
(*No Friend will ever see another agent's shared key 
paulson@1941
   113
  (excluding the Enemy, who might transmit his).
paulson@1941
   114
  The Server, of course, knows all shared keys.*)
paulson@1941
   115
goal thy 
paulson@1941
   116
 "!!evs. [| evs : otway; A ~= Enemy;  A ~= Friend j |] ==> \
paulson@1941
   117
\        Key (shrK A) ~: parts (sees (Friend j) evs)";
paulson@1941
   118
br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
paulson@1941
   119
by (ALLGOALS Asm_simp_tac);
paulson@1941
   120
qed "Friend_not_see_shrK";
paulson@1941
   121
paulson@1941
   122
paulson@1941
   123
(*Not for Addsimps -- it can cause goals to blow up!*)
paulson@1941
   124
goal thy  
paulson@1941
   125
 "!!evs. evs : otway ==>                                  \
paulson@1941
   126
\        (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) =  \
paulson@1941
   127
\        (A=B | A=Enemy)";
paulson@1941
   128
by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
paulson@1941
   129
		      addIs [impOfSubs (subset_insertI RS analz_mono)]
paulson@1941
   130
	              addss (!simpset)) 1);
paulson@1941
   131
qed "shrK_mem_analz";
paulson@1941
   132
paulson@1941
   133
paulson@1941
   134
(*** Future keys can't be seen or used! ***)
paulson@1941
   135
paulson@1941
   136
(*Nobody can have SEEN keys that will be generated in the future.
paulson@1941
   137
  This has to be proved anew for each protocol description,
paulson@1941
   138
  but should go by similar reasoning every time.  Hardest case is the
paulson@1941
   139
  standard Fake rule.  
paulson@1941
   140
      The length comparison, and Union over C, are essential for the 
paulson@1941
   141
  induction! *)
paulson@1941
   142
goal thy "!!evs. evs : otway ==> \
paulson@1941
   143
\                length evs <= length evs' --> \
paulson@1941
   144
\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
paulson@1941
   145
be otway.induct 1;
paulson@1941
   146
by OR2_OR4_tac;
paulson@1941
   147
(*auto_tac does not work here, as it performs safe_tac first*)
paulson@1941
   148
by (ALLGOALS Asm_simp_tac);
paulson@1941
   149
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@1941
   150
				       impOfSubs parts_insert_subset_Un,
paulson@1941
   151
				       Suc_leD]
paulson@1941
   152
			        addss (!simpset))));
paulson@1941
   153
val lemma = result();
paulson@1941
   154
paulson@1941
   155
(*Variant needed for the main theorem below*)
paulson@1941
   156
goal thy 
paulson@1941
   157
 "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
paulson@1941
   158
\        Key (newK evs') ~: parts (sees C evs)";
paulson@1941
   159
by (fast_tac (!claset addDs [lemma]) 1);
paulson@1941
   160
qed "new_keys_not_seen";
paulson@1941
   161
Addsimps [new_keys_not_seen];
paulson@1941
   162
paulson@1941
   163
(*Another variant: old messages must contain old keys!*)
paulson@1941
   164
goal thy 
paulson@1941
   165
 "!!evs. [| Says A B X : set_of_list evs;  \
paulson@1941
   166
\           Key (newK evt) : parts {X};    \
paulson@1941
   167
\           evs : otway                 \
paulson@1941
   168
\        |] ==> length evt < length evs";
paulson@1941
   169
br ccontr 1;
paulson@1941
   170
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
paulson@1941
   171
	              addIs [impOfSubs parts_mono, leI]) 1);
paulson@1941
   172
qed "Says_imp_old_keys";
paulson@1941
   173
paulson@1941
   174
paulson@1941
   175
(*Nobody can have USED keys that will be generated in the future.
paulson@1941
   176
  ...very like new_keys_not_seen*)
paulson@1941
   177
goal thy "!!evs. evs : otway ==> \
paulson@1941
   178
\                length evs <= length evs' --> \
paulson@1941
   179
\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
paulson@1941
   180
be otway.induct 1;
paulson@1941
   181
by OR2_OR4_tac;
paulson@1941
   182
bd OR5_parts_sees_Enemy 7;
paulson@1941
   183
by (ALLGOALS Asm_simp_tac);
paulson@1941
   184
(*OR1 and OR3*)
paulson@1941
   185
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
paulson@1941
   186
(*Fake, OR2, OR4: these messages send unknown (X) components*)
paulson@1941
   187
by (EVERY 
paulson@1941
   188
    (map
paulson@1941
   189
     (best_tac
paulson@1941
   190
      (!claset addSDs [newK_invKey]
paulson@1941
   191
	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
paulson@1941
   192
		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
paulson@1941
   193
		      Suc_leD]
paulson@1941
   194
	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
paulson@1941
   195
	       addss (!simpset)))
paulson@1941
   196
     [3,2,1]));
paulson@1941
   197
(*OR5: dummy message*)
paulson@1941
   198
by (best_tac (!claset addSDs [newK_invKey]
paulson@1941
   199
		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
paulson@1941
   200
			addIs  [less_SucI, impOfSubs keysFor_mono]
paulson@1941
   201
			addss (!simpset addsimps [le_def])) 1);
paulson@1941
   202
val lemma = result();
paulson@1941
   203
paulson@1941
   204
goal thy 
paulson@1941
   205
 "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
paulson@1941
   206
\        newK evs' ~: keysFor (parts (sees C evs))";
paulson@1941
   207
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
paulson@1941
   208
qed "new_keys_not_used";
paulson@1941
   209
paulson@1941
   210
bind_thm ("new_keys_not_analzd",
paulson@1941
   211
	  [analz_subset_parts RS keysFor_mono,
paulson@1941
   212
	   new_keys_not_used] MRS contra_subsetD);
paulson@1941
   213
paulson@1941
   214
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@1941
   215
paulson@1941
   216
paulson@1941
   217
(** Lemmas concerning the form of items passed in messages **)
paulson@1941
   218
paulson@1941
   219
paulson@1941
   220
(****
paulson@1941
   221
 The following is to prove theorems of the form
paulson@1941
   222
paulson@1941
   223
          Key K : analz (insert (Key (newK evt)) 
paulson@1941
   224
	                   (insert (Key (shrK C)) (sees Enemy evs))) ==>
paulson@1941
   225
          Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
paulson@1941
   226
paulson@1941
   227
 A more general formula must be proved inductively.
paulson@1941
   228
paulson@1941
   229
****)
paulson@1941
   230
paulson@1941
   231
paulson@1941
   232
(*NOT useful in this form, but it says that session keys are not used
paulson@1941
   233
  to encrypt messages containing other keys, in the actual protocol.
paulson@1941
   234
  We require that agents should behave like this subsequently also.*)
paulson@1941
   235
goal thy 
paulson@1941
   236
 "!!evs. evs : otway ==> \
paulson@1941
   237
\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
paulson@1941
   238
\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
paulson@1941
   239
be otway.induct 1;
paulson@1941
   240
by OR2_OR4_tac;
paulson@1941
   241
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
paulson@1941
   242
(*Deals with Faked messages*)
paulson@1941
   243
by (best_tac (!claset addSEs partsEs
paulson@1941
   244
		      addDs [impOfSubs analz_subset_parts,
paulson@1941
   245
                             impOfSubs parts_insert_subset_Un]
paulson@1941
   246
                      addss (!simpset)) 1);
paulson@1941
   247
(*OR5*)
paulson@1941
   248
by (fast_tac (!claset addss (!simpset)) 1);
paulson@1941
   249
result();
paulson@1941
   250
paulson@1941
   251
paulson@1941
   252
(** Specialized rewriting for this proof **)
paulson@1941
   253
paulson@1941
   254
Delsimps [image_insert];
paulson@1941
   255
Addsimps [image_insert RS sym];
paulson@1941
   256
paulson@1941
   257
goal thy "insert (Key (newK x)) (sees A evs) = \
paulson@1941
   258
\         Key `` (newK``{x}) Un (sees A evs)";
paulson@1941
   259
by (Fast_tac 1);
paulson@1941
   260
val insert_Key_singleton = result();
paulson@1941
   261
paulson@1941
   262
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
paulson@1941
   263
\         Key `` (f `` (insert x E)) Un C";
paulson@1941
   264
by (Fast_tac 1);
paulson@1941
   265
val insert_Key_image = result();
paulson@1941
   266
paulson@1941
   267
paulson@1941
   268
(*This lets us avoid analyzing the new message -- unless we have to!*)
paulson@1941
   269
(*NEEDED??*)
paulson@1941
   270
goal thy "synth (analz (sees Enemy evs)) <=   \
paulson@1941
   271
\         synth (analz (sees Enemy (Says A B X # evs)))";
paulson@1941
   272
by (Simp_tac 1);
paulson@1941
   273
br (subset_insertI RS analz_mono RS synth_mono) 1;
paulson@1941
   274
qed "synth_analz_thin";
paulson@1941
   275
paulson@1941
   276
AddIs [impOfSubs synth_analz_thin];
paulson@1941
   277
paulson@1941
   278
paulson@1941
   279
paulson@1941
   280
(** Session keys are not used to encrypt other session keys **)
paulson@1941
   281
paulson@1941
   282
(*Could generalize this so that the X component doesn't have to be first
paulson@1941
   283
  in the message?*)
paulson@1941
   284
val enemy_analz_tac =
paulson@1941
   285
  SELECT_GOAL 
paulson@1941
   286
   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
paulson@1941
   287
	   dtac (impOfSubs Fake_analz_insert) 1,
paulson@1941
   288
	   eresolve_tac [asm_rl, synth.Inj] 1,
paulson@1941
   289
	   Fast_tac 1,
paulson@1941
   290
	   Asm_full_simp_tac 1,
paulson@1941
   291
	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
paulson@1941
   292
	   ]);
paulson@1941
   293
paulson@1941
   294
paulson@1941
   295
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@1941
   296
goal thy  
paulson@1941
   297
 "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \
paulson@1941
   298
\          (K : nE | Key K : analz (insert KsC sEe))  ==>     \
paulson@1941
   299
\        (Key K : analz (insert KsC (Key``nE Un sEe))) = \
paulson@1941
   300
\          (K : nE | Key K : analz (insert KsC sEe))";
paulson@1941
   301
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
paulson@1941
   302
val lemma = result();
paulson@1941
   303
paulson@1941
   304
goal thy  
paulson@1941
   305
 "!!evs. evs : otway ==> \
paulson@1941
   306
\  ALL K E. (Key K : analz (insert (Key (shrK C)) \
paulson@1941
   307
\                             (Key``(newK``E) Un (sees Enemy evs)))) = \
paulson@1941
   308
\           (K : newK``E |  \
paulson@1941
   309
\            Key K : analz (insert (Key (shrK C)) \
paulson@1941
   310
\                             (sees Enemy evs)))";
paulson@1941
   311
be otway.induct 1;
paulson@1941
   312
bd OR2_analz_sees_Enemy 4;
paulson@1941
   313
bd OR4_analz_sees_Enemy 6;
paulson@1941
   314
by (REPEAT_FIRST (resolve_tac [allI, lemma]));
paulson@1941
   315
by (ALLGOALS (*Takes 40 secs*)
paulson@1941
   316
    (asm_simp_tac 
paulson@1941
   317
     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
paulson@1941
   318
			 @ pushes)
paulson@1941
   319
               setloop split_tac [expand_if])));
paulson@1941
   320
(*OR4*) 
paulson@1941
   321
by (enemy_analz_tac 5);
paulson@1941
   322
(*OR3*)
paulson@1941
   323
by (Fast_tac 4);
paulson@1941
   324
(*OR2*) (** LEVEL 11 **)
paulson@1941
   325
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
paulson@1941
   326
    (insert_commute RS ssubst) 3);
paulson@1941
   327
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
paulson@1941
   328
    (insert_commute RS ssubst) 3);
paulson@1941
   329
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
paulson@1941
   330
by (enemy_analz_tac 3);
paulson@1941
   331
(*Fake case*) (** LEVEL 6 **)
paulson@1941
   332
by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
paulson@1941
   333
    (insert_commute RS ssubst) 2);
paulson@1941
   334
by (enemy_analz_tac 2);
paulson@1941
   335
(*Base case*)
paulson@1941
   336
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
paulson@1941
   337
qed_spec_mp "analz_image_newK";
paulson@1941
   338
paulson@1941
   339
paulson@1941
   340
goal thy
paulson@1941
   341
 "!!evs. evs : otway ==>                               \
paulson@1941
   342
\        Key K : analz (insert (Key (newK evt))            \
paulson@1941
   343
\                         (insert (Key (shrK C))      \
paulson@1941
   344
\                          (sees Enemy evs))) =            \
paulson@1941
   345
\             (K = newK evt |                              \
paulson@1941
   346
\              Key K : analz (insert (Key (shrK C))   \
paulson@1941
   347
\                               (sees Enemy evs)))";
paulson@1941
   348
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
paulson@1941
   349
				   insert_Key_singleton]) 1);
paulson@1941
   350
by (Fast_tac 1);
paulson@1941
   351
qed "analz_insert_Key_newK";
paulson@1941
   352
paulson@1941
   353
paulson@1941
   354
(*Describes the form *and age* of K when the following message is sent*)
paulson@1941
   355
goal thy 
paulson@1941
   356
 "!!evs. [| Says Server B \
paulson@1941
   357
\            {|NA, Crypt {|NA, K|} (shrK A),                      \
paulson@1941
   358
\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
paulson@1941
   359
\           evs : otway |]                                        \
paulson@1941
   360
\        ==> (EX evt:otway. K = Key(newK evt) & \
paulson@1941
   361
\                           length evt < length evs) &            \
paulson@1941
   362
\            (EX i. NA = Nonce i)";
paulson@1941
   363
be rev_mp 1;
paulson@1941
   364
be otway.induct 1;
paulson@1941
   365
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
paulson@1941
   366
qed "Says_Server_message_form";
paulson@1941
   367
paulson@1941
   368
paulson@1941
   369
(*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*)
paulson@1941
   370
goal thy 
paulson@1941
   371
 "!!evs. [| Says Server (Friend j) \
paulson@1941
   372
\            {|Ni, Crypt {|Ni, K|} (shrK (Friend i)),                      \
paulson@1941
   373
\                  Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs;  \
paulson@1941
   374
\           evs : otway;  Friend i ~= C;  Friend j ~= C              \
paulson@1941
   375
\        |] ==>                                                       \
paulson@1941
   376
\     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
paulson@1941
   377
be rev_mp 1;
paulson@1941
   378
be otway.induct 1;
paulson@1941
   379
bd OR2_analz_sees_Enemy 4;
paulson@1941
   380
bd OR4_analz_sees_Enemy 6;
paulson@1941
   381
by (ALLGOALS Asm_simp_tac);
paulson@1941
   382
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
paulson@1941
   383
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
paulson@1941
   384
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
paulson@1941
   385
by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
paulson@1941
   386
by (ALLGOALS 
paulson@1941
   387
    (asm_full_simp_tac 
paulson@1941
   388
     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
paulson@1941
   389
			  analz_insert_Key_newK] @ pushes)
paulson@1941
   390
               setloop split_tac [expand_if])));
paulson@1941
   391
(*OR3*)
paulson@1941
   392
by (fast_tac (!claset addSEs [less_irrefl]) 3);
paulson@1941
   393
(*Fake*) (** LEVEL 8 **)
paulson@1941
   394
by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
paulson@1941
   395
by (enemy_analz_tac 1);
paulson@1941
   396
(*OR4*)
paulson@1941
   397
by (mp_tac 2);
paulson@1941
   398
by (enemy_analz_tac 2);
paulson@1941
   399
(*OR2*)
paulson@1941
   400
by (mp_tac 1);
paulson@1941
   401
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
paulson@1941
   402
    (insert_commute RS ssubst) 1);
paulson@1941
   403
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@1941
   404
by (enemy_analz_tac 1);
paulson@1941
   405
qed "Enemy_not_see_encrypted_key";
paulson@1945
   406
paulson@1945
   407
paulson@1945
   408
paulson@1945
   409
(*** Session keys are issued at most once, and identify the principals ***)
paulson@1945
   410
paulson@1945
   411
(** First, two lemmas for the Fake, OR2 and OR4 cases **)
paulson@1945
   412
paulson@1945
   413
goal thy 
paulson@1945
   414
 "!!evs. [| X : synth (analz (sees Enemy evs));       \
paulson@1945
   415
\           Crypt X' (shrK C) : parts{X};             \
paulson@1945
   416
\           C ~= Enemy;   evs : otway |]              \
paulson@1945
   417
\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
paulson@1945
   418
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
paulson@1945
   419
	              addDs [impOfSubs parts_insert_subset_Un]
paulson@1945
   420
                      addss (!simpset)) 1);
paulson@1945
   421
qed "Crypt_Fake_parts";
paulson@1945
   422
paulson@1945
   423
goal thy 
paulson@1945
   424
 "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
paulson@1945
   425
\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
paulson@1945
   426
\            Crypt X' K : parts {Y}";
paulson@1945
   427
bd parts_singleton 1;
paulson@1945
   428
by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
paulson@1945
   429
qed "Crypt_parts_singleton";
paulson@1945
   430
paulson@1945
   431
fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
paulson@1945
   432
paulson@1945
   433
(*The Key K uniquely identifies a pair of senders in the message encrypted by
paulson@1945
   434
  C, but if C=Enemy then he could send all sorts of nonsense.*)
paulson@1945
   435
goal thy 
paulson@1945
   436
 "!!evs. evs : otway ==>                        \
paulson@1945
   437
\      EX A B. ALL C.                    \
paulson@1945
   438
\         C ~= Enemy -->                        \
paulson@1945
   439
\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
paulson@1945
   440
\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
paulson@1945
   441
by (Simp_tac 1);
paulson@1945
   442
be otway.induct 1;
paulson@1945
   443
bd OR2_analz_sees_Enemy 4;
paulson@1945
   444
bd OR4_analz_sees_Enemy 6;
paulson@1945
   445
by (ALLGOALS 
paulson@1945
   446
    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
paulson@1945
   447
by (REPEAT_FIRST (etac exE));
paulson@1945
   448
(*OR4*)
paulson@1945
   449
by (ex_strip_tac 4);
paulson@1945
   450
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
paulson@1945
   451
			      Crypt_parts_singleton]) 4);
paulson@1945
   452
(*OR3: Case split propagates some context to other subgoal...*)
paulson@1945
   453
	(** LEVEL 8 **)
paulson@1945
   454
by (excluded_middle_tac "K = newK evsa" 3);
paulson@1945
   455
by (Asm_simp_tac 3);
paulson@1945
   456
by (REPEAT (ares_tac [exI] 3));
paulson@1945
   457
(*...we prove this case by contradiction: the key is too new!*)
paulson@1945
   458
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
paulson@1945
   459
		      addSEs partsEs
paulson@1945
   460
		      addEs [Says_imp_old_keys RS less_irrefl]
paulson@1945
   461
	              addss (!simpset)) 3);
paulson@1945
   462
(*OR2*) (** LEVEL 12 **)
paulson@1945
   463
by (ex_strip_tac 2);
paulson@1945
   464
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
paulson@1945
   465
    (insert_commute RS ssubst) 2);
paulson@1945
   466
by (Simp_tac 2);
paulson@1945
   467
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
paulson@1945
   468
			      Crypt_parts_singleton]) 2);
paulson@1945
   469
(*Fake*) (** LEVEL 16 **)
paulson@1945
   470
by (ex_strip_tac 1);
paulson@1945
   471
by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
paulson@1945
   472
qed "unique_session_keys";
paulson@1945
   473
paulson@1945
   474
(*It seems strange but this theorem is NOT needed to prove the main result!*)