src/HOL/Auth/TLS.ML
author paulson
Mon Sep 22 13:17:29 1997 +0200 (1997-09-22)
changeset 3687 fb7d096d7884
parent 3686 4b484805b4c4
child 3704 2f99d7a0dccc
permissions -rw-r--r--
Simplified SpyKeys to use sessionK instead of clientK and serverK
Proved and used analz_insert_key, shortening scripts
paulson@3474
     1
(*  Title:      HOL/Auth/TLS
paulson@3474
     2
    ID:         $Id$
paulson@3474
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3474
     4
    Copyright   1997  University of Cambridge
paulson@3474
     5
paulson@3480
     6
Protocol goals: 
paulson@3480
     7
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
paulson@3480
     8
     parties (though A is not necessarily authenticated).
paulson@3480
     9
paulson@3685
    10
* B upon receiving CertVerify knows that A is present (But this
paulson@3480
    11
    message is optional!)
paulson@3474
    12
paulson@3685
    13
* A upon receiving ServerFinished knows that B is present
paulson@3480
    14
paulson@3480
    15
* Each party who has received a FINISHED message can trust that the other
paulson@3480
    16
  party agrees on all message components, including XA and XB (thus foiling
paulson@3480
    17
  rollback attacks).
paulson@3474
    18
*)
paulson@3474
    19
paulson@3474
    20
open TLS;
paulson@3474
    21
paulson@3474
    22
proof_timing:=true;
paulson@3474
    23
HOL_quantifiers := false;
paulson@3474
    24
paulson@3519
    25
(** We mostly DO NOT unfold the definition of "certificate".  The attached
paulson@3519
    26
    lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
paulson@3519
    27
    contexts.
paulson@3519
    28
**)
paulson@3519
    29
paulson@3519
    30
goalw thy [certificate_def] 
paulson@3519
    31
    "parts (insert (certificate B KB) H) =  \
paulson@3519
    32
\    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
paulson@3519
    33
by (rtac refl 1);
paulson@3519
    34
qed "parts_insert_certificate";
paulson@3474
    35
paulson@3519
    36
goalw thy [certificate_def] 
paulson@3519
    37
    "analz (insert (certificate B KB) H) =  \
paulson@3519
    38
\    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
paulson@3519
    39
by (rtac refl 1);
paulson@3519
    40
qed "analz_insert_certificate";
paulson@3519
    41
Addsimps [parts_insert_certificate, analz_insert_certificate];
paulson@3519
    42
paulson@3519
    43
goalw thy [certificate_def] 
paulson@3519
    44
    "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
paulson@3480
    45
by (Blast_tac 1);
paulson@3519
    46
qed "eq_certificate_iff";
paulson@3519
    47
AddIffs [eq_certificate_iff];
paulson@3519
    48
paulson@3480
    49
paulson@3474
    50
(*Injectiveness of key-generating functions*)
paulson@3677
    51
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
paulson@3474
    52
paulson@3677
    53
(* invKey(sessionK x) = sessionK x*)
paulson@3677
    54
Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
paulson@3480
    55
paulson@3474
    56
paulson@3474
    57
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
paulson@3474
    58
paulson@3677
    59
goal thy "pubK A ~= sessionK arg";
paulson@3474
    60
br notI 1;
paulson@3474
    61
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    62
by (Full_simp_tac 1);
paulson@3677
    63
qed "pubK_neq_sessionK";
paulson@3474
    64
paulson@3677
    65
goal thy "priK A ~= sessionK arg";
paulson@3474
    66
br notI 1;
paulson@3474
    67
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    68
by (Full_simp_tac 1);
paulson@3677
    69
qed "priK_neq_sessionK";
paulson@3474
    70
paulson@3677
    71
val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
paulson@3515
    72
AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
paulson@3474
    73
paulson@3474
    74
paulson@3474
    75
(**** Protocol Proofs ****)
paulson@3474
    76
paulson@3474
    77
(*A "possibility property": there are traces that reach the end.
paulson@3474
    78
  This protocol has three end points and six messages to consider.*)
paulson@3474
    79
paulson@3672
    80
paulson@3672
    81
(** These proofs make the further assumption that the Nonce_supply nonces 
paulson@3672
    82
	(which have the form  @ N. Nonce N ~: used evs)
paulson@3672
    83
    lie outside the range of PRF.  This assumption seems reasonable, but
paulson@3672
    84
    as it is needed only for the possibility theorems, it is not taken
paulson@3672
    85
    as an axiom.
paulson@3672
    86
**)
paulson@3672
    87
paulson@3672
    88
paulson@3685
    89
(*Possibility property ending with ClientAccepts.*)
paulson@3474
    90
goal thy 
paulson@3672
    91
 "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
paulson@3685
    92
\           A ~= B |] ==> EX SID M. EX evs: tls.    \
paulson@3685
    93
\  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
paulson@3474
    94
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
    95
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3685
    96
	RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2);
paulson@3474
    97
by possibility_tac;
paulson@3672
    98
by (REPEAT (Blast_tac 1));
paulson@3474
    99
result();
paulson@3474
   100
paulson@3685
   101
(*And one for ServerAccepts.  Either FINISHED message may come first.*)
paulson@3474
   102
goal thy 
paulson@3672
   103
 "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
paulson@3676
   104
\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
paulson@3685
   105
\  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
paulson@3474
   106
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   107
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3685
   108
	  RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2);
paulson@3474
   109
by possibility_tac;
paulson@3672
   110
by (REPEAT (Blast_tac 1));
paulson@3474
   111
result();
paulson@3474
   112
paulson@3474
   113
(*Another one, for CertVerify (which is optional)*)
paulson@3474
   114
goal thy 
paulson@3672
   115
 "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
paulson@3672
   116
\           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
paulson@3474
   117
\  Says A B (Crypt (priK A)                 \
paulson@3672
   118
\            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
paulson@3474
   119
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3506
   120
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3506
   121
	  RS tls.CertVerify) 2);
paulson@3474
   122
by possibility_tac;
paulson@3672
   123
by (REPEAT (Blast_tac 1));
paulson@3474
   124
result();
paulson@3474
   125
paulson@3685
   126
(*Another one, for session resumption (both ServerResume and ClientResume) *)
paulson@3685
   127
goal thy 
paulson@3685
   128
 "!!A B. [| evs0 : tls;     \
paulson@3685
   129
\           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
paulson@3685
   130
\           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
paulson@3685
   131
\           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
paulson@3685
   132
\           A ~= B |] ==> EX NA XA NB XB. EX evs: tls.    \
paulson@3685
   133
\  Says A B (Crypt (clientK(NA,NB,M))                           \
paulson@3685
   134
\            (Hash{|Nonce M, Number SID,             \
paulson@3685
   135
\                   Nonce NA, Number XA, Agent A,      \
paulson@3685
   136
\                   Nonce NB, Number XB, Agent B|})) : set evs";
paulson@3685
   137
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3685
   138
by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
paulson@3685
   139
by possibility_tac;
paulson@3685
   140
by (REPEAT (Blast_tac 1));
paulson@3685
   141
result();
paulson@3685
   142
paulson@3685
   143
paulson@3474
   144
paulson@3474
   145
(**** Inductive proofs about tls ****)
paulson@3474
   146
paulson@3474
   147
(*Nobody sends themselves messages*)
paulson@3474
   148
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
paulson@3474
   149
by (etac tls.induct 1);
paulson@3474
   150
by (Auto_tac());
paulson@3474
   151
qed_spec_mp "not_Says_to_self";
paulson@3474
   152
Addsimps [not_Says_to_self];
paulson@3474
   153
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@3474
   154
paulson@3474
   155
paulson@3519
   156
(*Induction for regularity theorems.  If induction formula has the form
paulson@3683
   157
   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
paulson@3683
   158
   needless information about analz (insert X (spies evs))  *)
paulson@3519
   159
fun parts_induct_tac i = 
paulson@3519
   160
    etac tls.induct i
paulson@3519
   161
    THEN 
paulson@3519
   162
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
paulson@3519
   163
    THEN 
paulson@3519
   164
    fast_tac (!claset addss (!simpset)) i THEN
paulson@3519
   165
    ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
paulson@3519
   166
paulson@3519
   167
paulson@3683
   168
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@3474
   169
    sends messages containing X! **)
paulson@3474
   170
paulson@3683
   171
(*Spy never sees another agent's private key! (unless it's bad at start)*)
paulson@3474
   172
goal thy 
paulson@3683
   173
 "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
paulson@3519
   174
by (parts_induct_tac 1);
paulson@3474
   175
by (Fake_parts_insert_tac 1);
paulson@3474
   176
qed "Spy_see_priK";
paulson@3474
   177
Addsimps [Spy_see_priK];
paulson@3474
   178
paulson@3474
   179
goal thy 
paulson@3683
   180
 "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
paulson@3474
   181
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@3474
   182
qed "Spy_analz_priK";
paulson@3474
   183
Addsimps [Spy_analz_priK];
paulson@3474
   184
paulson@3683
   185
goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
paulson@3683
   186
\                  evs : tls |] ==> A:bad";
paulson@3474
   187
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
paulson@3474
   188
qed "Spy_see_priK_D";
paulson@3474
   189
paulson@3474
   190
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
paulson@3474
   191
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
paulson@3474
   192
paulson@3474
   193
paulson@3515
   194
(*This lemma says that no false certificates exist.  One might extend the
paulson@3519
   195
  model to include bogus certificates for the agents, but there seems
paulson@3515
   196
  little point in doing so: the loss of their private keys is a worse
paulson@3515
   197
  breach of security.*)
paulson@3515
   198
goalw thy [certificate_def]
paulson@3515
   199
 "!!evs. evs : tls     \
paulson@3683
   200
\        ==> certificate B KB : parts (spies evs) --> KB = pubK B";
paulson@3519
   201
by (parts_induct_tac 1);
paulson@3519
   202
by (Fake_parts_insert_tac 1);
paulson@3515
   203
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
paulson@3515
   204
paulson@3515
   205
paulson@3515
   206
(*Replace key KB in ClientCertKeyEx by (pubK B) *)
paulson@3515
   207
val ClientCertKeyEx_tac = 
paulson@3683
   208
    forward_tac [Says_imp_spies RS parts.Inj RS 
paulson@3515
   209
		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
paulson@3515
   210
    THEN' assume_tac
paulson@3515
   211
    THEN' hyp_subst_tac;
paulson@3515
   212
paulson@3515
   213
fun analz_induct_tac i = 
paulson@3515
   214
    etac tls.induct i   THEN
paulson@3515
   215
    ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
paulson@3515
   216
    ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
paulson@3515
   217
    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
paulson@3515
   218
    ALLGOALS (asm_simp_tac 
paulson@3672
   219
              (!simpset addcongs [if_weak_cong]
paulson@3515
   220
                        setloop split_tac [expand_if]))  THEN
paulson@3515
   221
    (*Remove instances of pubK B:  the Spy already knows all public keys.
paulson@3515
   222
      Combining the two simplifier calls makes them run extremely slowly.*)
paulson@3515
   223
    ALLGOALS (asm_simp_tac 
paulson@3672
   224
              (!simpset addcongs [if_weak_cong]
paulson@3672
   225
			addsimps [insert_absorb]
paulson@3515
   226
                        setloop split_tac [expand_if]));
paulson@3515
   227
paulson@3515
   228
paulson@3685
   229
(*** Notes are made under controlled circumstances ***)
paulson@3515
   230
paulson@3515
   231
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
paulson@3683
   232
\                ==> Crypt (pubK B) X : parts (spies evs)";
paulson@3515
   233
by (etac rev_mp 1);
paulson@3515
   234
by (analz_induct_tac 1);
paulson@3515
   235
by (blast_tac (!claset addIs [parts_insertI]) 1);
paulson@3683
   236
qed "Notes_Crypt_parts_spies";
paulson@3515
   237
paulson@3685
   238
(*C might be either A or B*)
paulson@3685
   239
goal thy
paulson@3685
   240
    "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce M|} : set evs;  \
paulson@3685
   241
\              evs : tls     \
paulson@3685
   242
\           |] ==> M : range PRF";
paulson@3685
   243
by (etac rev_mp 1);
paulson@3685
   244
by (parts_induct_tac 1);
paulson@3685
   245
by (Auto_tac());
paulson@3685
   246
qed "Notes_master_range_PRF";
paulson@3515
   247
paulson@3685
   248
(*C might be either A or B*)
paulson@3685
   249
goal thy
paulson@3685
   250
 "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \
paulson@3685
   251
\             : set evs;     evs : tls     \
paulson@3685
   252
\        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
paulson@3685
   253
by (etac rev_mp 1);
paulson@3685
   254
by (parts_induct_tac 1);
paulson@3685
   255
(*Fake*)
paulson@3685
   256
by (blast_tac (!claset addIs [parts_insertI]) 1);
paulson@3685
   257
(*Client, Server Accept*)
paulson@3685
   258
by (Step_tac 1);
paulson@3685
   259
by (REPEAT (blast_tac (!claset addSEs spies_partsEs
paulson@3685
   260
                               addSDs [Notes_Crypt_parts_spies]) 1));
paulson@3685
   261
qed "Notes_master_imp_Crypt_PMS";
paulson@3685
   262
paulson@3685
   263
(*Compared with the theorem above, both premise and conclusion are stronger*)
paulson@3685
   264
goal thy
paulson@3685
   265
 "!!evs. [| Notes A {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \
paulson@3685
   266
\             : set evs;     evs : tls     \
paulson@3685
   267
\        |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
paulson@3685
   268
by (etac rev_mp 1);
paulson@3685
   269
by (parts_induct_tac 1);
paulson@3685
   270
(*ServerAccepts*)
paulson@3685
   271
by (Fast_tac 1);	(*Blast_tac's very slow here*)
paulson@3685
   272
qed "Notes_master_imp_Notes_PMS";
paulson@3685
   273
paulson@3685
   274
paulson@3685
   275
(*Every Nonce that's hashed is already in past traffic; this event
paulson@3685
   276
  occurs in CertVerify.  The condition NB ~: range PRF excludes the 
paulson@3685
   277
  MASTER SECRET from consideration; it is created using PRF.*)
paulson@3685
   278
goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs);  \
paulson@3685
   279
\                   NB ~: range PRF;  evs : tls |]  \
paulson@3685
   280
\                ==> Nonce NB : parts (spies evs)";
paulson@3685
   281
by (etac rev_mp 1);
paulson@3685
   282
by (etac rev_mp 1);
paulson@3685
   283
by (parts_induct_tac 1);
paulson@3685
   284
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
paulson@3685
   285
(*Server/Client Resume: wrong sort of nonce!*)
paulson@3685
   286
by (REPEAT (blast_tac (!claset addSDs [Notes_master_range_PRF]) 5));
paulson@3685
   287
(*FINISHED messages are trivial because M : range PRF*)
paulson@3685
   288
by (REPEAT (Blast_tac 3));
paulson@3685
   289
(*CertVerify is the only interesting case*)
paulson@3685
   290
by (blast_tac (!claset addSEs spies_partsEs) 2);
paulson@3685
   291
by (Fake_parts_insert_tac 1);
paulson@3685
   292
qed "Hash_Nonce_CV";
paulson@3685
   293
paulson@3685
   294
paulson@3685
   295
paulson@3685
   296
(*** Protocol goal: if B receives CertVerify, then A sent it ***)
paulson@3474
   297
paulson@3506
   298
(*B can check A's signature if he has received A's certificate.
paulson@3506
   299
  Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
paulson@3480
   300
  message is Fake.  We don't need guarantees for the Spy anyway.  We must
paulson@3683
   301
  assume A~:bad; otherwise, the Spy can forge A's signature.*)
paulson@3519
   302
goal thy
paulson@3506
   303
 "!!evs. [| X = Crypt (priK A)                                        \
paulson@3672
   304
\                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
paulson@3683
   305
\           evs : tls;  A ~: bad;  B ~= Spy |]                       \
paulson@3676
   306
\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
paulson@3506
   307
\          : set evs --> \
paulson@3683
   308
\        X : parts (spies evs) --> Says A B X : set evs";
paulson@3480
   309
by (hyp_subst_tac 1);
paulson@3519
   310
by (parts_induct_tac 1);
paulson@3474
   311
by (Fake_parts_insert_tac 1);
paulson@3480
   312
(*ServerHello: nonce NB cannot be in X because it's fresh!*)
paulson@3672
   313
by (blast_tac (!claset addSDs [Hash_Nonce_CV]
paulson@3683
   314
	               addSEs spies_partsEs) 1);
paulson@3474
   315
qed_spec_mp "TrustCertVerify";
paulson@3474
   316
paulson@3474
   317
paulson@3685
   318
(*If CertVerify is present then A has chosen PMS.*)
paulson@3506
   319
goal thy
paulson@3672
   320
 "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
paulson@3683
   321
\             : parts (spies evs);                                \
paulson@3683
   322
\           evs : tls;  A ~: bad |]                                      \
paulson@3672
   323
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
paulson@3515
   324
be rev_mp 1;
paulson@3519
   325
by (parts_induct_tac 1);
paulson@3519
   326
by (Fake_parts_insert_tac 1);
paulson@3515
   327
qed "UseCertVerify";
paulson@3474
   328
paulson@3480
   329
paulson@3687
   330
(*Key compromise lemma needed to prove analz_image_keys.
paulson@3687
   331
  No collection of keys can help the spy get new private keys.*)
paulson@3480
   332
goal thy  
paulson@3480
   333
 "!!evs. evs : tls ==>                                    \
paulson@3683
   334
\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
paulson@3687
   335
\          (priK B : KK | B : bad)";
paulson@3480
   336
by (etac tls.induct 1);
paulson@3515
   337
by (ALLGOALS
paulson@3519
   338
    (asm_simp_tac (analz_image_keys_ss
paulson@3677
   339
		   addsimps (analz_insert_certificate::keys_distinct))));
paulson@3480
   340
(*Fake*) 
paulson@3480
   341
by (spy_analz_tac 2);
paulson@3480
   342
(*Base*)
paulson@3480
   343
by (Blast_tac 1);
paulson@3480
   344
qed_spec_mp "analz_image_priK";
paulson@3480
   345
paulson@3480
   346
paulson@3480
   347
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@3480
   348
goal thy  
paulson@3480
   349
 "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
paulson@3480
   350
\        (X : analz (G Un H))  =  (X : analz H)";
paulson@3480
   351
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
paulson@3480
   352
val lemma = result();
paulson@3480
   353
paulson@3677
   354
(*slightly speeds up the big simplification below*)
paulson@3677
   355
goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
paulson@3677
   356
by (Blast_tac 1);
paulson@3677
   357
val range_sessionkeys_not_priK = result();
paulson@3677
   358
paulson@3687
   359
(** It is a mystery to me why the following formulation is actually slower
paulson@3687
   360
    in simplification:
paulson@3687
   361
paulson@3687
   362
\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
paulson@3687
   363
\           (Nonce N : analz (spies evs))";
paulson@3687
   364
paulson@3687
   365
More so as it can take advantage of unconditional rewrites such as 
paulson@3687
   366
     priK B ~: sessionK``Z
paulson@3687
   367
**)
paulson@3687
   368
paulson@3480
   369
goal thy  
paulson@3480
   370
 "!!evs. evs : tls ==>                                 \
paulson@3677
   371
\    ALL KK. KK <= range sessionK -->           \
paulson@3683
   372
\            (Nonce N : analz (Key``KK Un (spies evs))) = \
paulson@3683
   373
\            (Nonce N : analz (spies evs))";
paulson@3480
   374
by (etac tls.induct 1);
paulson@3480
   375
by (ClientCertKeyEx_tac 6);
paulson@3480
   376
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3515
   377
by (REPEAT_FIRST (rtac lemma));
paulson@3677
   378
writeln"SLOW simplification: 55 secs??";
paulson@3683
   379
(*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
paulson@3515
   380
by (ALLGOALS
paulson@3515
   381
    (asm_simp_tac (analz_image_keys_ss 
paulson@3677
   382
		   addsimps [range_sessionkeys_not_priK, 
paulson@3677
   383
			     analz_image_priK, analz_insert_certificate])));
paulson@3515
   384
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
paulson@3480
   385
(*Fake*) 
paulson@3480
   386
by (spy_analz_tac 2);
paulson@3480
   387
(*Base*)
paulson@3480
   388
by (Blast_tac 1);
paulson@3480
   389
qed_spec_mp "analz_image_keys";
paulson@3480
   390
paulson@3687
   391
(*Knowing some session keys is no help in getting new nonces*)
paulson@3687
   392
goal thy
paulson@3687
   393
 "!!evs. evs : tls ==>          \
paulson@3687
   394
\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
paulson@3687
   395
\        (Nonce N : analz (spies evs))";
paulson@3687
   396
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
paulson@3687
   397
qed "analz_insert_key";
paulson@3687
   398
Addsimps [analz_insert_key];
paulson@3480
   399
paulson@3672
   400
goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
paulson@3672
   401
by (parts_induct_tac 1);
paulson@3672
   402
(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
paulson@3672
   403
by (Blast_tac 1);
paulson@3672
   404
qed "no_Notes_A_PRF";
paulson@3672
   405
Addsimps [no_Notes_A_PRF];
paulson@3672
   406
paulson@3672
   407
paulson@3683
   408
goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
paulson@3672
   409
\                   evs : tls |]  \
paulson@3683
   410
\                ==> Nonce PMS : parts (spies evs)";
paulson@3672
   411
by (etac rev_mp 1);
paulson@3672
   412
by (parts_induct_tac 1);
paulson@3683
   413
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
paulson@3672
   414
by (Fake_parts_insert_tac 1);
paulson@3677
   415
(*Six others, all trivial or by freshness*)
paulson@3683
   416
by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
paulson@3683
   417
                               addSEs spies_partsEs) 1));
paulson@3672
   418
qed "MS_imp_PMS";
paulson@3672
   419
AddSDs [MS_imp_PMS];
paulson@3672
   420
paulson@3672
   421
paulson@3474
   422
paulson@3474
   423
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
paulson@3474
   424
paulson@3677
   425
(** Some lemmas about session keys, comprising clientK and serverK **)
paulson@3515
   426
paulson@3672
   427
(*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
paulson@3515
   428
  Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
paulson@3515
   429
paulson@3474
   430
goal thy 
paulson@3686
   431
 "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
paulson@3686
   432
\           Nonce M ~: analz (spies evs);  evs : tls |]   \
paulson@3686
   433
\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
paulson@3686
   434
by (etac rev_mp 1);
paulson@3480
   435
by (etac rev_mp 1);
paulson@3686
   436
by (analz_induct_tac 1);	(*30 seconds??*)
paulson@3686
   437
(*Oops*)
paulson@3686
   438
by (Blast_tac 4);
paulson@3480
   439
(*SpyKeys*)
paulson@3683
   440
by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
paulson@3480
   441
(*Fake*) 
paulson@3480
   442
by (spy_analz_tac 2);
paulson@3480
   443
(*Base*)
paulson@3480
   444
by (Blast_tac 1);
paulson@3677
   445
qed "sessionK_notin_parts";
paulson@3677
   446
bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE));
paulson@3515
   447
paulson@3677
   448
Addsimps [sessionK_notin_parts];
paulson@3677
   449
AddSEs [sessionK_in_partsE, 
paulson@3677
   450
	impOfSubs analz_subset_parts RS sessionK_in_partsE];
paulson@3515
   451
paulson@3672
   452
paulson@3677
   453
(*Lemma: session keys are never used if PMS is fresh.  
paulson@3672
   454
  Nonces don't have to agree, allowing session resumption.
paulson@3672
   455
  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
paulson@3672
   456
  They are NOT suitable as safe elim rules.*)
paulson@3515
   457
paulson@3515
   458
goal thy 
paulson@3686
   459
 "!!evs. [| ALL A. Says A Spy (Key (sessionK((Na, Nb, PRF(PMS,NA,NB)),b))) \
paulson@3686
   460
\                    ~: set evs; \
paulson@3686
   461
\           Nonce PMS ~: parts (spies evs);  evs : tls |]             \
paulson@3686
   462
\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
paulson@3686
   463
by (etac rev_mp 1);
paulson@3515
   464
by (etac rev_mp 1);
paulson@3515
   465
by (analz_induct_tac 1);
paulson@3677
   466
(*Fake*)
paulson@3686
   467
by (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]) 2);
paulson@3515
   468
by (Fake_parts_insert_tac 2);
paulson@3685
   469
(*Base, ClientFinished, ServerFinished, ClientResume: 
paulson@3685
   470
  trivial, e.g. by freshness*)
paulson@3677
   471
by (REPEAT 
paulson@3685
   472
    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
paulson@3685
   473
				Notes_master_imp_Crypt_PMS]
paulson@3683
   474
                        addSEs spies_partsEs) 1));
paulson@3677
   475
qed "Crypt_sessionK_notin_parts";
paulson@3686
   476
paulson@3677
   477
Addsimps [Crypt_sessionK_notin_parts];
paulson@3677
   478
AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
paulson@3515
   479
paulson@3515
   480
paulson@3519
   481
(*NEEDED??*)
paulson@3515
   482
goal thy
paulson@3515
   483
 "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
paulson@3519
   484
\           A ~= Spy;  evs : tls |] ==> KB = pubK B";
paulson@3515
   485
be rev_mp 1;
paulson@3515
   486
by (analz_induct_tac 1);
paulson@3515
   487
qed "A_Crypt_pubB";
paulson@3515
   488
paulson@3515
   489
paulson@3672
   490
(*** Unicity results for PMS, the pre-master-secret ***)
paulson@3515
   491
paulson@3672
   492
(*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
paulson@3515
   493
goal thy 
paulson@3683
   494
 "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
paulson@3515
   495
\        ==> EX B'. ALL B.   \
paulson@3683
   496
\              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
paulson@3515
   497
by (etac rev_mp 1);
paulson@3519
   498
by (parts_induct_tac 1);
paulson@3519
   499
by (Fake_parts_insert_tac 1);
paulson@3515
   500
(*ClientCertKeyEx*)
paulson@3519
   501
by (ClientCertKeyEx_tac 1);
paulson@3519
   502
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
paulson@3672
   503
by (expand_case_tac "PMS = ?y" 1 THEN
paulson@3519
   504
    blast_tac (!claset addSEs partsEs) 1);
paulson@3515
   505
val lemma = result();
paulson@3515
   506
paulson@3515
   507
goal thy 
paulson@3683
   508
 "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
paulson@3683
   509
\           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
paulson@3683
   510
\           Nonce PMS ~: analz (spies evs);                 \
paulson@3515
   511
\           evs : tls |]                                          \
paulson@3515
   512
\        ==> B=B'";
paulson@3515
   513
by (prove_unique_tac lemma 1);
paulson@3672
   514
qed "unique_PMS";
paulson@3515
   515
paulson@3685
   516
(** It is frustrating that we need two versions of the unicity results.
paulson@3685
   517
    But Notes A {|Agent B, Nonce PMS|} determines both A and B, while
paulson@3685
   518
    Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only
paulson@3685
   519
    this weaker item is available.
paulson@3685
   520
**)
paulson@3515
   521
paulson@3677
   522
(*In A's internal Note, PMS determines A and B.*)
paulson@3515
   523
goal thy 
paulson@3683
   524
 "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]            \
paulson@3515
   525
\ ==> EX A' B'. ALL A B.                                                   \
paulson@3672
   526
\        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
paulson@3515
   527
by (etac rev_mp 1);
paulson@3519
   528
by (parts_induct_tac 1);
paulson@3515
   529
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
paulson@3672
   530
(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
paulson@3672
   531
by (expand_case_tac "PMS = ?y" 1 THEN
paulson@3683
   532
    blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
paulson@3515
   533
val lemma = result();
paulson@3515
   534
paulson@3515
   535
goal thy 
paulson@3672
   536
 "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
paulson@3672
   537
\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
paulson@3683
   538
\           Nonce PMS ~: analz (spies evs);      \
paulson@3515
   539
\           evs : tls |]                               \
paulson@3515
   540
\        ==> A=A' & B=B'";
paulson@3515
   541
by (prove_unique_tac lemma 1);
paulson@3672
   542
qed "Notes_unique_PMS";
paulson@3515
   543
paulson@3515
   544
paulson@3474
   545
paulson@3677
   546
(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
paulson@3677
   547
goal thy
paulson@3683
   548
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
paulson@3677
   549
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
paulson@3683
   550
\            Nonce PMS ~: analz (spies evs)";
paulson@3685
   551
by (analz_induct_tac 1);   (*30 seconds??*)
paulson@3677
   552
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
paulson@3686
   553
by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
paulson@3687
   554
(*ClientHello, ServerHello, ClientCertKeyEx, ServerResume: 
paulson@3687
   555
  mostly freshness reasoning*)
paulson@3677
   556
by (REPEAT (blast_tac (!claset addSEs partsEs
paulson@3683
   557
			       addDs  [Notes_Crypt_parts_spies,
paulson@3677
   558
				       impOfSubs analz_subset_parts,
paulson@3687
   559
				       Says_imp_spies RS analz.Inj]) 3));
paulson@3677
   560
(*SpyKeys*)
paulson@3677
   561
by (fast_tac (!claset addss (!simpset)) 2);
paulson@3677
   562
(*Fake*)
paulson@3677
   563
by (spy_analz_tac 1);
paulson@3677
   564
bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
paulson@3677
   565
paulson@3677
   566
paulson@3685
   567
(*Another way of showing unicity*)
paulson@3685
   568
goal thy 
paulson@3685
   569
 "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
paulson@3685
   570
\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
paulson@3685
   571
\           A ~: bad;  B ~: bad;                         \
paulson@3685
   572
\           evs : tls |]                                 \
paulson@3685
   573
\        ==> A=A' & B=B'";
paulson@3685
   574
by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1));
paulson@3685
   575
qed "good_Notes_unique_PMS";
paulson@3677
   576
paulson@3677
   577
paulson@3677
   578
(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
paulson@3677
   579
  will stay secret.*)
paulson@3677
   580
goal thy
paulson@3683
   581
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
paulson@3677
   582
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
paulson@3683
   583
\            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
paulson@3677
   584
by (analz_induct_tac 1);   (*35 seconds*)
paulson@3677
   585
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
paulson@3677
   586
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
paulson@3683
   587
				      Says_imp_spies RS analz.Inj,
paulson@3683
   588
				      Notes_imp_spies RS analz.Inj]) 6));
paulson@3677
   589
(*ClientHello*)
paulson@3677
   590
by (Blast_tac 3);
paulson@3677
   591
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
paulson@3677
   592
by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
paulson@3683
   593
			       Says_imp_spies RS analz.Inj]) 2);
paulson@3677
   594
(*Fake*)
paulson@3677
   595
by (spy_analz_tac 1);
paulson@3677
   596
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
paulson@3677
   597
by (REPEAT (blast_tac (!claset addSEs partsEs
paulson@3683
   598
			       addDs  [Notes_Crypt_parts_spies,
paulson@3677
   599
				       impOfSubs analz_subset_parts,
paulson@3683
   600
				       Says_imp_spies RS analz.Inj]) 1));
paulson@3677
   601
bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
paulson@3677
   602
paulson@3677
   603
paulson@3685
   604
(*** Protocol goals: if A receives ServerFinished, then B is present 
paulson@3474
   605
     and has used the quoted values XA, XB, etc.  Note that it is up to A
paulson@3474
   606
     to compare XA with what she originally sent.
paulson@3474
   607
***)
paulson@3474
   608
paulson@3685
   609
(*The mention of her name (A) in X assures A that B knows who she is.*)
paulson@3515
   610
goal thy
paulson@3686
   611
 "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
paulson@3686
   612
\           X = Crypt (serverK(Na,Nb,M))                  \
paulson@3676
   613
\                 (Hash{|Nonce M, Number SID,             \
paulson@3676
   614
\                        Nonce NA, Number XA, Agent A,    \
paulson@3672
   615
\                        Nonce NB, Number XB, Agent B|}); \
paulson@3676
   616
\           M = PRF(PMS,NA,NB);                           \
paulson@3683
   617
\           evs : tls;  A ~: bad;  B ~: bad |]          \
paulson@3676
   618
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
paulson@3683
   619
\        X : parts (spies evs) --> Says B A X : set evs";
paulson@3686
   620
by (etac rev_mp 1);
paulson@3480
   621
by (hyp_subst_tac 1);
paulson@3677
   622
by (analz_induct_tac 1);	(*16 seconds*)
paulson@3685
   623
(*ServerResume is trivial, but Blast_tac is too slow*)
paulson@3685
   624
by (Best_tac 3);
paulson@3677
   625
(*ClientCertKeyEx*)
paulson@3677
   626
by (Blast_tac 2);
paulson@3480
   627
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3480
   628
by (REPEAT (rtac impI 1));
paulson@3683
   629
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
paulson@3672
   630
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
paulson@3480
   631
				     not_parts_not_analz]) 2);
paulson@3474
   632
by (Fake_parts_insert_tac 1);
paulson@3474
   633
qed_spec_mp "TrustServerFinished";
paulson@3474
   634
paulson@3474
   635
paulson@3685
   636
(*This version refers not to ServerFinished but to any message from B.
paulson@3685
   637
  We don't assume B has received CertVerify, and an intruder could
paulson@3515
   638
  have changed A's identity in all other messages, so we can't be sure
paulson@3519
   639
  that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
paulson@3672
   640
  to bind A's identity with M, then we could replace A' by A below.*)
paulson@3515
   641
goal thy
paulson@3686
   642
 "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
paulson@3686
   643
\           evs : tls;  A ~: bad;  B ~: bad;                 \
paulson@3672
   644
\           M = PRF(PMS,NA,NB) |]            \
paulson@3672
   645
\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
paulson@3683
   646
\            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
paulson@3672
   647
\            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
paulson@3686
   648
by (etac rev_mp 1);
paulson@3672
   649
by (hyp_subst_tac 1);
paulson@3686
   650
by (analz_induct_tac 1);	(*20 seconds*)
paulson@3515
   651
by (REPEAT_FIRST (rtac impI));
paulson@3685
   652
(*ServerResume, by unicity of PMS*)
paulson@3685
   653
by (blast_tac (!claset addSEs [MPair_parts]
paulson@3685
   654
		       addDs  [Spy_not_see_PMS, 
paulson@3685
   655
			       Notes_Crypt_parts_spies,
paulson@3685
   656
			       Notes_master_imp_Crypt_PMS, unique_PMS]) 4);
paulson@3685
   657
(*ServerFinished, by unicity of PMS (10 seconds)*)
paulson@3685
   658
by (blast_tac (!claset addSEs [MPair_parts]
paulson@3685
   659
		       addDs  [Spy_not_see_PMS, 
paulson@3685
   660
			       Notes_Crypt_parts_spies,
paulson@3685
   661
			       Says_imp_spies RS parts.Inj,
paulson@3685
   662
			       unique_PMS]) 3);
paulson@3677
   663
(*ClientCertKeyEx*)
paulson@3677
   664
by (Blast_tac 2);
paulson@3515
   665
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3683
   666
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
paulson@3672
   667
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
paulson@3515
   668
				     not_parts_not_analz]) 2);
paulson@3515
   669
by (Fake_parts_insert_tac 1);
paulson@3515
   670
qed_spec_mp "TrustServerMsg";
paulson@3515
   671
paulson@3515
   672
paulson@3515
   673
(*** Protocol goal: if B receives any message encrypted with clientK
paulson@3672
   674
     then A has sent it, ASSUMING that A chose PMS.  Authentication is
paulson@3515
   675
     assumed here; B cannot verify it.  But if the message is
paulson@3685
   676
     ClientFinished, then B can then check the quoted values XA, XB, etc.
paulson@3506
   677
***)
paulson@3515
   678
goal thy
paulson@3683
   679
 "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
paulson@3686
   680
\  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
paulson@3686
   681
\      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
paulson@3683
   682
\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
paulson@3672
   683
\      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
paulson@3686
   684
by (analz_induct_tac 1);	(*23 seconds*)
paulson@3515
   685
by (REPEAT_FIRST (rtac impI));
paulson@3686
   686
(*ClientResume: by unicity of PMS*)
paulson@3686
   687
by (blast_tac (!claset delrules [conjI]
paulson@3686
   688
		       addSEs [MPair_parts]
paulson@3686
   689
                       addSDs [Notes_master_imp_Notes_PMS]
paulson@3686
   690
	 	       addDs  [good_Notes_unique_PMS]) 4);
paulson@3686
   691
(*ClientFinished: by unicity of PMS*)
paulson@3686
   692
by (blast_tac (!claset delrules [conjI]
paulson@3686
   693
		       addSEs [MPair_parts]
paulson@3686
   694
		       addDs  [good_Notes_unique_PMS]) 3);
paulson@3677
   695
(*ClientCertKeyEx*)
paulson@3677
   696
by (Blast_tac 2);
paulson@3480
   697
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3683
   698
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
paulson@3672
   699
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
paulson@3480
   700
				     not_parts_not_analz]) 2);
paulson@3474
   701
by (Fake_parts_insert_tac 1);
paulson@3515
   702
qed_spec_mp "TrustClientMsg";
paulson@3506
   703
paulson@3506
   704
paulson@3685
   705
paulson@3685
   706
(*** Protocol goal: if B receives ClientFinished, and if B is able to
paulson@3685
   707
     check a CertVerify from A, then A has used the quoted
paulson@3506
   708
     values XA, XB, etc.  Even this one requires A to be uncompromised.
paulson@3506
   709
 ***)
paulson@3506
   710
goal thy
paulson@3686
   711
 "!!evs. [| ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
paulson@3686
   712
\           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
paulson@3676
   713
\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
paulson@3515
   714
\             : set evs;                                                  \
paulson@3515
   715
\           Says A'' B (Crypt (priK A)                                    \
paulson@3672
   716
\                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
paulson@3515
   717
\             : set evs;                                                  \
paulson@3683
   718
\        evs : tls;  A ~: bad;  B ~: bad |]                             \
paulson@3672
   719
\     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
paulson@3515
   720
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
paulson@3683
   721
                       addDs  [Says_imp_spies RS parts.Inj]) 1);
paulson@3515
   722
qed "AuthClientFinished";
paulson@3687
   723
paulson@3687
   724
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)