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