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