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