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