src/HOL/Auth/Recur.ML
author paulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 3686 4b484805b4c4
parent 3683 aafe719dff14
child 3730 6933d20f335f
permissions -rw-r--r--
First working version with Oops event for session keys
paulson@2449
     1
(*  Title:      HOL/Auth/Recur
paulson@2449
     2
    ID:         $Id$
paulson@2449
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2449
     4
    Copyright   1996  University of Cambridge
paulson@2449
     5
paulson@2449
     6
Inductive relation "recur" for the Recursive Authentication protocol.
paulson@2449
     7
*)
paulson@2449
     8
paulson@2449
     9
open Recur;
paulson@2449
    10
paulson@2449
    11
proof_timing:=true;
paulson@2449
    12
HOL_quantifiers := false;
paulson@2516
    13
Pretty.setdepth 30;
paulson@2449
    14
paulson@2449
    15
paulson@2449
    16
(** Possibility properties: traces that reach the end 
paulson@2516
    17
        ONE theorem would be more elegant and faster!
paulson@2516
    18
        By induction on a list of agents (no repetitions)
paulson@2449
    19
**)
paulson@2449
    20
paulson@2516
    21
paulson@2449
    22
(*Simplest case: Alice goes directly to the server*)
paulson@2481
    23
goal thy
paulson@3483
    24
 "!!A. A ~= Server                                                      \
paulson@3519
    25
\ ==> EX K NA. EX evs: recur.                                      \
paulson@2516
    26
\     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
paulson@3466
    27
\                     Agent Server|}  : set evs";
paulson@2449
    28
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2451
    29
by (rtac (recur.Nil RS recur.RA1 RS 
paulson@2516
    30
          (respond.One RSN (4,recur.RA3))) 2);
paulson@2516
    31
by possibility_tac;
paulson@2449
    32
result();
paulson@2449
    33
paulson@2449
    34
paulson@2449
    35
(*Case two: Alice, Bob and the server*)
paulson@2481
    36
goal thy
paulson@3483
    37
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                 \
paulson@3519
    38
\ ==> EX K. EX NA. EX evs: recur.                          \
paulson@2516
    39
\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
paulson@3466
    40
\                  Agent Server|}  : set evs";
paulson@2516
    41
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
paulson@2516
    42
by (REPEAT (eresolve_tac [exE, conjE] 1));
paulson@2449
    43
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2451
    44
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
paulson@2516
    45
          (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
paulson@2516
    46
          recur.RA4) 2);
paulson@2516
    47
by basic_possibility_tac;
paulson@2516
    48
by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
paulson@2516
    49
			       less_not_refl2 RS not_sym] 1));
paulson@2449
    50
result();
paulson@2449
    51
paulson@2449
    52
paulson@2516
    53
(*Case three: Alice, Bob, Charlie and the server
paulson@2533
    54
  TOO SLOW to run every time!
paulson@2481
    55
goal thy
paulson@2516
    56
 "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
paulson@3519
    57
\ ==> EX K. EX NA. EX evs: recur.                                 \
paulson@3483
    58
\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
paulson@3466
    59
\                  Agent Server|}  : set evs";
paulson@2516
    60
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
paulson@2516
    61
by (REPEAT (eresolve_tac [exE, conjE] 1));
paulson@2449
    62
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2451
    63
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
paulson@2516
    64
          (respond.One RS respond.Cons RS respond.Cons RSN
paulson@2516
    65
           (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
paulson@2516
    66
(*SLOW: 70 seconds*)
paulson@2516
    67
by basic_possibility_tac;
paulson@2516
    68
by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
paulson@2516
    69
		 ORELSE
paulson@2516
    70
		 eresolve_tac [asm_rl, less_not_refl2, 
paulson@2516
    71
			       less_not_refl2 RS not_sym] 1));
paulson@2449
    72
result();
paulson@2516
    73
****************)
paulson@2449
    74
paulson@2449
    75
(**** Inductive proofs about recur ****)
paulson@2449
    76
paulson@2449
    77
(*Nobody sends themselves messages*)
paulson@3519
    78
goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
paulson@2449
    79
by (etac recur.induct 1);
paulson@2449
    80
by (Auto_tac());
paulson@2449
    81
qed_spec_mp "not_Says_to_self";
paulson@2449
    82
Addsimps [not_Says_to_self];
paulson@2449
    83
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@2449
    84
paulson@2449
    85
paulson@2516
    86
paulson@2516
    87
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
paulson@2516
    88
by (etac respond.induct 1);
paulson@2516
    89
by (ALLGOALS Simp_tac);
paulson@2516
    90
qed "respond_Key_in_parts";
paulson@2516
    91
paulson@2516
    92
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
paulson@2516
    93
by (etac respond.induct 1);
paulson@2516
    94
by (REPEAT (assume_tac 1));
paulson@2516
    95
qed "respond_imp_not_used";
paulson@2516
    96
paulson@2516
    97
goal thy
paulson@2516
    98
 "!!evs. [| Key K : parts {RB};  (PB,RB,K') : respond evs |] \
paulson@2516
    99
\        ==> Key K ~: used evs";
paulson@2516
   100
by (etac rev_mp 1);
paulson@2516
   101
by (etac respond.induct 1);
paulson@2516
   102
by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
paulson@2516
   103
             !simpset));
paulson@2516
   104
qed_spec_mp "Key_in_parts_respond";
paulson@2516
   105
paulson@2449
   106
(*Simple inductive reasoning about responses*)
paulson@2516
   107
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
paulson@2449
   108
by (etac respond.induct 1);
paulson@2516
   109
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
paulson@2449
   110
qed "respond_imp_responses";
paulson@2449
   111
paulson@2449
   112
paulson@2449
   113
(** For reasoning about the encrypted portion of messages **)
paulson@2449
   114
paulson@3683
   115
val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
paulson@2449
   116
nipkow@3465
   117
goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
paulson@3683
   118
\                ==> RA : analz (spies evs)";
paulson@3683
   119
by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
paulson@3683
   120
qed "RA4_analz_spies";
paulson@2449
   121
paulson@2451
   122
(*RA2_analz... and RA4_analz... let us treat those cases using the same 
paulson@2449
   123
  argument as for the Fake case.  This is possible for most, but not all,
paulson@2451
   124
  proofs: Fake does not invent new nonces (as in RA2), and of course Fake
paulson@2449
   125
  messages originate from the Spy. *)
paulson@2449
   126
paulson@3683
   127
bind_thm ("RA2_parts_spies",
paulson@3683
   128
          RA2_analz_spies RS (impOfSubs analz_subset_parts));
paulson@3683
   129
bind_thm ("RA4_parts_spies",
paulson@3683
   130
          RA4_analz_spies RS (impOfSubs analz_subset_parts));
paulson@2449
   131
paulson@3683
   132
(*For proving the easier theorems about X ~: parts (spies evs).*)
paulson@3519
   133
fun parts_induct_tac i = 
paulson@3519
   134
    etac recur.induct i				THEN
paulson@3683
   135
    forward_tac [RA2_parts_spies] (i+3)	THEN
paulson@3519
   136
    etac subst (i+3) (*RA2: DELETE needless definition of PA!*)  THEN
paulson@3519
   137
    forward_tac [respond_imp_responses] (i+4)	THEN
paulson@3683
   138
    forward_tac [RA4_parts_spies] (i+5)	THEN
paulson@3519
   139
    prove_simple_subgoals_tac i;
paulson@2449
   140
paulson@2449
   141
paulson@3683
   142
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@2449
   143
    sends messages containing X! **)
paulson@2449
   144
paulson@2449
   145
paulson@3683
   146
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
paulson@2449
   147
paulson@2449
   148
goal thy 
paulson@3683
   149
 "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
paulson@3519
   150
by (parts_induct_tac 1);
paulson@3121
   151
by (Fake_parts_insert_tac 1);
paulson@3121
   152
by (ALLGOALS 
paulson@3683
   153
    (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_spies])));
paulson@2550
   154
(*RA3*)
paulson@3121
   155
by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
paulson@2451
   156
(*RA2*)
paulson@3121
   157
by (blast_tac (!claset addSEs partsEs  addDs [parts_cut]) 1);
paulson@2449
   158
qed "Spy_see_shrK";
paulson@2449
   159
Addsimps [Spy_see_shrK];
paulson@2449
   160
paulson@2449
   161
goal thy 
paulson@3683
   162
 "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
paulson@2449
   163
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@2449
   164
qed "Spy_analz_shrK";
paulson@2449
   165
Addsimps [Spy_analz_shrK];
paulson@2449
   166
paulson@3683
   167
goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : recur |] ==> A:bad";
paulson@3121
   168
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
paulson@2449
   169
qed "Spy_see_shrK_D";
paulson@2449
   170
paulson@2449
   171
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
paulson@2449
   172
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
paulson@2449
   173
paulson@2449
   174
paulson@2516
   175
paulson@2516
   176
(** Nobody can have used non-existent keys! **)
paulson@2449
   177
paulson@2516
   178
goal thy
paulson@2516
   179
 "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
paulson@2516
   180
\        ==> K : range shrK";
paulson@2516
   181
by (etac rev_mp 1);
paulson@2516
   182
by (etac (respond_imp_responses RS responses.induct) 1);
paulson@2449
   183
by (Auto_tac());
paulson@2516
   184
qed_spec_mp "Key_in_keysFor_parts";
paulson@2449
   185
paulson@2449
   186
paulson@3519
   187
goal thy "!!evs. evs : recur ==>          \
paulson@3683
   188
\                Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
paulson@3519
   189
by (parts_induct_tac 1);
paulson@2451
   190
(*RA3*)
paulson@2516
   191
by (best_tac (!claset addDs  [Key_in_keysFor_parts]
paulson@3683
   192
	      addss  (!simpset addsimps [parts_insert_spies])) 2);
paulson@2516
   193
(*Fake*)
paulson@2516
   194
by (best_tac
paulson@2516
   195
      (!claset addIs [impOfSubs analz_subset_parts]
paulson@2516
   196
               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
paulson@2516
   197
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
oheimb@3207
   198
               addss (!simpset)) 1);
paulson@2449
   199
qed_spec_mp "new_keys_not_used";
paulson@2449
   200
paulson@2449
   201
paulson@2449
   202
bind_thm ("new_keys_not_analzd",
paulson@2449
   203
          [analz_subset_parts RS keysFor_mono,
paulson@2449
   204
           new_keys_not_used] MRS contra_subsetD);
paulson@2449
   205
paulson@2449
   206
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@2449
   207
paulson@2449
   208
paulson@2449
   209
paulson@2449
   210
(*** Proofs involving analz ***)
paulson@2449
   211
paulson@3519
   212
(*For proofs involving analz.*)
paulson@3683
   213
val analz_spies_tac = 
paulson@2485
   214
    etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
paulson@3683
   215
    dtac RA2_analz_spies 4 THEN 
paulson@2449
   216
    forward_tac [respond_imp_responses] 5                THEN
paulson@3683
   217
    dtac RA4_analz_spies 6;
paulson@2449
   218
paulson@2449
   219
paulson@2449
   220
(** Session keys are not used to encrypt other session keys **)
paulson@2449
   221
paulson@2451
   222
(*Version for "responses" relation.  Handles case RA3 in the theorem below.  
paulson@3683
   223
  Note that it holds for *any* set H (not just "spies evs")
paulson@2449
   224
  satisfying the inductive hypothesis.*)
paulson@2449
   225
goal thy  
paulson@2516
   226
 "!!evs. [| RB : responses evs;                             \
paulson@2516
   227
\           ALL K KK. KK <= Compl (range shrK) -->          \
paulson@2516
   228
\                     (Key K : analz (Key``KK Un H)) =      \
paulson@2516
   229
\                     (K : KK | Key K : analz H) |]         \
paulson@2516
   230
\       ==> ALL K KK. KK <= Compl (range shrK) -->          \
paulson@2516
   231
\                     (Key K : analz (insert RB (Key``KK Un H))) = \
paulson@2516
   232
\                     (K : KK | Key K : analz (insert RB H))";
paulson@2516
   233
by (etac responses.induct 1);
paulson@2516
   234
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
paulson@2516
   235
qed "resp_analz_image_freshK_lemma";
paulson@2449
   236
paulson@2449
   237
(*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
paulson@2449
   238
goal thy  
paulson@3519
   239
 "!!evs. evs : recur ==>                                    \
paulson@3519
   240
\  ALL K KK. KK <= Compl (range shrK) -->                   \
paulson@3683
   241
\            (Key K : analz (Key``KK Un (spies evs))) =  \
paulson@3683
   242
\            (K : KK | Key K : analz (spies evs))";
paulson@2449
   243
by (etac recur.induct 1);
paulson@3683
   244
by analz_spies_tac;
paulson@2516
   245
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@2516
   246
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
paulson@2516
   247
by (ALLGOALS 
paulson@2516
   248
    (asm_simp_tac
paulson@2516
   249
     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
paulson@2449
   250
(*Base*)
paulson@3121
   251
by (Blast_tac 1);
paulson@3451
   252
(*Fake*) 
paulson@3451
   253
by (spy_analz_tac 1);
paulson@2516
   254
val raw_analz_image_freshK = result();
paulson@2516
   255
qed_spec_mp "analz_image_freshK";
paulson@2449
   256
paulson@2449
   257
paulson@3683
   258
(*Instance of the lemma with H replaced by (spies evs):
paulson@3519
   259
   [| RB : responses evs;  evs : recur; |]
paulson@2516
   260
   ==> KK <= Compl (range shrK) --> 
paulson@3683
   261
       Key K : analz (insert RB (Key``KK Un spies evs)) =
paulson@3683
   262
       (K : KK | Key K : analz (insert RB (spies evs))) 
paulson@2449
   263
*)
paulson@2516
   264
bind_thm ("resp_analz_image_freshK",
paulson@2516
   265
          raw_analz_image_freshK RSN
paulson@2516
   266
            (2, resp_analz_image_freshK_lemma) RS spec RS spec);
paulson@2449
   267
paulson@2449
   268
goal thy
paulson@3519
   269
 "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>              \
paulson@3683
   270
\        Key K : analz (insert (Key KAB) (spies evs)) =      \
paulson@3683
   271
\        (K = KAB | Key K : analz (spies evs))";
paulson@2516
   272
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@2516
   273
qed "analz_insert_freshK";
paulson@2449
   274
paulson@2449
   275
paulson@2516
   276
(*Everything that's hashed is already in past traffic. *)
paulson@3683
   277
goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs);  \
paulson@3683
   278
\                   evs : recur;  A ~: bad |]                       \
paulson@3683
   279
\                ==> X : parts (spies evs)";
paulson@2550
   280
by (etac rev_mp 1);
paulson@3519
   281
by (parts_induct_tac 1);
paulson@2451
   282
(*RA3 requires a further induction*)
paulson@3121
   283
by (etac responses.induct 2);
paulson@2449
   284
by (ALLGOALS Asm_simp_tac);
paulson@2449
   285
(*Fake*)
paulson@3683
   286
by (simp_tac (!simpset addsimps [parts_insert_spies]) 1);
paulson@3121
   287
by (Fake_parts_insert_tac 1);
paulson@2550
   288
qed "Hash_imp_body";
paulson@2449
   289
paulson@2449
   290
paulson@2449
   291
(** The Nonce NA uniquely identifies A's message. 
paulson@2516
   292
    This theorem applies to steps RA1 and RA2!
paulson@2455
   293
paulson@2455
   294
  Unicity is not used in other proofs but is desirable in its own right.
paulson@2449
   295
**)
paulson@2449
   296
paulson@2449
   297
goal thy 
paulson@3683
   298
 "!!evs. [| evs : recur; A ~: bad |]                   \
paulson@2560
   299
\ ==> EX B' P'. ALL B P.                                     \
paulson@3683
   300
\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
paulson@2560
   301
\          -->  B=B' & P=P'";
paulson@3519
   302
by (parts_induct_tac 1);
paulson@3121
   303
by (Fake_parts_insert_tac 1);
paulson@2516
   304
by (etac responses.induct 3);
paulson@2485
   305
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
paulson@2449
   306
by (step_tac (!claset addSEs partsEs) 1);
paulson@2516
   307
(*RA1,2: creation of new Nonce.  Move assertion into global context*)
paulson@2516
   308
by (ALLGOALS (expand_case_tac "NA = ?y"));
paulson@2516
   309
by (REPEAT_FIRST (ares_tac [exI]));
paulson@3121
   310
by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
paulson@3683
   311
                               addSEs spies_partsEs) 1));
paulson@2449
   312
val lemma = result();
paulson@2449
   313
paulson@2481
   314
goalw thy [HPair_def]
paulson@3683
   315
 "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(spies evs); \
paulson@3683
   316
\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \
paulson@3683
   317
\        evs : recur;  A ~: bad |]                                     \
paulson@3483
   318
\      ==> B=B' & P=P'";
paulson@2481
   319
by (REPEAT (eresolve_tac partsEs 1));
paulson@2449
   320
by (prove_unique_tac lemma 1);
paulson@2449
   321
qed "unique_NA";
paulson@2449
   322
paulson@2449
   323
paulson@2449
   324
(*** Lemmas concerning the Server's response
paulson@2449
   325
      (relations "respond" and "responses") 
paulson@2449
   326
***)
paulson@2449
   327
paulson@2449
   328
goal thy
paulson@3519
   329
 "!!evs. [| RB : responses evs;  evs : recur |] \
paulson@3683
   330
\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
paulson@2516
   331
by (etac responses.induct 1);
paulson@2449
   332
by (ALLGOALS
paulson@2449
   333
    (asm_simp_tac 
paulson@2516
   334
     (analz_image_freshK_ss addsimps [Spy_analz_shrK,
paulson@2516
   335
                                      resp_analz_image_freshK])));
paulson@2449
   336
qed "shrK_in_analz_respond";
paulson@2449
   337
Addsimps [shrK_in_analz_respond];
paulson@2449
   338
paulson@2449
   339
paulson@2449
   340
goal thy  
paulson@2516
   341
 "!!evs. [| RB : responses evs;                             \
paulson@2516
   342
\           ALL K KK. KK <= Compl (range shrK) -->          \
paulson@2516
   343
\                     (Key K : analz (Key``KK Un H)) =      \
paulson@2516
   344
\                     (K : KK | Key K : analz H) |]         \
paulson@3483
   345
\       ==> (Key K : analz (insert RB H)) -->               \
paulson@2516
   346
\           (Key K : parts{RB} | Key K : analz H)";
paulson@2516
   347
by (etac responses.induct 1);
paulson@2449
   348
by (ALLGOALS
paulson@2449
   349
    (asm_simp_tac 
paulson@2516
   350
     (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
paulson@2516
   351
(*Simplification using two distinct treatments of "image"*)
paulson@2516
   352
by (simp_tac (!simpset addsimps [parts_insert2]) 1);
paulson@3121
   353
by (blast_tac (!claset delrules [allE]) 1);
paulson@2449
   354
qed "resp_analz_insert_lemma";
paulson@2449
   355
paulson@2449
   356
bind_thm ("resp_analz_insert",
paulson@2516
   357
          raw_analz_image_freshK RSN
paulson@2516
   358
            (2, resp_analz_insert_lemma) RSN(2, rev_mp));
paulson@2449
   359
paulson@2449
   360
paulson@2449
   361
(*The Server does not send such messages.  This theorem lets us avoid
paulson@2451
   362
  assuming B~=Server in RA4.*)
paulson@2449
   363
goal thy 
paulson@3519
   364
 "!!evs. evs : recur \
paulson@3483
   365
\        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
paulson@2449
   366
by (etac recur.induct 1);
paulson@2516
   367
by (etac (respond.induct) 5);
paulson@2449
   368
by (Auto_tac());
paulson@2449
   369
qed_spec_mp "Says_Server_not";
paulson@2449
   370
AddSEs [Says_Server_not RSN (2,rev_notE)];
paulson@2449
   371
paulson@2449
   372
paulson@2516
   373
(*The last key returned by respond indeed appears in a certificate*)
paulson@2449
   374
goal thy 
paulson@2516
   375
 "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
paulson@2516
   376
\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
paulson@2516
   377
by (etac respond.elim 1);
paulson@2516
   378
by (ALLGOALS Asm_full_simp_tac);
paulson@2516
   379
qed "respond_certificate";
paulson@2516
   380
paulson@2516
   381
paulson@2516
   382
goal thy 
paulson@2560
   383
 "!!K'. (PB,RB,KXY) : respond evs                          \
paulson@2560
   384
\  ==> EX A' B'. ALL A B N.                                \
paulson@2449
   385
\        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
paulson@2449
   386
\          -->   (A'=A & B'=B) | (A'=B & B'=A)";
paulson@2516
   387
by (etac respond.induct 1);
paulson@2449
   388
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
paulson@2449
   389
(*Base case*)
paulson@3121
   390
by (Blast_tac 1);
paulson@2449
   391
by (Step_tac 1);
paulson@2550
   392
by (expand_case_tac "K = KBC" 1);
paulson@2516
   393
by (dtac respond_Key_in_parts 1);
paulson@3121
   394
by (blast_tac (!claset addSIs [exI]
paulson@3519
   395
                       addSEs partsEs
paulson@3519
   396
                       addDs [Key_in_parts_respond]) 1);
paulson@2550
   397
by (expand_case_tac "K = KAB" 1);
paulson@2449
   398
by (REPEAT (ares_tac [exI] 2));
paulson@2449
   399
by (ex_strip_tac 1);
paulson@2516
   400
by (dtac respond_certificate 1);
paulson@2449
   401
by (Fast_tac 1);
paulson@2449
   402
val lemma = result();
paulson@2449
   403
paulson@2449
   404
goal thy 
paulson@2560
   405
 "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};      \
paulson@2449
   406
\          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
paulson@2560
   407
\          (PB,RB,KXY) : respond evs |]                            \
paulson@2449
   408
\ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
paulson@2560
   409
by (prove_unique_tac lemma 1);
paulson@2449
   410
qed "unique_session_keys";
paulson@2449
   411
paulson@2449
   412
paulson@2451
   413
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
paulson@2449
   414
    Does not in itself guarantee security: an attack could violate 
paulson@2449
   415
    the premises, e.g. by having A=Spy **)
paulson@2449
   416
paulson@2449
   417
goal thy 
paulson@3519
   418
 "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur |]              \
paulson@3683
   419
\        ==> ALL A A' N. A ~: bad & A' ~: bad -->                 \
paulson@2449
   420
\            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
paulson@3683
   421
\            Key K ~: analz (insert RB (spies evs))";
paulson@2516
   422
by (etac respond.induct 1);
paulson@2449
   423
by (forward_tac [respond_imp_responses] 2);
paulson@2516
   424
by (forward_tac [respond_imp_not_used] 2);
paulson@3681
   425
by (ALLGOALS (*12 seconds*)
paulson@2449
   426
    (asm_simp_tac 
paulson@2516
   427
     (analz_image_freshK_ss addsimps 
paulson@2533
   428
       [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
paulson@3681
   429
by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib])));
paulson@3681
   430
(** LEVEL 5 **)
paulson@3121
   431
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
paulson@2449
   432
by (step_tac (!claset addSEs [MPair_parts]) 1);
paulson@3681
   433
by (REPEAT (blast_tac (!claset addSDs [respond_certificate]
paulson@3681
   434
		               addDs [resp_analz_insert]
paulson@3681
   435
			       addIs  [impOfSubs analz_subset_parts]) 4));
paulson@3681
   436
by (Blast_tac 3);
paulson@3121
   437
by (blast_tac (!claset addSEs partsEs
paulson@3121
   438
                       addDs [Key_in_parts_respond]) 2);
paulson@3683
   439
(*by unicity, either B=Aa or B=A', a contradiction since B: bad*)
paulson@2516
   440
by (dtac unique_session_keys 1);
paulson@2516
   441
by (etac respond_certificate 1);
paulson@2516
   442
by (assume_tac 1);
paulson@3121
   443
by (Blast_tac 1);
paulson@2533
   444
qed_spec_mp "respond_Spy_not_see_session_key";
paulson@2449
   445
paulson@2449
   446
paulson@2449
   447
goal thy
paulson@3683
   448
 "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
paulson@3683
   449
\           A ~: bad;  A' ~: bad;  evs : recur |]   \
paulson@3683
   450
\        ==> Key K ~: analz (spies evs)";
paulson@2550
   451
by (etac rev_mp 1);
paulson@2449
   452
by (etac recur.induct 1);
paulson@3683
   453
by analz_spies_tac;
paulson@2449
   454
by (ALLGOALS
paulson@2449
   455
    (asm_simp_tac
paulson@3683
   456
     (!simpset addsimps [parts_insert_spies, analz_insert_freshK] 
paulson@2449
   457
               setloop split_tac [expand_if])));
paulson@2451
   458
(*RA4*)
paulson@2533
   459
by (spy_analz_tac 5);
paulson@2533
   460
(*RA2*)
paulson@2533
   461
by (spy_analz_tac 3);
paulson@2449
   462
(*Fake*)
paulson@2533
   463
by (spy_analz_tac 2);
paulson@2533
   464
(*Base*)
paulson@3121
   465
by (Blast_tac 1);
paulson@2533
   466
(*RA3 remains*)
paulson@2449
   467
by (step_tac (!claset delrules [impCE]) 1);
paulson@2451
   468
(*RA3, case 2: K is an old key*)
paulson@3121
   469
by (blast_tac (!claset addSDs [resp_analz_insert]
paulson@3121
   470
                       addSEs partsEs
paulson@3121
   471
                       addDs [Key_in_parts_respond]) 2);
paulson@2451
   472
(*RA3, case 1: use lemma previously proved by induction*)
paulson@3121
   473
by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
paulson@3121
   474
			       (2,rev_notE)]) 1);
paulson@2550
   475
qed "Spy_not_see_session_key";
paulson@2449
   476
paulson@2449
   477
paulson@2449
   478
(**** Authenticity properties for Agents ****)
paulson@2449
   479
paulson@2481
   480
(*The response never contains Hashes*)
paulson@2481
   481
goal thy
paulson@2550
   482
 "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
paulson@2550
   483
\           (PB,RB,K) : respond evs |]                      \
paulson@2550
   484
\        ==> Hash {|Key (shrK B), M|} : parts H";
paulson@2550
   485
by (etac rev_mp 1);
paulson@2516
   486
by (etac (respond_imp_responses RS responses.induct) 1);
paulson@2481
   487
by (Auto_tac());
paulson@2550
   488
qed "Hash_in_parts_respond";
paulson@2481
   489
paulson@2533
   490
(*Only RA1 or RA2 can have caused such a part of a message to appear.
paulson@2533
   491
  This result is of no use to B, who cannot verify the Hash.  Moreover,
paulson@2533
   492
  it can say nothing about how recent A's message is.  It might later be
paulson@2533
   493
  used to prove B's presence to A at the run's conclusion.*)
paulson@2481
   494
goalw thy [HPair_def]
paulson@3683
   495
 "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
paulson@3683
   496
\           A ~: bad;  evs : recur |]                      \
paulson@3466
   497
\     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
paulson@2516
   498
by (etac rev_mp 1);
paulson@3519
   499
by (parts_induct_tac 1);
paulson@3121
   500
by (Fake_parts_insert_tac 1);
paulson@2451
   501
(*RA3*)
paulson@3121
   502
by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
paulson@2449
   503
qed_spec_mp "Hash_auth_sender";
paulson@2449
   504
paulson@2516
   505
(** These two results subsume (for all agents) the guarantees proved
paulson@2449
   506
    separately for A and B in the Otway-Rees protocol.
paulson@2449
   507
**)
paulson@2449
   508
paulson@2449
   509
paulson@2533
   510
(*Certificates can only originate with the Server.*)
paulson@2449
   511
goal thy 
paulson@3683
   512
 "!!evs. [| Crypt (shrK A) Y : parts (spies evs);    \
paulson@3683
   513
\           A ~: bad;  A ~= Spy;  evs : recur |]       \
paulson@3519
   514
\        ==> EX C RC. Says Server C RC : set evs  &     \
paulson@2550
   515
\                     Crypt (shrK A) Y : parts {RC}";
paulson@2550
   516
by (etac rev_mp 1);
paulson@3519
   517
by (parts_induct_tac 1);
paulson@3121
   518
by (Fake_parts_insert_tac 1);
paulson@2451
   519
(*RA4*)
paulson@3121
   520
by (Blast_tac 4);
paulson@2455
   521
(*RA3*)
paulson@3683
   522
by (full_simp_tac (!simpset addsimps [parts_insert_spies]) 3
paulson@3121
   523
    THEN Blast_tac 3);
paulson@2455
   524
(*RA1*)
paulson@3121
   525
by (Blast_tac 1);
paulson@2451
   526
(*RA2: it cannot be a new Nonce, contradiction.*)
paulson@3121
   527
by (Blast_tac 1);
paulson@2550
   528
qed "Cert_imp_Server_msg";