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