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