src/HOL/Auth/TLS.ML
author paulson
Tue Jul 01 17:37:42 1997 +0200 (1997-07-01)
changeset 3480 d59bbf053258
parent 3474 44249bba00ec
child 3500 0d8ad2f192d8
permissions -rw-r--r--
More realistic model: the Spy can compute clientK and serverK
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@3474
     6
The public-key model has a weakness, especially concerning anonymous sessions.
paulson@3480
     7
The Spy's state is recorded as the trace of message.  But if he himself is the
paulson@3480
     8
Client and invents M, then he sends contains M encrypted with B's public key.
paulson@3480
     9
This message gives no evidence that the spy knows M, and yet the spy actually
paulson@3480
    10
chose M!  So, in any property concerning the secrecy of some item, one must
paulson@3480
    11
establish that the spy didn't choose the item.  Guarantees normally assume
paulson@3480
    12
that the other party is uncompromised (otherwise, one can prove little).
paulson@3480
    13
paulson@3480
    14
Protocol goals: 
paulson@3480
    15
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
paulson@3480
    16
     parties (though A is not necessarily authenticated).
paulson@3480
    17
paulson@3480
    18
* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
paulson@3480
    19
    message is optional!)
paulson@3474
    20
paulson@3480
    21
* A upon receiving SERVER FINISHED knows that B is present
paulson@3480
    22
paulson@3480
    23
* Each party who has received a FINISHED message can trust that the other
paulson@3480
    24
  party agrees on all message components, including XA and XB (thus foiling
paulson@3480
    25
  rollback attacks).
paulson@3480
    26
paulson@3480
    27
A curious property found in these proofs is that CERTIFICATE VERIFY actually
paulson@3480
    28
gives weaker authentication than CLIENT FINISHED.  The theorem for CERTIFICATE
paulson@3480
    29
VERIFY is subject to A~:lost, since if A's private key is known to the spy
paulson@3480
    30
then he can forge A's signature.  But the theorem for CLIENT FINISHED merely
paulson@3480
    31
assumes that A is not the spy himself, since the model assumes that all other
paulson@3480
    32
agents tell the truth.
paulson@3480
    33
paulson@3480
    34
In the real world, there are agents who are not active attackers, and yet
paulson@3480
    35
still cannot be trusted to identify themselves.  There may well be more such
paulson@3480
    36
agents than there are compromised private keys.
paulson@3474
    37
*)
paulson@3474
    38
paulson@3474
    39
open TLS;
paulson@3474
    40
paulson@3474
    41
proof_timing:=true;
paulson@3474
    42
HOL_quantifiers := false;
paulson@3474
    43
paulson@3474
    44
AddIffs [Spy_in_lost, Server_not_lost];
paulson@3474
    45
paulson@3480
    46
goal thy "!!A. A ~: lost ==> A ~= Spy";
paulson@3480
    47
by (Blast_tac 1);
paulson@3480
    48
qed "not_lost_not_eq_Spy";
paulson@3480
    49
Addsimps [not_lost_not_eq_Spy];
paulson@3480
    50
paulson@3474
    51
(*Injectiveness of key-generating functions*)
paulson@3474
    52
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
paulson@3474
    53
paulson@3474
    54
(* invKey(clientK x) = clientK x  and similarly for serverK*)
paulson@3474
    55
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
paulson@3474
    56
	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
paulson@3480
    57
paulson@3474
    58
paulson@3474
    59
(*Replacing the variable by a constant improves search speed by 50%!*)
paulson@3474
    60
val Says_imp_sees_Spy' = 
paulson@3474
    61
    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
paulson@3474
    62
paulson@3474
    63
paulson@3474
    64
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
paulson@3474
    65
paulson@3474
    66
goal thy "pubK A ~= clientK arg";
paulson@3474
    67
br notI 1;
paulson@3474
    68
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    69
by (Full_simp_tac 1);
paulson@3474
    70
qed "pubK_neq_clientK";
paulson@3474
    71
paulson@3474
    72
goal thy "pubK A ~= serverK arg";
paulson@3474
    73
br notI 1;
paulson@3474
    74
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    75
by (Full_simp_tac 1);
paulson@3474
    76
qed "pubK_neq_serverK";
paulson@3474
    77
paulson@3474
    78
goal thy "priK A ~= clientK arg";
paulson@3474
    79
br notI 1;
paulson@3474
    80
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    81
by (Full_simp_tac 1);
paulson@3474
    82
qed "priK_neq_clientK";
paulson@3474
    83
paulson@3474
    84
goal thy "priK A ~= serverK arg";
paulson@3474
    85
br notI 1;
paulson@3474
    86
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    87
by (Full_simp_tac 1);
paulson@3474
    88
qed "priK_neq_serverK";
paulson@3474
    89
paulson@3480
    90
(*clientK and serverK have disjoint ranges*)
paulson@3480
    91
goal thy "clientK arg ~= serverK arg'";
paulson@3480
    92
by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
paulson@3480
    93
by (Blast_tac 1);
paulson@3480
    94
qed "clientK_neq_serverK";
paulson@3480
    95
paulson@3474
    96
val ths = [pubK_neq_clientK, pubK_neq_serverK, 
paulson@3480
    97
	   priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
paulson@3474
    98
AddIffs (ths @ (ths RL [not_sym]));
paulson@3474
    99
paulson@3474
   100
paulson@3474
   101
(**** Protocol Proofs ****)
paulson@3474
   102
paulson@3474
   103
(*A "possibility property": there are traces that reach the end.
paulson@3474
   104
  This protocol has three end points and six messages to consider.*)
paulson@3474
   105
paulson@3474
   106
(*Possibility property ending with ServerFinished.*)
paulson@3474
   107
goal thy 
paulson@3474
   108
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
paulson@3474
   109
\  Says B A (Crypt (serverK(NA,NB,M))                 \
paulson@3474
   110
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
paulson@3474
   111
\                   Nonce NA, Agent XA, Agent A,      \
paulson@3474
   112
\                   Nonce NB, Agent XB,               \
paulson@3474
   113
\                   Crypt (priK Server) {|Agent B, Key (pubK B)|}|})) \
paulson@3474
   114
\    : set evs";
paulson@3474
   115
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   116
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3474
   117
	  RS tls.ServerFinished) 2);
paulson@3474
   118
by possibility_tac;
paulson@3474
   119
result();
paulson@3474
   120
paulson@3474
   121
(*And one for ClientFinished.  Either FINISHED message may come first.*)
paulson@3474
   122
goal thy 
paulson@3474
   123
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
paulson@3474
   124
\  Says A B (Crypt (clientK(NA,NB,M))                 \
paulson@3474
   125
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
paulson@3474
   126
\                   Nonce NA, Agent XA,               \
paulson@3474
   127
\                   Crypt (priK Server) {|Agent A, Key (pubK A)|},      \
paulson@3474
   128
\                   Nonce NB, Agent XB, Agent B|})) : set evs";
paulson@3474
   129
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   130
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3474
   131
	  RS tls.ClientFinished) 2);
paulson@3474
   132
by possibility_tac;
paulson@3474
   133
result();
paulson@3474
   134
paulson@3474
   135
(*Another one, for CertVerify (which is optional)*)
paulson@3474
   136
goal thy 
paulson@3474
   137
 "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
paulson@3474
   138
\  Says A B (Crypt (priK A)                 \
paulson@3474
   139
\            (Hash{|Nonce NB,               \
paulson@3474
   140
\                   Crypt (priK Server)     \
paulson@3474
   141
\                         {|Agent B, Key (pubK B)|}|})) : set evs";
paulson@3474
   142
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   143
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
paulson@3474
   144
by possibility_tac;
paulson@3474
   145
result();
paulson@3474
   146
paulson@3474
   147
paulson@3474
   148
(**** Inductive proofs about tls ****)
paulson@3474
   149
paulson@3474
   150
(*Nobody sends themselves messages*)
paulson@3474
   151
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
paulson@3474
   152
by (etac tls.induct 1);
paulson@3474
   153
by (Auto_tac());
paulson@3474
   154
qed_spec_mp "not_Says_to_self";
paulson@3474
   155
Addsimps [not_Says_to_self];
paulson@3474
   156
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@3474
   157
paulson@3474
   158
paulson@3474
   159
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
paulson@3474
   160
    sends messages containing X! **)
paulson@3474
   161
paulson@3474
   162
(*Spy never sees another agent's private key! (unless it's lost at start)*)
paulson@3474
   163
goal thy 
paulson@3474
   164
 "!!evs. evs : tls \
paulson@3474
   165
\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
paulson@3474
   166
by (etac tls.induct 1);
paulson@3474
   167
by (prove_simple_subgoals_tac 1);
paulson@3474
   168
by (Fake_parts_insert_tac 1);
paulson@3474
   169
qed "Spy_see_priK";
paulson@3474
   170
Addsimps [Spy_see_priK];
paulson@3474
   171
paulson@3474
   172
goal thy 
paulson@3474
   173
 "!!evs. evs : tls \
paulson@3474
   174
\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
paulson@3474
   175
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@3474
   176
qed "Spy_analz_priK";
paulson@3474
   177
Addsimps [Spy_analz_priK];
paulson@3474
   178
paulson@3474
   179
goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
paulson@3474
   180
\                  evs : tls |] ==> A:lost";
paulson@3474
   181
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
paulson@3474
   182
qed "Spy_see_priK_D";
paulson@3474
   183
paulson@3474
   184
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
paulson@3474
   185
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
paulson@3474
   186
paulson@3474
   187
paulson@3474
   188
(*Every Nonce that's hashed is already in past traffic. *)
paulson@3474
   189
goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
paulson@3474
   190
\                   evs : tls |]  \
paulson@3474
   191
\                ==> Nonce N : parts (sees lost Spy evs)";
paulson@3474
   192
by (etac rev_mp 1);
paulson@3474
   193
by (etac tls.induct 1);
paulson@3474
   194
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   195
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   196
		      addSEs partsEs) 1);
paulson@3474
   197
by (Fake_parts_insert_tac 1);
paulson@3474
   198
qed "Hash_imp_Nonce1";
paulson@3474
   199
paulson@3474
   200
(*Lemma needed to prove Hash_Hash_imp_Nonce*)
paulson@3474
   201
goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
paulson@3474
   202
\                       : parts (sees lost Spy evs);     \
paulson@3474
   203
\                   evs : tls |]  \
paulson@3474
   204
\                ==> Nonce M : parts (sees lost Spy evs)";
paulson@3474
   205
by (etac rev_mp 1);
paulson@3474
   206
by (etac tls.induct 1);
paulson@3474
   207
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   208
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   209
		      addSEs partsEs) 1);
paulson@3474
   210
by (Fake_parts_insert_tac 1);
paulson@3474
   211
qed "Hash_imp_Nonce2";
paulson@3474
   212
AddSDs [Hash_imp_Nonce2];
paulson@3474
   213
paulson@3474
   214
goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
paulson@3474
   215
\                      : parts (sees lost Spy evs);      \
paulson@3474
   216
\                   evs : tls |]                         \
paulson@3474
   217
\                ==> Nonce M : parts (sees lost Spy evs)";
paulson@3474
   218
by (etac rev_mp 1);
paulson@3474
   219
by (etac tls.induct 1);
paulson@3474
   220
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   221
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   222
		      addSEs partsEs) 1);
paulson@3474
   223
by (Fake_parts_insert_tac 1);
paulson@3474
   224
qed "Hash_Hash_imp_Nonce";
paulson@3474
   225
paulson@3474
   226
paulson@3474
   227
(*NEEDED??
paulson@3474
   228
  Every Nonce that's hashed is already in past traffic. 
paulson@3474
   229
  This general formulation is tricky to prove and hard to use, since the
paulson@3474
   230
  2nd premise is typically proved by simplification.*)
paulson@3474
   231
goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
paulson@3474
   232
\                   Nonce N : parts {X};  evs : tls |]  \
paulson@3474
   233
\                ==> Nonce N : parts (sees lost Spy evs)";
paulson@3474
   234
by (etac rev_mp 1);
paulson@3474
   235
by (etac tls.induct 1);
paulson@3474
   236
by (ALLGOALS Asm_simp_tac);
paulson@3474
   237
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   238
		      addSEs partsEs) 1);
paulson@3474
   239
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   240
(*ServerFinished*)
paulson@3474
   241
by (Blast_tac 3);
paulson@3474
   242
(*ClientFinished*)
paulson@3474
   243
by (Blast_tac 2);
paulson@3474
   244
by (Fake_parts_insert_tac 1);
paulson@3474
   245
qed "Hash_imp_Nonce_seen";
paulson@3474
   246
paulson@3474
   247
paulson@3474
   248
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
paulson@3474
   249
paulson@3474
   250
(*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
paulson@3480
   251
  message is Fake.  We don't need guarantees for the Spy anyway.  We must
paulson@3480
   252
  assume A~:lost; otherwise, the Spy can forge A's signature.*)
paulson@3474
   253
goal thy 
paulson@3474
   254
 "!!evs. [| X = Crypt (priK A)                          \
paulson@3474
   255
\                 (Hash{|Nonce NB,                                      \
paulson@3474
   256
\                        Crypt (priK Server) {|Agent B, Key KB|}|});    \
paulson@3474
   257
\           evs : tls;  A ~: lost;  B ~= Spy |]         \
paulson@3474
   258
\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
paulson@3474
   259
\                   Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
paulson@3474
   260
\        X : parts (sees lost Spy evs) --> Says A B X : set evs";
paulson@3480
   261
by (hyp_subst_tac 1);
paulson@3474
   262
by (etac tls.induct 1);
paulson@3474
   263
by (ALLGOALS Asm_simp_tac);
paulson@3474
   264
by (Fake_parts_insert_tac 1);
paulson@3480
   265
(*ServerHello: nonce NB cannot be in X because it's fresh!*)
paulson@3474
   266
by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
paulson@3474
   267
	               addSEs sees_Spy_partsEs) 1);
paulson@3474
   268
qed_spec_mp "TrustCertVerify";
paulson@3474
   269
paulson@3474
   270
paulson@3474
   271
(*This lemma says that no false certificates exist.  One might extend the
paulson@3474
   272
  model to include bogus certificates for the lost agents, but there seems
paulson@3474
   273
  little point in doing so: the loss of their private keys is a worse
paulson@3474
   274
  breach of security.*)
paulson@3474
   275
goal thy 
paulson@3474
   276
 "!!evs. evs : tls     \
paulson@3474
   277
\    ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \
paulson@3474
   278
\        --> KB = pubK B";
paulson@3474
   279
by (etac tls.induct 1);
paulson@3474
   280
by (ALLGOALS Asm_simp_tac);
paulson@3474
   281
by (Fake_parts_insert_tac 2);
paulson@3474
   282
by (Blast_tac 1);
paulson@3474
   283
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
paulson@3474
   284
paulson@3474
   285
paulson@3474
   286
(*Replace key KB in ClientCertKeyEx by (pubK B) *)
paulson@3474
   287
val ClientCertKeyEx_tac = 
paulson@3474
   288
    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
paulson@3474
   289
		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
paulson@3474
   290
    THEN' assume_tac
paulson@3474
   291
    THEN' hyp_subst_tac;
paulson@3474
   292
paulson@3474
   293
fun analz_induct_tac i = 
paulson@3474
   294
    etac tls.induct i   THEN
paulson@3480
   295
    ClientCertKeyEx_tac  (i+5)  THEN
paulson@3474
   296
    ALLGOALS (asm_simp_tac 
paulson@3474
   297
              (!simpset addsimps [not_parts_not_analz]
paulson@3474
   298
                        setloop split_tac [expand_if]))  THEN
paulson@3474
   299
    (*Remove instances of pubK B:  the Spy already knows all public keys.
paulson@3474
   300
      Combining the two simplifier calls makes them run extremely slowly.*)
paulson@3474
   301
    ALLGOALS (asm_simp_tac 
paulson@3474
   302
              (!simpset addsimps [insert_absorb]
paulson@3474
   303
                        setloop split_tac [expand_if]));
paulson@3474
   304
paulson@3480
   305
(*** Specialized rewriting for the analz_image_... theorems ***)
paulson@3480
   306
paulson@3480
   307
goal thy "insert (Key K) H = Key `` {K} Un H";
paulson@3480
   308
by (Blast_tac 1);
paulson@3480
   309
qed "insert_Key_singleton";
paulson@3480
   310
paulson@3480
   311
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
paulson@3480
   312
by (Blast_tac 1);
paulson@3480
   313
qed "insert_Key_image";
paulson@3480
   314
paulson@3480
   315
(*Reverse the normal simplification of "image" to build up (not break down)
paulson@3480
   316
  the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
paulson@3480
   317
val analz_image_keys_ss = 
paulson@3480
   318
     !simpset delsimps [image_insert, image_Un]
paulson@3480
   319
              addsimps [image_insert RS sym, image_Un RS sym,
paulson@3480
   320
			rangeI, 
paulson@3480
   321
			insert_Key_singleton, 
paulson@3480
   322
			insert_Key_image, Un_assoc RS sym]
paulson@3480
   323
              setloop split_tac [expand_if];
paulson@3480
   324
paulson@3480
   325
(*No collection of keys can help the spy get new private keys*)
paulson@3480
   326
goal thy  
paulson@3480
   327
 "!!evs. evs : tls ==>                                    \
paulson@3480
   328
\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
paulson@3480
   329
\            (priK B : KK | B : lost)";
paulson@3480
   330
by (etac tls.induct 1);
paulson@3480
   331
by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
paulson@3480
   332
(*Fake*) 
paulson@3480
   333
by (spy_analz_tac 2);
paulson@3480
   334
(*Base*)
paulson@3480
   335
by (Blast_tac 1);
paulson@3480
   336
qed_spec_mp "analz_image_priK";
paulson@3480
   337
paulson@3480
   338
paulson@3480
   339
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@3480
   340
goal thy  
paulson@3480
   341
 "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
paulson@3480
   342
\        (X : analz (G Un H))  =  (X : analz H)";
paulson@3480
   343
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
paulson@3480
   344
val lemma = result();
paulson@3480
   345
paulson@3480
   346
(*Knowing some clientKs and serverKs is no help in getting new nonces*)
paulson@3480
   347
goal thy  
paulson@3480
   348
 "!!evs. evs : tls ==>                                 \
paulson@3480
   349
\    ALL KK. KK <= (range clientK Un range serverK) -->           \
paulson@3480
   350
\            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
paulson@3480
   351
\            (Nonce N : analz (sees lost Spy evs))";
paulson@3480
   352
by (etac tls.induct 1);
paulson@3480
   353
by (ClientCertKeyEx_tac 6);
paulson@3480
   354
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3480
   355
by (REPEAT_FIRST (rtac lemma ));
paulson@3480
   356
	(*SLOW: 30s!*)
paulson@3480
   357
by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
paulson@3480
   358
by (ALLGOALS (asm_simp_tac
paulson@3480
   359
	      (!simpset addsimps [analz_image_priK, insert_absorb])));
paulson@3480
   360
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
paulson@3480
   361
by (Blast_tac 3);
paulson@3480
   362
(*Fake*) 
paulson@3480
   363
by (spy_analz_tac 2);
paulson@3480
   364
(*Base*)
paulson@3480
   365
by (Blast_tac 1);
paulson@3480
   366
qed_spec_mp "analz_image_keys";
paulson@3480
   367
paulson@3480
   368
paulson@3480
   369
(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.
paulson@3480
   370
  The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
paulson@3480
   371
  here.*)
paulson@3474
   372
goal thy 
paulson@3480
   373
 "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                       \
paulson@3480
   374
\        ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
paulson@3480
   375
\                       Crypt KB (Nonce M)|} : set evs -->             \
paulson@3480
   376
\            Nonce M ~: analz (sees lost Spy evs)";
paulson@3474
   377
by (analz_induct_tac 1);
paulson@3474
   378
(*ClientHello*)
paulson@3480
   379
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
paulson@3480
   380
(*SpyKeys*)
paulson@3480
   381
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
paulson@3474
   382
(*Fake*)
paulson@3474
   383
by (spy_analz_tac 1);
paulson@3474
   384
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
paulson@3474
   385
by (REPEAT (blast_tac (!claset addSEs partsEs
paulson@3474
   386
			       addDs  [impOfSubs analz_subset_parts,
paulson@3474
   387
				       Says_imp_sees_Spy' RS analz.Inj]) 1));
paulson@3474
   388
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
paulson@3474
   389
paulson@3474
   390
paulson@3474
   391
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
paulson@3474
   392
paulson@3480
   393
(*The two proofs are identical*)
paulson@3474
   394
goal thy 
paulson@3480
   395
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
paulson@3480
   396
\           evs : tls |]                           \
paulson@3480
   397
\        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
paulson@3480
   398
by (etac rev_mp 1);
paulson@3480
   399
by (analz_induct_tac 1);
paulson@3480
   400
(*SpyKeys*)
paulson@3480
   401
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
paulson@3480
   402
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
paulson@3480
   403
(*Fake*) 
paulson@3480
   404
by (spy_analz_tac 2);
paulson@3480
   405
(*Base*)
paulson@3480
   406
by (Blast_tac 1);
paulson@3474
   407
qed "clientK_notin_parts";
paulson@3474
   408
paulson@3474
   409
goal thy 
paulson@3480
   410
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
paulson@3480
   411
\           evs : tls |]                           \
paulson@3480
   412
\        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
paulson@3480
   413
by (etac rev_mp 1);
paulson@3480
   414
by (analz_induct_tac 1);
paulson@3480
   415
(*SpyKeys*)
paulson@3480
   416
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
paulson@3480
   417
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
paulson@3480
   418
(*Fake*) 
paulson@3480
   419
by (spy_analz_tac 2);
paulson@3480
   420
(*Base*)
paulson@3480
   421
by (Blast_tac 1);
paulson@3474
   422
qed "serverK_notin_parts";
paulson@3474
   423
paulson@3474
   424
paulson@3474
   425
(*** Protocol goals: if A receives SERVER FINISHED, then B is present 
paulson@3474
   426
     and has used the quoted values XA, XB, etc.  Note that it is up to A
paulson@3474
   427
     to compare XA with what she originally sent.
paulson@3474
   428
***)
paulson@3474
   429
paulson@3474
   430
goal thy 
paulson@3480
   431
 "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
paulson@3480
   432
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
paulson@3480
   433
\                        Nonce NA, Agent XA, Agent A,               \
paulson@3480
   434
\                        Nonce NB, Agent XB,                        \
paulson@3474
   435
\                        Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
paulson@3480
   436
\           evs : tls;  A~=Spy;  B ~: lost |]                       \
paulson@3480
   437
\    ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
paulson@3480
   438
\                   Crypt KB (Nonce M)|} : set evs -->              \
paulson@3480
   439
\        X : parts (sees lost Spy evs) --> Says B A X : set evs";
paulson@3480
   440
by (hyp_subst_tac 1);
paulson@3474
   441
by (etac tls.induct 1);
paulson@3474
   442
by (ALLGOALS Asm_simp_tac);
paulson@3480
   443
(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
paulson@3480
   444
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
paulson@3480
   445
                       addSEs sees_Spy_partsEs) 2);
paulson@3480
   446
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3480
   447
by (REPEAT (rtac impI 1));
paulson@3480
   448
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
paulson@3480
   449
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
paulson@3480
   450
				     serverK_notin_parts, 
paulson@3480
   451
				     not_parts_not_analz]) 2);
paulson@3474
   452
by (Fake_parts_insert_tac 1);
paulson@3474
   453
qed_spec_mp "TrustServerFinished";
paulson@3474
   454
paulson@3474
   455
paulson@3480
   456
(*** Protocol goal: if B receives CLIENT FINISHED, then A  is present
paulson@3474
   457
     and has used the quoted values XA, XB, etc.  Note that it is up to B
paulson@3474
   458
     to compare XB with what he originally sent. ***)
paulson@3474
   459
paulson@3480
   460
(*This result seems too strong: A need not have sent CERTIFICATE VERIFY.  
paulson@3480
   461
  But we assume (as always) that the other party is honest...*)
paulson@3474
   462
goal thy 
paulson@3474
   463
 "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
paulson@3474
   464
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
paulson@3474
   465
\                        Nonce NA, Agent XA,                    \
paulson@3474
   466
\                        Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
paulson@3474
   467
\                        Nonce NB, Agent XB, Agent B|});        \
paulson@3480
   468
\           evs : tls;  A~=Spy;  B ~: lost |]                   \
paulson@3480
   469
\     ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
paulson@3480
   470
\                    Crypt KB (Nonce M)|} : set evs -->              \
paulson@3480
   471
\         X : parts (sees lost Spy evs) --> Says A B X : set evs";
paulson@3480
   472
by (hyp_subst_tac 1);
paulson@3474
   473
by (etac tls.induct 1);
paulson@3474
   474
by (ALLGOALS Asm_simp_tac);
paulson@3480
   475
(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
paulson@3480
   476
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
paulson@3480
   477
                       addSEs sees_Spy_partsEs) 2);
paulson@3480
   478
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3480
   479
by (REPEAT (rtac impI 1));
paulson@3480
   480
by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
paulson@3480
   481
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
paulson@3480
   482
				     clientK_notin_parts, 
paulson@3480
   483
				     not_parts_not_analz]) 2);
paulson@3474
   484
by (Fake_parts_insert_tac 1);
paulson@3474
   485
qed_spec_mp "TrustClientFinished";