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