src/HOL/Auth/TLS.ML
author paulson
Tue Jul 01 11:11:42 1997 +0200 (1997-07-01)
changeset 3474 44249bba00ec
child 3480 d59bbf053258
permissions -rw-r--r--
Baby TLS. Proofs work, but model seems unrealistic
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@3474
     7
The Spy's state is recorded as the trace of message.  But if he himself is 
paulson@3474
     8
the Client and invents M, then the event he sends contains M encrypted with B's
paulson@3474
     9
public key.  From the trace there is no reason to believe that the spy knows
paulson@3474
    10
M, and yet the spy actually chose M!  So, in any property concerning the 
paulson@3474
    11
secrecy of some item, one must somehow establish that the spy didn't choose
paulson@3474
    12
the item.  In practice, this weakness does little harm, since one can expect
paulson@3474
    13
few guarantees when communicating directly with an enemy.
paulson@3474
    14
paulson@3474
    15
The model, at present, doesn't recognize that if the Spy has NA, NB and M then
paulson@3474
    16
he also has clientK(NA,NB,M) and serverK(NA,NB,M).  Maybe this doesn't really
paulson@3474
    17
matter, since one can prove that he doesn't get M.
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@3474
    26
paulson@3474
    27
(*Injectiveness of key-generating functions*)
paulson@3474
    28
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
paulson@3474
    29
paulson@3474
    30
(* invKey(clientK x) = clientK x  and similarly for serverK*)
paulson@3474
    31
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
paulson@3474
    32
	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
paulson@3474
    33
	  
paulson@3474
    34
paulson@3474
    35
(*Replacing the variable by a constant improves search speed by 50%!*)
paulson@3474
    36
val Says_imp_sees_Spy' = 
paulson@3474
    37
    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
paulson@3474
    38
paulson@3474
    39
paulson@3474
    40
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
paulson@3474
    41
paulson@3474
    42
goal thy "pubK A ~= clientK arg";
paulson@3474
    43
br notI 1;
paulson@3474
    44
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
paulson@3474
    45
by (Full_simp_tac 1);
paulson@3474
    46
qed "pubK_neq_clientK";
paulson@3474
    47
paulson@3474
    48
goal thy "pubK A ~= serverK 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_serverK";
paulson@3474
    53
paulson@3474
    54
goal thy "priK A ~= clientK 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 "priK_neq_clientK";
paulson@3474
    59
paulson@3474
    60
goal thy "priK A ~= serverK 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_serverK";
paulson@3474
    65
paulson@3474
    66
val ths = [pubK_neq_clientK, pubK_neq_serverK, 
paulson@3474
    67
	   priK_neq_clientK, priK_neq_serverK];
paulson@3474
    68
AddIffs (ths @ (ths RL [not_sym]));
paulson@3474
    69
paulson@3474
    70
paulson@3474
    71
(**** Protocol Proofs ****)
paulson@3474
    72
paulson@3474
    73
(*A "possibility property": there are traces that reach the end.
paulson@3474
    74
  This protocol has three end points and six messages to consider.*)
paulson@3474
    75
paulson@3474
    76
(*Possibility property ending with ServerFinished.*)
paulson@3474
    77
goal thy 
paulson@3474
    78
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
paulson@3474
    79
\  Says B A (Crypt (serverK(NA,NB,M))                 \
paulson@3474
    80
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
paulson@3474
    81
\                   Nonce NA, Agent XA, Agent A,      \
paulson@3474
    82
\                   Nonce NB, Agent XB,               \
paulson@3474
    83
\                   Crypt (priK Server) {|Agent B, Key (pubK B)|}|})) \
paulson@3474
    84
\    : set evs";
paulson@3474
    85
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
    86
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3474
    87
	  RS tls.ServerFinished) 2);
paulson@3474
    88
by possibility_tac;
paulson@3474
    89
result();
paulson@3474
    90
paulson@3474
    91
(*And one for ClientFinished.  Either FINISHED message may come first.*)
paulson@3474
    92
goal thy 
paulson@3474
    93
 "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
paulson@3474
    94
\  Says A B (Crypt (clientK(NA,NB,M))                 \
paulson@3474
    95
\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
paulson@3474
    96
\                   Nonce NA, Agent XA,               \
paulson@3474
    97
\                   Crypt (priK Server) {|Agent A, Key (pubK A)|},      \
paulson@3474
    98
\                   Nonce NB, Agent XB, Agent B|})) : set evs";
paulson@3474
    99
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   100
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
paulson@3474
   101
	  RS tls.ClientFinished) 2);
paulson@3474
   102
by possibility_tac;
paulson@3474
   103
result();
paulson@3474
   104
paulson@3474
   105
(*Another one, for CertVerify (which is optional)*)
paulson@3474
   106
goal thy 
paulson@3474
   107
 "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
paulson@3474
   108
\  Says A B (Crypt (priK A)                 \
paulson@3474
   109
\            (Hash{|Nonce NB,               \
paulson@3474
   110
\                   Crypt (priK Server)     \
paulson@3474
   111
\                         {|Agent B, Key (pubK B)|}|})) : set evs";
paulson@3474
   112
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3474
   113
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
paulson@3474
   114
by possibility_tac;
paulson@3474
   115
result();
paulson@3474
   116
paulson@3474
   117
paulson@3474
   118
(**** Inductive proofs about tls ****)
paulson@3474
   119
paulson@3474
   120
(*Nobody sends themselves messages*)
paulson@3474
   121
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
paulson@3474
   122
by (etac tls.induct 1);
paulson@3474
   123
by (Auto_tac());
paulson@3474
   124
qed_spec_mp "not_Says_to_self";
paulson@3474
   125
Addsimps [not_Says_to_self];
paulson@3474
   126
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@3474
   127
paulson@3474
   128
paulson@3474
   129
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
paulson@3474
   130
    sends messages containing X! **)
paulson@3474
   131
paulson@3474
   132
(*Spy never sees another agent's private key! (unless it's lost at start)*)
paulson@3474
   133
goal thy 
paulson@3474
   134
 "!!evs. evs : tls \
paulson@3474
   135
\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
paulson@3474
   136
by (etac tls.induct 1);
paulson@3474
   137
by (prove_simple_subgoals_tac 1);
paulson@3474
   138
by (Fake_parts_insert_tac 1);
paulson@3474
   139
qed "Spy_see_priK";
paulson@3474
   140
Addsimps [Spy_see_priK];
paulson@3474
   141
paulson@3474
   142
goal thy 
paulson@3474
   143
 "!!evs. evs : tls \
paulson@3474
   144
\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
paulson@3474
   145
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@3474
   146
qed "Spy_analz_priK";
paulson@3474
   147
Addsimps [Spy_analz_priK];
paulson@3474
   148
paulson@3474
   149
goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
paulson@3474
   150
\                  evs : tls |] ==> A:lost";
paulson@3474
   151
by (blast_tac (!claset addDs [Spy_see_priK]) 1);
paulson@3474
   152
qed "Spy_see_priK_D";
paulson@3474
   153
paulson@3474
   154
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
paulson@3474
   155
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
paulson@3474
   156
paulson@3474
   157
paulson@3474
   158
(*Every Nonce that's hashed is already in past traffic. *)
paulson@3474
   159
goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
paulson@3474
   160
\                   evs : tls |]  \
paulson@3474
   161
\                ==> Nonce N : parts (sees lost Spy evs)";
paulson@3474
   162
by (etac rev_mp 1);
paulson@3474
   163
by (etac tls.induct 1);
paulson@3474
   164
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   165
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   166
		      addSEs partsEs) 1);
paulson@3474
   167
by (Fake_parts_insert_tac 1);
paulson@3474
   168
qed "Hash_imp_Nonce1";
paulson@3474
   169
paulson@3474
   170
(*Lemma needed to prove Hash_Hash_imp_Nonce*)
paulson@3474
   171
goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
paulson@3474
   172
\                       : parts (sees lost Spy evs);     \
paulson@3474
   173
\                   evs : tls |]  \
paulson@3474
   174
\                ==> Nonce M : parts (sees lost Spy evs)";
paulson@3474
   175
by (etac rev_mp 1);
paulson@3474
   176
by (etac tls.induct 1);
paulson@3474
   177
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   178
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   179
		      addSEs partsEs) 1);
paulson@3474
   180
by (Fake_parts_insert_tac 1);
paulson@3474
   181
qed "Hash_imp_Nonce2";
paulson@3474
   182
AddSDs [Hash_imp_Nonce2];
paulson@3474
   183
paulson@3474
   184
goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
paulson@3474
   185
\                      : parts (sees lost Spy evs);      \
paulson@3474
   186
\                   evs : tls |]                         \
paulson@3474
   187
\                ==> Nonce M : parts (sees lost Spy evs)";
paulson@3474
   188
by (etac rev_mp 1);
paulson@3474
   189
by (etac tls.induct 1);
paulson@3474
   190
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   191
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   192
		      addSEs partsEs) 1);
paulson@3474
   193
by (Fake_parts_insert_tac 1);
paulson@3474
   194
qed "Hash_Hash_imp_Nonce";
paulson@3474
   195
paulson@3474
   196
paulson@3474
   197
(*NEEDED??
paulson@3474
   198
  Every Nonce that's hashed is already in past traffic. 
paulson@3474
   199
  This general formulation is tricky to prove and hard to use, since the
paulson@3474
   200
  2nd premise is typically proved by simplification.*)
paulson@3474
   201
goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
paulson@3474
   202
\                   Nonce N : parts {X};  evs : tls |]  \
paulson@3474
   203
\                ==> Nonce N : parts (sees lost Spy evs)";
paulson@3474
   204
by (etac rev_mp 1);
paulson@3474
   205
by (etac tls.induct 1);
paulson@3474
   206
by (ALLGOALS Asm_simp_tac);
paulson@3474
   207
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@3474
   208
		      addSEs partsEs) 1);
paulson@3474
   209
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
paulson@3474
   210
(*ServerFinished*)
paulson@3474
   211
by (Blast_tac 3);
paulson@3474
   212
(*ClientFinished*)
paulson@3474
   213
by (Blast_tac 2);
paulson@3474
   214
by (Fake_parts_insert_tac 1);
paulson@3474
   215
qed "Hash_imp_Nonce_seen";
paulson@3474
   216
paulson@3474
   217
paulson@3474
   218
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
paulson@3474
   219
paulson@3474
   220
(*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
paulson@3474
   221
  message is Fake.  We don't need guarantees for the Spy anyway.*)
paulson@3474
   222
goal thy 
paulson@3474
   223
 "!!evs. [| X = Crypt (priK A)                          \
paulson@3474
   224
\                 (Hash{|Nonce NB,                                      \
paulson@3474
   225
\                        Crypt (priK Server) {|Agent B, Key KB|}|});    \
paulson@3474
   226
\           evs : tls;  A ~: lost;  B ~= Spy |]         \
paulson@3474
   227
\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
paulson@3474
   228
\                   Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
paulson@3474
   229
\        X : parts (sees lost Spy evs) --> Says A B X : set evs";
paulson@3474
   230
by (Asm_simp_tac 1);
paulson@3474
   231
by (etac tls.induct 1);
paulson@3474
   232
by (ALLGOALS Asm_simp_tac);
paulson@3474
   233
by (Fake_parts_insert_tac 1);
paulson@3474
   234
(*ServerHello*)
paulson@3474
   235
by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
paulson@3474
   236
	               addSEs sees_Spy_partsEs) 1);
paulson@3474
   237
qed_spec_mp "TrustCertVerify";
paulson@3474
   238
paulson@3474
   239
paulson@3474
   240
(*This lemma says that no false certificates exist.  One might extend the
paulson@3474
   241
  model to include bogus certificates for the lost agents, but there seems
paulson@3474
   242
  little point in doing so: the loss of their private keys is a worse
paulson@3474
   243
  breach of security.*)
paulson@3474
   244
goal thy 
paulson@3474
   245
 "!!evs. evs : tls     \
paulson@3474
   246
\    ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \
paulson@3474
   247
\        --> KB = pubK B";
paulson@3474
   248
by (etac tls.induct 1);
paulson@3474
   249
by (ALLGOALS Asm_simp_tac);
paulson@3474
   250
by (Fake_parts_insert_tac 2);
paulson@3474
   251
by (Blast_tac 1);
paulson@3474
   252
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
paulson@3474
   253
paulson@3474
   254
paulson@3474
   255
(*Replace key KB in ClientCertKeyEx by (pubK B) *)
paulson@3474
   256
val ClientCertKeyEx_tac = 
paulson@3474
   257
    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
paulson@3474
   258
		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
paulson@3474
   259
    THEN' assume_tac
paulson@3474
   260
    THEN' hyp_subst_tac;
paulson@3474
   261
paulson@3474
   262
fun analz_induct_tac i = 
paulson@3474
   263
    etac tls.induct i   THEN
paulson@3474
   264
    ClientCertKeyEx_tac  (i+4)  THEN
paulson@3474
   265
    ALLGOALS (asm_simp_tac 
paulson@3474
   266
              (!simpset addsimps [not_parts_not_analz]
paulson@3474
   267
                        setloop split_tac [expand_if]))  THEN
paulson@3474
   268
    (*Remove instances of pubK B:  the Spy already knows all public keys.
paulson@3474
   269
      Combining the two simplifier calls makes them run extremely slowly.*)
paulson@3474
   270
    ALLGOALS (asm_simp_tac 
paulson@3474
   271
              (!simpset addsimps [insert_absorb]
paulson@3474
   272
                        setloop split_tac [expand_if]));
paulson@3474
   273
paulson@3474
   274
(*If A sends ClientCertKeyEx to an honest agent B, then M will stay secret.*)
paulson@3474
   275
goal thy 
paulson@3474
   276
 "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |] ==> \
paulson@3474
   277
\    Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
paulson@3474
   278
\               Crypt KB (Nonce M)|} : set evs -->  \
paulson@3474
   279
\    Nonce M ~: analz (sees lost Spy evs)";
paulson@3474
   280
by (analz_induct_tac 1);
paulson@3474
   281
(*ClientHello*)
paulson@3474
   282
by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
paulson@3474
   283
(*Fake*)
paulson@3474
   284
by (spy_analz_tac 1);
paulson@3474
   285
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
paulson@3474
   286
by (REPEAT (blast_tac (!claset addSEs partsEs
paulson@3474
   287
			       addDs  [impOfSubs analz_subset_parts,
paulson@3474
   288
				       Says_imp_sees_Spy' RS analz.Inj]) 1));
paulson@3474
   289
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
paulson@3474
   290
paulson@3474
   291
paulson@3474
   292
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
paulson@3474
   293
paulson@3474
   294
(*In fact, nothing of the form clientK(NA,NB,M) or serverK(NA,NB,M) is ever
paulson@3474
   295
  sent!  These two theorems are too strong: the Spy is quite capable of
paulson@3474
   296
  forming many items of the form serverK(NA,NB,M).
paulson@3474
   297
  Additional Fake rules could model this capability.*)
paulson@3474
   298
paulson@3474
   299
goal thy 
paulson@3474
   300
 "!!evs. evs : tls ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
paulson@3474
   301
by (etac tls.induct 1);
paulson@3474
   302
by (prove_simple_subgoals_tac 1);
paulson@3474
   303
by (Fake_parts_insert_tac 1);
paulson@3474
   304
qed "clientK_notin_parts";
paulson@3474
   305
paulson@3474
   306
goal thy 
paulson@3474
   307
 "!!evs. evs : tls ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
paulson@3474
   308
by (etac tls.induct 1);
paulson@3474
   309
by (prove_simple_subgoals_tac 1);
paulson@3474
   310
by (Fake_parts_insert_tac 1);
paulson@3474
   311
qed "serverK_notin_parts";
paulson@3474
   312
paulson@3474
   313
(*We need a version of AddIffs that takes CONDITIONAL equivalences*)
paulson@3474
   314
val ths = [clientK_notin_parts, clientK_notin_parts RS not_parts_not_analz,
paulson@3474
   315
	   serverK_notin_parts, serverK_notin_parts RS not_parts_not_analz];
paulson@3474
   316
Addsimps ths;
paulson@3474
   317
AddSEs (ths RLN (2, [rev_notE]));
paulson@3474
   318
paulson@3474
   319
paulson@3474
   320
(*** Protocol goals: if A receives SERVER FINISHED, then B is present 
paulson@3474
   321
     and has used the quoted values XA, XB, etc.  Note that it is up to A
paulson@3474
   322
     to compare XA with what she originally sent.
paulson@3474
   323
***)
paulson@3474
   324
paulson@3474
   325
(*Perhaps A~=Spy is unnecessary, but there's no obvious proof if the first
paulson@3474
   326
  message is Fake.  We don't need guarantees for the Spy anyway.*)
paulson@3474
   327
goal thy 
paulson@3474
   328
 "!!evs. [| X = Crypt (serverK(NA,NB,M))                        \
paulson@3474
   329
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
paulson@3474
   330
\                        Nonce NA, Agent XA, Agent A,           \
paulson@3474
   331
\                        Nonce NB, Agent XB,                    \
paulson@3474
   332
\                        Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
paulson@3474
   333
\           evs : tls;  A~=Spy;  B ~: lost |] ==>               \
paulson@3474
   334
\    Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
paulson@3474
   335
\               Crypt KB (Nonce M)|} : set evs -->              \
paulson@3474
   336
\    X : parts (sees lost Spy evs) --> Says B A X : set evs";
paulson@3474
   337
by (Asm_simp_tac 1);
paulson@3474
   338
by (etac tls.induct 1);
paulson@3474
   339
by (ALLGOALS Asm_simp_tac);
paulson@3474
   340
by (Fake_parts_insert_tac 1);
paulson@3474
   341
(*ClientCertKeyEx*)
paulson@3474
   342
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
paulson@3474
   343
                       addSEs sees_Spy_partsEs) 1);
paulson@3474
   344
qed_spec_mp "TrustServerFinished";
paulson@3474
   345
paulson@3474
   346
paulson@3474
   347
(*** Protocol goal: if B receives CLIENT FINISHED, then A  is present ??
paulson@3474
   348
     and has used the quoted values XA, XB, etc.  Note that it is up to B
paulson@3474
   349
     to compare XB with what he originally sent. ***)
paulson@3474
   350
paulson@3474
   351
(*This result seems far too strong--it may be provable because the current
paulson@3474
   352
  model gives the Spy access to NO keys of the form clientK(NA,NB,M).*)
paulson@3474
   353
goal thy 
paulson@3474
   354
 "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
paulson@3474
   355
\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
paulson@3474
   356
\                        Nonce NA, Agent XA,                    \
paulson@3474
   357
\                        Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
paulson@3474
   358
\                        Nonce NB, Agent XB, Agent B|});        \
paulson@3474
   359
\           evs : tls |] ==>               \
paulson@3474
   360
\    X : parts (sees lost Spy evs) --> Says A B X : set evs";
paulson@3474
   361
by (Asm_simp_tac 1);
paulson@3474
   362
by (etac tls.induct 1);
paulson@3474
   363
by (ALLGOALS Asm_simp_tac);
paulson@3474
   364
by (Blast_tac 1);
paulson@3474
   365
by (Fake_parts_insert_tac 1);
paulson@3474
   366
qed_spec_mp "TrustClientFinished";
paulson@3474
   367
paulson@3474
   368
paulson@3474
   369