src/HOL/Auth/TLS.ML
author paulson
Fri Jul 11 13:30:01 1997 +0200 (1997-07-11)
changeset 3515 d8a71f6eaf40
parent 3506 a36e0a49d2cd
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Now uses the Notes constructor to distinguish the Client (who has chosen M)
from the Spy (who may have replayed her messages)
paulson@3474
     1
(*  Title:      HOL/Auth/TLS
paulson@3474
     2
    ID:         $Id$
paulson@3474
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3474
     4
    Copyright   1997  University of Cambridge
paulson@3474
     5
paulson@3480
     6
Protocol goals: 
paulson@3480
     7
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
paulson@3480
     8
     parties (though A is not necessarily authenticated).
paulson@3480
     9
paulson@3480
    10
* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
paulson@3480
    11
    message is optional!)
paulson@3474
    12
paulson@3480
    13
* A upon receiving SERVER FINISHED knows that B is present
paulson@3480
    14
paulson@3480
    15
* Each party who has received a FINISHED message can trust that the other
paulson@3480
    16
  party agrees on all message components, including XA and XB (thus foiling
paulson@3480
    17
  rollback attacks).
paulson@3474
    18
*)
paulson@3474
    19
paulson@3474
    20
open TLS;
paulson@3474
    21
paulson@3474
    22
proof_timing:=true;
paulson@3474
    23
HOL_quantifiers := false;
paulson@3474
    24
paulson@3474
    25
AddIffs [Spy_in_lost, Server_not_lost];
paulson@3500
    26
Addsimps [certificate_def];
paulson@3474
    27
paulson@3480
    28
goal thy "!!A. A ~: lost ==> A ~= Spy";
paulson@3480
    29
by (Blast_tac 1);
paulson@3480
    30
qed "not_lost_not_eq_Spy";
paulson@3480
    31
Addsimps [not_lost_not_eq_Spy];
paulson@3480
    32
paulson@3474
    33
(*Injectiveness of key-generating functions*)
paulson@3474
    34
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
paulson@3474
    35
paulson@3474
    36
(* invKey(clientK x) = clientK x  and similarly for serverK*)
paulson@3474
    37
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
paulson@3474
    38
	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
paulson@3480
    39
paulson@3474
    40
paulson@3474
    41
(*Replacing the variable by a constant improves search speed by 50%!*)
paulson@3474
    42
val Says_imp_sees_Spy' = 
paulson@3474
    43
    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
paulson@3474
    44
paulson@3474
    45
paulson@3474
    46
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
paulson@3474
    47
paulson@3474
    48
goal thy "pubK A ~= clientK arg";
paulson@3474
    49
br notI 1;
paulson@3474
    50
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    51
by (Full_simp_tac 1);
paulson@3474
    52
qed "pubK_neq_clientK";
paulson@3474
    53
paulson@3474
    54
goal thy "pubK A ~= serverK arg";
paulson@3474
    55
br notI 1;
paulson@3474
    56
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    57
by (Full_simp_tac 1);
paulson@3474
    58
qed "pubK_neq_serverK";
paulson@3474
    59
paulson@3474
    60
goal thy "priK A ~= clientK arg";
paulson@3474
    61
br notI 1;
paulson@3474
    62
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    63
by (Full_simp_tac 1);
paulson@3474
    64
qed "priK_neq_clientK";
paulson@3474
    65
paulson@3474
    66
goal thy "priK A ~= serverK 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 "priK_neq_serverK";
paulson@3474
    71
paulson@3480
    72
(*clientK and serverK have disjoint ranges*)
paulson@3480
    73
goal thy "clientK arg ~= serverK arg'";
paulson@3480
    74
by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
paulson@3480
    75
by (Blast_tac 1);
paulson@3480
    76
qed "clientK_neq_serverK";
paulson@3480
    77
paulson@3515
    78
val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, 
paulson@3515
    79
		     priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
paulson@3515
    80
AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
paulson@3474
    81
paulson@3474
    82
paulson@3474
    83
(**** Protocol Proofs ****)
paulson@3474
    84
paulson@3474
    85
(*A "possibility property": there are traces that reach the end.
paulson@3474
    86
  This protocol has three end points and six messages to consider.*)
paulson@3474
    87
paulson@3474
    88
(*Possibility property ending with ServerFinished.*)
paulson@3474
    89
goal thy 
paulson@3474
    90
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
paulson@3474
    91
\  Says B A (Crypt (serverK(NA,NB,M))                 \
paulson@3474
    92
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
paulson@3474
    93
\                   Nonce NA, Agent XA, Agent A,      \
paulson@3474
    94
\                   Nonce NB, Agent XB,               \
paulson@3500
    95
\                   certificate B (pubK B)|})) \
paulson@3474
    96
\    : set evs";
paulson@3474
    97
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
    98
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3474
    99
	  RS tls.ServerFinished) 2);
paulson@3474
   100
by possibility_tac;
paulson@3474
   101
result();
paulson@3474
   102
paulson@3474
   103
(*And one for ClientFinished.  Either FINISHED message may come first.*)
paulson@3474
   104
goal thy 
paulson@3474
   105
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
paulson@3474
   106
\  Says A B (Crypt (clientK(NA,NB,M))                 \
paulson@3474
   107
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
paulson@3474
   108
\                   Nonce NA, Agent XA,               \
paulson@3500
   109
\                   certificate A (pubK A),      \
paulson@3474
   110
\                   Nonce NB, Agent XB, Agent B|})) : set evs";
paulson@3474
   111
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   112
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3474
   113
	  RS tls.ClientFinished) 2);
paulson@3474
   114
by possibility_tac;
paulson@3474
   115
result();
paulson@3474
   116
paulson@3474
   117
(*Another one, for CertVerify (which is optional)*)
paulson@3474
   118
goal thy 
paulson@3506
   119
 "!!A B. A ~= B ==> EX NB M. EX evs: tls.     \
paulson@3474
   120
\  Says A B (Crypt (priK A)                 \
paulson@3506
   121
\            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
paulson@3474
   122
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3506
   123
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3506
   124
	  RS tls.CertVerify) 2);
paulson@3474
   125
by possibility_tac;
paulson@3474
   126
result();
paulson@3474
   127
paulson@3474
   128
paulson@3474
   129
(**** Inductive proofs about tls ****)
paulson@3474
   130
paulson@3474
   131
(*Nobody sends themselves messages*)
paulson@3474
   132
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
paulson@3474
   133
by (etac tls.induct 1);
paulson@3474
   134
by (Auto_tac());
paulson@3474
   135
qed_spec_mp "not_Says_to_self";
paulson@3474
   136
Addsimps [not_Says_to_self];
paulson@3474
   137
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@3474
   138
paulson@3474
   139
paulson@3474
   140
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
paulson@3474
   141
    sends messages containing X! **)
paulson@3474
   142
paulson@3474
   143
(*Spy never sees another agent's private key! (unless it's lost at start)*)
paulson@3474
   144
goal thy 
paulson@3474
   145
 "!!evs. evs : tls \
paulson@3474
   146
\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
paulson@3474
   147
by (etac tls.induct 1);
paulson@3474
   148
by (prove_simple_subgoals_tac 1);
paulson@3515
   149
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2);
paulson@3474
   150
by (Fake_parts_insert_tac 1);
paulson@3474
   151
qed "Spy_see_priK";
paulson@3474
   152
Addsimps [Spy_see_priK];
paulson@3474
   153
paulson@3474
   154
goal thy 
paulson@3474
   155
 "!!evs. evs : tls \
paulson@3474
   156
\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
paulson@3474
   157
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@3474
   158
qed "Spy_analz_priK";
paulson@3474
   159
Addsimps [Spy_analz_priK];
paulson@3474
   160
paulson@3474
   161
goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
paulson@3474
   162
\                  evs : tls |] ==> A:lost";
paulson@3474
   163
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
paulson@3474
   164
qed "Spy_see_priK_D";
paulson@3474
   165
paulson@3474
   166
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
paulson@3474
   167
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
paulson@3474
   168
paulson@3474
   169
paulson@3515
   170
(*This lemma says that no false certificates exist.  One might extend the
paulson@3515
   171
  model to include bogus certificates for the lost agents, but there seems
paulson@3515
   172
  little point in doing so: the loss of their private keys is a worse
paulson@3515
   173
  breach of security.*)
paulson@3515
   174
goalw thy [certificate_def]
paulson@3515
   175
 "!!evs. evs : tls     \
paulson@3515
   176
\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
paulson@3515
   177
by (etac tls.induct 1);
paulson@3515
   178
by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
paulson@3515
   179
by (Fake_parts_insert_tac 2);
paulson@3515
   180
by (Blast_tac 1);
paulson@3515
   181
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
paulson@3515
   182
paulson@3515
   183
paulson@3515
   184
(*Replace key KB in ClientCertKeyEx by (pubK B) *)
paulson@3515
   185
val ClientCertKeyEx_tac = 
paulson@3515
   186
    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
paulson@3515
   187
		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
paulson@3515
   188
    THEN' assume_tac
paulson@3515
   189
    THEN' hyp_subst_tac;
paulson@3515
   190
paulson@3515
   191
fun analz_induct_tac i = 
paulson@3515
   192
    etac tls.induct i   THEN
paulson@3515
   193
    ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
paulson@3515
   194
    ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
paulson@3515
   195
    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
paulson@3515
   196
    rewrite_goals_tac  [certificate_def]  THEN
paulson@3515
   197
    ALLGOALS (asm_simp_tac 
paulson@3515
   198
              (!simpset addsimps [not_parts_not_analz]
paulson@3515
   199
                        setloop split_tac [expand_if]))  THEN
paulson@3515
   200
    (*Remove instances of pubK B:  the Spy already knows all public keys.
paulson@3515
   201
      Combining the two simplifier calls makes them run extremely slowly.*)
paulson@3515
   202
    ALLGOALS (asm_simp_tac 
paulson@3515
   203
              (!simpset addsimps [insert_absorb]
paulson@3515
   204
                        setloop split_tac [expand_if]));
paulson@3515
   205
paulson@3515
   206
paulson@3515
   207
(*** Hashing of nonces ***)
paulson@3515
   208
paulson@3474
   209
(*Every Nonce that's hashed is already in past traffic. *)
paulson@3474
   210
goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
paulson@3474
   211
\                   evs : tls |]  \
paulson@3474
   212
\                ==> Nonce N : parts (sees lost Spy evs)";
paulson@3474
   213
by (etac rev_mp 1);
paulson@3474
   214
by (etac tls.induct 1);
paulson@3515
   215
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
paulson@3515
   216
			             setloop split_tac [expand_if])));
paulson@3515
   217
by (Fake_parts_insert_tac 2);
paulson@3515
   218
by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3515
   219
		               addSEs partsEs) 1));
paulson@3474
   220
qed "Hash_imp_Nonce1";
paulson@3474
   221
paulson@3474
   222
(*Lemma needed to prove Hash_Hash_imp_Nonce*)
paulson@3474
   223
goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
paulson@3474
   224
\                       : parts (sees lost Spy evs);     \
paulson@3474
   225
\                   evs : tls |]  \
paulson@3474
   226
\                ==> Nonce M : parts (sees lost Spy evs)";
paulson@3474
   227
by (etac rev_mp 1);
paulson@3474
   228
by (etac tls.induct 1);
paulson@3515
   229
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
paulson@3515
   230
			             setloop split_tac [expand_if])));
paulson@3515
   231
by (Fake_parts_insert_tac 2);
paulson@3515
   232
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3515
   233
		       addSEs partsEs) 1);
paulson@3474
   234
qed "Hash_imp_Nonce2";
paulson@3474
   235
AddSDs [Hash_imp_Nonce2];
paulson@3474
   236
paulson@3515
   237
paulson@3515
   238
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
paulson@3515
   239
\                ==> Crypt (pubK B) X : parts (sees lost Spy evs)";
paulson@3515
   240
by (etac rev_mp 1);
paulson@3515
   241
by (analz_induct_tac 1);
paulson@3515
   242
by (blast_tac (!claset addIs [parts_insertI]) 1);
paulson@3515
   243
qed "Notes_Crypt_parts_sees";
paulson@3515
   244
paulson@3515
   245
paulson@3515
   246
(*NEEDED??*)
paulson@3474
   247
goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
paulson@3474
   248
\                      : parts (sees lost Spy evs);      \
paulson@3474
   249
\                   evs : tls |]                         \
paulson@3474
   250
\                ==> Nonce M : parts (sees lost Spy evs)";
paulson@3474
   251
by (etac rev_mp 1);
paulson@3474
   252
by (etac tls.induct 1);
paulson@3515
   253
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
paulson@3515
   254
			             setloop split_tac [expand_if])));
paulson@3515
   255
by (Fake_parts_insert_tac 2);
paulson@3515
   256
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
paulson@3515
   257
			      Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   258
		      addSEs partsEs) 1);
paulson@3474
   259
qed "Hash_Hash_imp_Nonce";
paulson@3474
   260
paulson@3474
   261
paulson@3474
   262
(*NEEDED??
paulson@3474
   263
  Every Nonce that's hashed is already in past traffic. 
paulson@3474
   264
  This general formulation is tricky to prove and hard to use, since the
paulson@3474
   265
  2nd premise is typically proved by simplification.*)
paulson@3474
   266
goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
paulson@3474
   267
\                   Nonce N : parts {X};  evs : tls |]  \
paulson@3474
   268
\                ==> Nonce N : parts (sees lost Spy evs)";
paulson@3474
   269
by (etac rev_mp 1);
paulson@3474
   270
by (etac tls.induct 1);
paulson@3515
   271
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
paulson@3515
   272
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
paulson@3515
   273
			      Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   274
		      addSEs partsEs) 1);
paulson@3474
   275
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   276
by (Fake_parts_insert_tac 1);
paulson@3506
   277
(*CertVerify, ClientFinished, ServerFinished (?)*)
paulson@3506
   278
by (REPEAT (Blast_tac 1));
paulson@3474
   279
qed "Hash_imp_Nonce_seen";
paulson@3474
   280
paulson@3474
   281
paulson@3474
   282
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
paulson@3474
   283
paulson@3506
   284
(*B can check A's signature if he has received A's certificate.
paulson@3506
   285
  Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
paulson@3480
   286
  message is Fake.  We don't need guarantees for the Spy anyway.  We must
paulson@3480
   287
  assume A~:lost; otherwise, the Spy can forge A's signature.*)
paulson@3500
   288
goalw thy [certificate_def]
paulson@3506
   289
 "!!evs. [| X = Crypt (priK A)                                        \
paulson@3506
   290
\                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
paulson@3506
   291
\           evs : tls;  A ~: lost;  B ~= Spy |]                       \
paulson@3506
   292
\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
paulson@3506
   293
\          : set evs --> \
paulson@3474
   294
\        X : parts (sees lost Spy evs) --> Says A B X : set evs";
paulson@3480
   295
by (hyp_subst_tac 1);
paulson@3474
   296
by (etac tls.induct 1);
paulson@3515
   297
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
paulson@3474
   298
by (Fake_parts_insert_tac 1);
paulson@3480
   299
(*ServerHello: nonce NB cannot be in X because it's fresh!*)
paulson@3474
   300
by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
paulson@3474
   301
	               addSEs sees_Spy_partsEs) 1);
paulson@3474
   302
qed_spec_mp "TrustCertVerify";
paulson@3474
   303
paulson@3474
   304
paulson@3515
   305
(*If CERTIFICATE VERIFY is present then A has chosen M.*)
paulson@3506
   306
goal thy
paulson@3515
   307
 "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})  \
paulson@3515
   308
\             : parts (sees lost Spy evs);                                \
paulson@3515
   309
\           evs : tls;  A ~: lost |]                                      \
paulson@3515
   310
\        ==> Notes A {|Agent B, Nonce M|} : set evs";
paulson@3515
   311
be rev_mp 1;
paulson@3506
   312
by (etac tls.induct 1);
paulson@3515
   313
by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
paulson@3474
   314
by (Fake_parts_insert_tac 2);
paulson@3474
   315
by (Blast_tac 1);
paulson@3515
   316
qed "UseCertVerify";
paulson@3474
   317
paulson@3480
   318
paulson@3480
   319
(*No collection of keys can help the spy get new private keys*)
paulson@3480
   320
goal thy  
paulson@3480
   321
 "!!evs. evs : tls ==>                                    \
paulson@3480
   322
\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
paulson@3480
   323
\            (priK B : KK | B : lost)";
paulson@3480
   324
by (etac tls.induct 1);
paulson@3515
   325
by (ALLGOALS
paulson@3515
   326
    (asm_simp_tac (analz_image_keys_ss 
paulson@3515
   327
		   addsimps (certificate_def::keys_distinct))));
paulson@3480
   328
(*Fake*) 
paulson@3480
   329
by (spy_analz_tac 2);
paulson@3480
   330
(*Base*)
paulson@3480
   331
by (Blast_tac 1);
paulson@3480
   332
qed_spec_mp "analz_image_priK";
paulson@3480
   333
paulson@3480
   334
paulson@3480
   335
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@3480
   336
goal thy  
paulson@3480
   337
 "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
paulson@3480
   338
\        (X : analz (G Un H))  =  (X : analz H)";
paulson@3480
   339
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
paulson@3480
   340
val lemma = result();
paulson@3480
   341
paulson@3480
   342
(*Knowing some clientKs and serverKs is no help in getting new nonces*)
paulson@3480
   343
goal thy  
paulson@3480
   344
 "!!evs. evs : tls ==>                                 \
paulson@3480
   345
\    ALL KK. KK <= (range clientK Un range serverK) -->           \
paulson@3480
   346
\            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
paulson@3480
   347
\            (Nonce N : analz (sees lost Spy evs))";
paulson@3480
   348
by (etac tls.induct 1);
paulson@3480
   349
by (ClientCertKeyEx_tac 6);
paulson@3480
   350
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3515
   351
by (REPEAT_FIRST (rtac lemma));
paulson@3515
   352
writeln"SLOW simplification: 50 secs!??";
paulson@3515
   353
by (ALLGOALS
paulson@3515
   354
    (asm_simp_tac (analz_image_keys_ss 
paulson@3515
   355
		   addsimps (analz_image_priK::certificate_def::
paulson@3515
   356
			     keys_distinct))));
paulson@3515
   357
by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
paulson@3515
   358
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
paulson@3480
   359
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
paulson@3480
   360
by (Blast_tac 3);
paulson@3480
   361
(*Fake*) 
paulson@3480
   362
by (spy_analz_tac 2);
paulson@3480
   363
(*Base*)
paulson@3480
   364
by (Blast_tac 1);
paulson@3480
   365
qed_spec_mp "analz_image_keys";
paulson@3480
   366
paulson@3480
   367
paulson@3515
   368
(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*)
paulson@3515
   369
goal thy
paulson@3515
   370
 "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
paulson@3515
   371
\        ==> Notes A {|Agent B, Nonce M|} : set evs  -->   \
paulson@3515
   372
\            Nonce M ~: analz (sees lost Spy evs)";
paulson@3474
   373
by (analz_induct_tac 1);
paulson@3474
   374
(*ClientHello*)
paulson@3515
   375
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
paulson@3515
   376
                               addSEs sees_Spy_partsEs) 3);
paulson@3480
   377
(*SpyKeys*)
paulson@3480
   378
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
paulson@3474
   379
(*Fake*)
paulson@3474
   380
by (spy_analz_tac 1);
paulson@3474
   381
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
paulson@3474
   382
by (REPEAT (blast_tac (!claset addSEs partsEs
paulson@3515
   383
			       addDs  [Notes_Crypt_parts_sees,
paulson@3515
   384
				       impOfSubs analz_subset_parts,
paulson@3474
   385
				       Says_imp_sees_Spy' RS analz.Inj]) 1));
paulson@3474
   386
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
paulson@3474
   387
paulson@3474
   388
paulson@3474
   389
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
paulson@3474
   390
paulson@3515
   391
(** First, some lemmas about those write keys.  The proofs for serverK are 
paulson@3515
   392
    nearly identical to those for clientK. **)
paulson@3515
   393
paulson@3515
   394
(*Lemma: those write keys are never sent if M is secure.  
paulson@3515
   395
  Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
paulson@3515
   396
paulson@3474
   397
goal thy 
paulson@3515
   398
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
paulson@3480
   399
\        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
paulson@3480
   400
by (etac rev_mp 1);
paulson@3480
   401
by (analz_induct_tac 1);
paulson@3480
   402
(*SpyKeys*)
paulson@3480
   403
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
paulson@3480
   404
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
paulson@3480
   405
(*Fake*) 
paulson@3480
   406
by (spy_analz_tac 2);
paulson@3480
   407
(*Base*)
paulson@3480
   408
by (Blast_tac 1);
paulson@3474
   409
qed "clientK_notin_parts";
paulson@3474
   410
paulson@3515
   411
Addsimps [clientK_notin_parts];
paulson@3515
   412
AddSEs [clientK_notin_parts RSN (2, rev_notE)];
paulson@3515
   413
paulson@3474
   414
goal thy 
paulson@3515
   415
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
paulson@3480
   416
\        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
paulson@3480
   417
by (etac rev_mp 1);
paulson@3480
   418
by (analz_induct_tac 1);
paulson@3480
   419
(*SpyKeys*)
paulson@3480
   420
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
paulson@3480
   421
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
paulson@3480
   422
(*Fake*) 
paulson@3480
   423
by (spy_analz_tac 2);
paulson@3480
   424
(*Base*)
paulson@3480
   425
by (Blast_tac 1);
paulson@3474
   426
qed "serverK_notin_parts";
paulson@3474
   427
paulson@3515
   428
Addsimps [serverK_notin_parts];
paulson@3515
   429
AddSEs [serverK_notin_parts RSN (2, rev_notE)];
paulson@3515
   430
paulson@3515
   431
(*Lemma: those write keys are never used if M is fresh.  
paulson@3515
   432
  Converse doesn't hold; betraying M doesn't force the keys to be sent!
paulson@3515
   433
  NOT suitable as safe elim rules.*)
paulson@3515
   434
paulson@3515
   435
goal thy 
paulson@3515
   436
 "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
paulson@3515
   437
\        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
paulson@3515
   438
by (etac rev_mp 1);
paulson@3515
   439
by (analz_induct_tac 1);
paulson@3515
   440
(*ClientFinished: since M is fresh, a different instance of clientK was used.*)
paulson@3515
   441
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
paulson@3515
   442
                               addSEs sees_Spy_partsEs) 3);
paulson@3515
   443
by (Fake_parts_insert_tac 2);
paulson@3515
   444
(*Base*)
paulson@3515
   445
by (Blast_tac 1);
paulson@3515
   446
qed "Crypt_clientK_notin_parts";
paulson@3515
   447
paulson@3515
   448
Addsimps [Crypt_clientK_notin_parts];
paulson@3515
   449
AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
paulson@3515
   450
paulson@3515
   451
goal thy 
paulson@3515
   452
 "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
paulson@3515
   453
\        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
paulson@3515
   454
by (etac rev_mp 1);
paulson@3515
   455
by (analz_induct_tac 1);
paulson@3515
   456
(*ServerFinished: since M is fresh, a different instance of serverK was used.*)
paulson@3515
   457
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
paulson@3515
   458
                               addSEs sees_Spy_partsEs) 3);
paulson@3515
   459
by (Fake_parts_insert_tac 2);
paulson@3515
   460
(*Base*)
paulson@3515
   461
by (Blast_tac 1);
paulson@3515
   462
qed "Crypt_serverK_notin_parts";
paulson@3515
   463
paulson@3515
   464
Addsimps [Crypt_serverK_notin_parts];
paulson@3515
   465
AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
paulson@3515
   466
paulson@3515
   467
paulson@3515
   468
(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*)
paulson@3515
   469
goal thy
paulson@3515
   470
 "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
paulson@3515
   471
\           A ~: lost;  evs : tls |] ==> KB = pubK B";
paulson@3515
   472
be rev_mp 1;
paulson@3515
   473
by (analz_induct_tac 1);
paulson@3515
   474
qed "A_Crypt_pubB";
paulson@3515
   475
paulson@3515
   476
paulson@3515
   477
(*** Unicity results for M, the pre-master-secret ***)
paulson@3515
   478
paulson@3515
   479
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
paulson@3515
   480
  It simplifies the proof by discarding needless information about
paulson@3515
   481
	analz (insert X (sees lost Spy evs)) 
paulson@3515
   482
*)
paulson@3515
   483
fun analz_mono_parts_induct_tac i = 
paulson@3515
   484
    etac tls.induct i           THEN 
paulson@3515
   485
    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
paulson@3515
   486
    REPEAT_FIRST analz_mono_contra_tac;
paulson@3515
   487
paulson@3515
   488
paulson@3515
   489
(*M determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
paulson@3515
   490
goal thy 
paulson@3515
   491
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
paulson@3515
   492
\        ==> EX B'. ALL B.   \
paulson@3515
   493
\              Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'";
paulson@3515
   494
by (etac rev_mp 1);
paulson@3515
   495
by (analz_mono_parts_induct_tac 1);
paulson@3515
   496
by (prove_simple_subgoals_tac 1);
paulson@3515
   497
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]
paulson@3515
   498
                           setloop split_tac [expand_if]) 2);
paulson@3515
   499
(*ClientCertKeyEx*)
paulson@3515
   500
by (expand_case_tac "M = ?y" 2 THEN
paulson@3515
   501
    REPEAT (blast_tac (!claset addSEs partsEs) 2));
paulson@3515
   502
by (Fake_parts_insert_tac 1);
paulson@3515
   503
val lemma = result();
paulson@3515
   504
paulson@3515
   505
goal thy 
paulson@3515
   506
 "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees lost Spy evs); \
paulson@3515
   507
\           Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \
paulson@3515
   508
\           Nonce M ~: analz (sees lost Spy evs);                 \
paulson@3515
   509
\           evs : tls |]                                          \
paulson@3515
   510
\        ==> B=B'";
paulson@3515
   511
by (prove_unique_tac lemma 1);
paulson@3515
   512
qed "unique_M";
paulson@3515
   513
paulson@3515
   514
paulson@3515
   515
(*In A's note to herself, M determines A and B.*)
paulson@3515
   516
goal thy 
paulson@3515
   517
 "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]            \
paulson@3515
   518
\ ==> EX A' B'. ALL A B.                                                   \
paulson@3515
   519
\        Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
paulson@3515
   520
by (etac rev_mp 1);
paulson@3515
   521
by (analz_mono_parts_induct_tac 1);
paulson@3515
   522
by (prove_simple_subgoals_tac 1);
paulson@3515
   523
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
paulson@3515
   524
(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
paulson@3515
   525
by (expand_case_tac "M = ?y" 1 THEN
paulson@3515
   526
    blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
paulson@3515
   527
val lemma = result();
paulson@3515
   528
paulson@3515
   529
goal thy 
paulson@3515
   530
 "!!evs. [| Notes A  {|Agent B,  Nonce M|} : set evs;  \
paulson@3515
   531
\           Notes A' {|Agent B', Nonce M|} : set evs;  \
paulson@3515
   532
\           Nonce M ~: analz (sees lost Spy evs);      \
paulson@3515
   533
\           evs : tls |]                               \
paulson@3515
   534
\        ==> A=A' & B=B'";
paulson@3515
   535
by (prove_unique_tac lemma 1);
paulson@3515
   536
qed "Notes_unique_M";
paulson@3515
   537
paulson@3515
   538
paulson@3474
   539
paulson@3474
   540
(*** Protocol goals: if A receives SERVER FINISHED, then B is present 
paulson@3474
   541
     and has used the quoted values XA, XB, etc.  Note that it is up to A
paulson@3474
   542
     to compare XA with what she originally sent.
paulson@3474
   543
***)
paulson@3474
   544
paulson@3515
   545
(*The mention of her name (A) in X assumes A that B knows who she is.*)
paulson@3515
   546
goal thy
paulson@3515
   547
 "!!evs. [| X = Crypt (serverK(NA,NB,M))                                \
paulson@3515
   548
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},           \
paulson@3515
   549
\                        Nonce NA, Agent XA, Agent A,                   \
paulson@3506
   550
\                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
paulson@3515
   551
\           evs : tls;  A ~: lost;  B ~: lost |]                        \
paulson@3515
   552
\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                 \
paulson@3480
   553
\        X : parts (sees lost Spy evs) --> Says B A X : set evs";
paulson@3480
   554
by (hyp_subst_tac 1);
paulson@3515
   555
by (analz_induct_tac 1);
paulson@3515
   556
by (REPEAT_FIRST (rtac impI));
paulson@3480
   557
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3480
   558
by (REPEAT (rtac impI 1));
paulson@3480
   559
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
paulson@3480
   560
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
paulson@3480
   561
				     not_parts_not_analz]) 2);
paulson@3474
   562
by (Fake_parts_insert_tac 1);
paulson@3474
   563
qed_spec_mp "TrustServerFinished";
paulson@3474
   564
paulson@3474
   565
paulson@3515
   566
(*This version refers not to SERVER FINISHED but to any message from B.
paulson@3515
   567
  We don't assume B has received CERTIFICATE VERIFY, and an intruder could
paulson@3515
   568
  have changed A's identity in all other messages, so we can't be sure
paulson@3515
   569
  that B sends his message to A.*)
paulson@3515
   570
goal thy
paulson@3515
   571
 "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
paulson@3515
   572
\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
paulson@3515
   573
\            Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs)  --> \
paulson@3515
   574
\            (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
paulson@3515
   575
by (analz_induct_tac 1);
paulson@3515
   576
by (REPEAT_FIRST (rtac impI));
paulson@3515
   577
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3515
   578
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
paulson@3515
   579
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
paulson@3515
   580
				     not_parts_not_analz]) 2);
paulson@3515
   581
by (Fake_parts_insert_tac 1);
paulson@3515
   582
(*ServerFinished.  If the message is old then apply induction hypothesis...*)
paulson@3515
   583
by (rtac conjI 1 THEN Blast_tac 2);
paulson@3515
   584
(*...otherwise delete induction hyp and use unicity of M.*)
paulson@3515
   585
by (thin_tac "?PP-->?QQ" 1);
paulson@3515
   586
by (Step_tac 1);
paulson@3515
   587
by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
paulson@3515
   588
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
paulson@3515
   589
by (blast_tac (!claset addSEs [MPair_parts]
paulson@3515
   590
		       addDs  [Notes_Crypt_parts_sees,
paulson@3515
   591
			       Says_imp_sees_Spy' RS parts.Inj,
paulson@3515
   592
			       unique_M]) 1);
paulson@3515
   593
qed_spec_mp "TrustServerMsg";
paulson@3515
   594
paulson@3515
   595
paulson@3515
   596
(*** Protocol goal: if B receives any message encrypted with clientK
paulson@3515
   597
     then A has sent it, ASSUMING that A chose M.  Authentication is
paulson@3515
   598
     assumed here; B cannot verify it.  But if the message is
paulson@3515
   599
     CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
paulson@3506
   600
***)
paulson@3515
   601
goal thy
paulson@3515
   602
 "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
paulson@3515
   603
\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
paulson@3515
   604
\            Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) -->  \
paulson@3515
   605
\            Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
paulson@3515
   606
by (analz_induct_tac 1);
paulson@3515
   607
by (REPEAT_FIRST (rtac impI));
paulson@3480
   608
(*Fake: the Spy doesn't have the critical session key!*)
paulson@3480
   609
by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
paulson@3480
   610
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
paulson@3480
   611
				     not_parts_not_analz]) 2);
paulson@3474
   612
by (Fake_parts_insert_tac 1);
paulson@3515
   613
(*ClientFinished.  If the message is old then apply induction hypothesis...*)
paulson@3515
   614
by (step_tac (!claset delrules [conjI]) 1);
paulson@3515
   615
by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
paulson@3515
   616
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
paulson@3515
   617
by (blast_tac (!claset addSEs [MPair_parts]
paulson@3515
   618
		       addDs  [Notes_unique_M]) 1);
paulson@3515
   619
qed_spec_mp "TrustClientMsg";
paulson@3506
   620
paulson@3506
   621
paulson@3506
   622
(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
paulson@3506
   623
     check a CERTIFICATE VERIFY from A, then A has used the quoted
paulson@3506
   624
     values XA, XB, etc.  Even this one requires A to be uncompromised.
paulson@3506
   625
 ***)
paulson@3506
   626
goal thy
paulson@3515
   627
 "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs;             \
paulson@3515
   628
\           Says B  A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
paulson@3515
   629
\             : set evs;                                                  \
paulson@3515
   630
\           Says A'' B (Crypt (priK A)                                    \
paulson@3515
   631
\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))    \
paulson@3515
   632
\             : set evs;                                                  \
paulson@3515
   633
\        evs : tls;  A ~: lost;  B ~: lost |]                             \
paulson@3515
   634
\     ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
paulson@3515
   635
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
paulson@3515
   636
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
paulson@3515
   637
qed "AuthClientFinished";