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