src/HOL/Auth/OtwayRees.ML
author paulson
Tue Sep 03 16:43:31 1996 +0200 (1996-09-03)
changeset 1941 f97a6e5b6375
child 1945 20ca9cf90e69
permissions -rw-r--r--
Initial working proof of Otway-Rees protocol
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
(*** Session keys are issued at most once, and identify the principals ***)
paulson@1941
   355
paulson@1941
   356
(*NOW WE HAVE... 
paulson@1941
   357
          Says S B
paulson@1941
   358
           {|Nonce NA, Crypt {|Nonce NA, Key (newK evta)|} (shrK A),
paulson@1941
   359
            Crypt {|Nonce NB, Key (newK evta)|} (shrK B)|} 
paulson@1941
   360
AND
paulson@1941
   361
          Says Server (Friend j)
paulson@1941
   362
           {|Ni, Crypt {|Ni, Key (newK evta)|} (shrK (Friend i)),
paulson@1941
   363
            Crypt {|Nj, Key (newK evta)|} (shrK (Friend j))|} 
paulson@1941
   364
THUS
paulson@1941
   365
          A = Friend i | A = Friend j
paulson@1941
   366
AND THIS LETS US PROVE IT!!
paulson@1941
   367
*)
paulson@1941
   368
paulson@1941
   369
goal thy 
paulson@1941
   370
 "!!evs. [| X : synth (analz (sees Enemy evs));       \
paulson@1941
   371
\           Crypt X' (shrK C) : parts{X};             \
paulson@1941
   372
\           C ~= Enemy;   evs : otway |]              \
paulson@1941
   373
\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
paulson@1941
   374
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
paulson@1941
   375
	              addDs [impOfSubs parts_insert_subset_Un]
paulson@1941
   376
                      addss (!simpset)) 1);
paulson@1941
   377
qed "Crypt_Fake_parts";
paulson@1941
   378
paulson@1941
   379
goal thy 
paulson@1941
   380
 "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
paulson@1941
   381
\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
paulson@1941
   382
\            Crypt X' K : parts {Y}";
paulson@1941
   383
bd parts_singleton 1;
paulson@1941
   384
by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
paulson@1941
   385
qed "Crypt_parts_singleton";
paulson@1941
   386
paulson@1941
   387
fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
paulson@1941
   388
paulson@1941
   389
(*The Key K uniquely identifies a pair of senders in the message encrypted by
paulson@1941
   390
  C, but if C=Enemy then he could send all sorts of nonsense.*)
paulson@1941
   391
goal thy 
paulson@1941
   392
 "!!evs. evs : otway ==>                        \
paulson@1941
   393
\      EX A B. ALL C S S' X NA.                    \
paulson@1941
   394
\         C ~= Enemy -->                        \
paulson@1941
   395
\         Says S S' X : set_of_list evs -->     \
paulson@1941
   396
\           (Crypt {|NA, Key K|} (shrK C) : parts{X} --> C=A | C=B)";
paulson@1941
   397
be otway.induct 1;
paulson@1941
   398
bd OR2_analz_sees_Enemy 4;
paulson@1941
   399
bd OR4_analz_sees_Enemy 6;
paulson@1941
   400
by (ALLGOALS 
paulson@1941
   401
    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
paulson@1941
   402
by (REPEAT_FIRST (etac exE));
paulson@1941
   403
(*OR4*)
paulson@1941
   404
by (ex_strip_tac 4);
paulson@1941
   405
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
paulson@1941
   406
			      Crypt_parts_singleton]) 4);
paulson@1941
   407
(*OR3: Case split propagates some context to other subgoal...*)
paulson@1941
   408
	(** LEVEL 8 **)
paulson@1941
   409
by (excluded_middle_tac "K = newK evsa" 3);
paulson@1941
   410
by (Asm_simp_tac 3);
paulson@1941
   411
by (REPEAT (ares_tac [exI] 3));
paulson@1941
   412
(*...we prove this case by contradiction: the key is too new!*)
paulson@1941
   413
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
paulson@1941
   414
		      addSEs partsEs
paulson@1941
   415
		      addEs [Says_imp_old_keys RS less_irrefl]
paulson@1941
   416
	              addss (!simpset)) 3);
paulson@1941
   417
(*OR2*) (** LEVEL 12 **)
paulson@1941
   418
by (ex_strip_tac 2);
paulson@1941
   419
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
paulson@1941
   420
    (insert_commute RS ssubst) 2);
paulson@1941
   421
by (Simp_tac 2);
paulson@1941
   422
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
paulson@1941
   423
			      Crypt_parts_singleton]) 2);
paulson@1941
   424
(*Fake*) (** LEVEL 16 **)
paulson@1941
   425
by (ex_strip_tac 1);
paulson@1941
   426
by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
paulson@1941
   427
qed "unique_session_keys";
paulson@1941
   428
paulson@1941
   429
paulson@1941
   430
(*Describes the form *and age* of K when the following message is sent*)
paulson@1941
   431
goal thy 
paulson@1941
   432
 "!!evs. [| Says Server B \
paulson@1941
   433
\            {|NA, Crypt {|NA, K|} (shrK A),                      \
paulson@1941
   434
\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
paulson@1941
   435
\           evs : otway |]                                        \
paulson@1941
   436
\        ==> (EX evt:otway. K = Key(newK evt) & \
paulson@1941
   437
\                           length evt < length evs) &            \
paulson@1941
   438
\            (EX i. NA = Nonce i)";
paulson@1941
   439
be rev_mp 1;
paulson@1941
   440
be otway.induct 1;
paulson@1941
   441
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
paulson@1941
   442
qed "Says_Server_message_form";
paulson@1941
   443
paulson@1941
   444
paulson@1941
   445
(*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*)
paulson@1941
   446
goal thy 
paulson@1941
   447
 "!!evs. [| Says Server (Friend j) \
paulson@1941
   448
\            {|Ni, Crypt {|Ni, K|} (shrK (Friend i)),                      \
paulson@1941
   449
\                  Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs;  \
paulson@1941
   450
\           evs : otway;  Friend i ~= C;  Friend j ~= C              \
paulson@1941
   451
\        |] ==>                                                       \
paulson@1941
   452
\     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
paulson@1941
   453
be rev_mp 1;
paulson@1941
   454
be otway.induct 1;
paulson@1941
   455
bd OR2_analz_sees_Enemy 4;
paulson@1941
   456
bd OR4_analz_sees_Enemy 6;
paulson@1941
   457
by (ALLGOALS Asm_simp_tac);
paulson@1941
   458
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
paulson@1941
   459
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
paulson@1941
   460
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
paulson@1941
   461
by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
paulson@1941
   462
by (ALLGOALS 
paulson@1941
   463
    (asm_full_simp_tac 
paulson@1941
   464
     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
paulson@1941
   465
			  analz_insert_Key_newK] @ pushes)
paulson@1941
   466
               setloop split_tac [expand_if])));
paulson@1941
   467
(*OR3*)
paulson@1941
   468
by (fast_tac (!claset addSEs [less_irrefl]) 3);
paulson@1941
   469
(*Fake*) (** LEVEL 8 **)
paulson@1941
   470
by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
paulson@1941
   471
by (enemy_analz_tac 1);
paulson@1941
   472
(*OR4*)
paulson@1941
   473
by (mp_tac 2);
paulson@1941
   474
by (enemy_analz_tac 2);
paulson@1941
   475
(*OR2*)
paulson@1941
   476
by (mp_tac 1);
paulson@1941
   477
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
paulson@1941
   478
    (insert_commute RS ssubst) 1);
paulson@1941
   479
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@1941
   480
by (enemy_analz_tac 1);
paulson@1941
   481
qed "Enemy_not_see_encrypted_key";