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