Baby TLS. Proofs work, but model seems unrealistic
authorpaulson
Tue Jul 01 11:11:42 1997 +0200 (1997-07-01)
changeset 347444249bba00ec
parent 3473 c2334f9532ab
child 3475 368206f85f4b
Baby TLS. Proofs work, but model seems unrealistic
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Jul 01 11:11:42 1997 +0200
     1.3 @@ -0,0 +1,369 @@
     1.4 +(*  Title:      HOL/Auth/TLS
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +
     1.9 +The public-key model has a weakness, especially concerning anonymous sessions.
    1.10 +The Spy's state is recorded as the trace of message.  But if he himself is 
    1.11 +the Client and invents M, then the event he sends contains M encrypted with B's
    1.12 +public key.  From the trace there is no reason to believe that the spy knows
    1.13 +M, and yet the spy actually chose M!  So, in any property concerning the 
    1.14 +secrecy of some item, one must somehow establish that the spy didn't choose
    1.15 +the item.  In practice, this weakness does little harm, since one can expect
    1.16 +few guarantees when communicating directly with an enemy.
    1.17 +
    1.18 +The model, at present, doesn't recognize that if the Spy has NA, NB and M then
    1.19 +he also has clientK(NA,NB,M) and serverK(NA,NB,M).  Maybe this doesn't really
    1.20 +matter, since one can prove that he doesn't get M.
    1.21 +*)
    1.22 +
    1.23 +open TLS;
    1.24 +
    1.25 +proof_timing:=true;
    1.26 +HOL_quantifiers := false;
    1.27 +
    1.28 +AddIffs [Spy_in_lost, Server_not_lost];
    1.29 +
    1.30 +(*Injectiveness of key-generating functions*)
    1.31 +AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
    1.32 +
    1.33 +(* invKey(clientK x) = clientK x  and similarly for serverK*)
    1.34 +Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    1.35 +	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
    1.36 +	  
    1.37 +
    1.38 +(*Replacing the variable by a constant improves search speed by 50%!*)
    1.39 +val Says_imp_sees_Spy' = 
    1.40 +    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    1.41 +
    1.42 +
    1.43 +(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    1.44 +
    1.45 +goal thy "pubK A ~= clientK arg";
    1.46 +br notI 1;
    1.47 +by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.48 +by (Full_simp_tac 1);
    1.49 +qed "pubK_neq_clientK";
    1.50 +
    1.51 +goal thy "pubK A ~= serverK arg";
    1.52 +br notI 1;
    1.53 +by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.54 +by (Full_simp_tac 1);
    1.55 +qed "pubK_neq_serverK";
    1.56 +
    1.57 +goal thy "priK A ~= clientK arg";
    1.58 +br notI 1;
    1.59 +by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.60 +by (Full_simp_tac 1);
    1.61 +qed "priK_neq_clientK";
    1.62 +
    1.63 +goal thy "priK A ~= serverK arg";
    1.64 +br notI 1;
    1.65 +by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.66 +by (Full_simp_tac 1);
    1.67 +qed "priK_neq_serverK";
    1.68 +
    1.69 +val ths = [pubK_neq_clientK, pubK_neq_serverK, 
    1.70 +	   priK_neq_clientK, priK_neq_serverK];
    1.71 +AddIffs (ths @ (ths RL [not_sym]));
    1.72 +
    1.73 +
    1.74 +(**** Protocol Proofs ****)
    1.75 +
    1.76 +(*A "possibility property": there are traces that reach the end.
    1.77 +  This protocol has three end points and six messages to consider.*)
    1.78 +
    1.79 +(*Possibility property ending with ServerFinished.*)
    1.80 +goal thy 
    1.81 + "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
    1.82 +\  Says B A (Crypt (serverK(NA,NB,M))                 \
    1.83 +\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
    1.84 +\                   Nonce NA, Agent XA, Agent A,      \
    1.85 +\                   Nonce NB, Agent XB,               \
    1.86 +\                   Crypt (priK Server) {|Agent B, Key (pubK B)|}|})) \
    1.87 +\    : set evs";
    1.88 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.89 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.90 +	  RS tls.ServerFinished) 2);
    1.91 +by possibility_tac;
    1.92 +result();
    1.93 +
    1.94 +(*And one for ClientFinished.  Either FINISHED message may come first.*)
    1.95 +goal thy 
    1.96 + "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
    1.97 +\  Says A B (Crypt (clientK(NA,NB,M))                 \
    1.98 +\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
    1.99 +\                   Nonce NA, Agent XA,               \
   1.100 +\                   Crypt (priK Server) {|Agent A, Key (pubK A)|},      \
   1.101 +\                   Nonce NB, Agent XB, Agent B|})) : set evs";
   1.102 +by (REPEAT (resolve_tac [exI,bexI] 1));
   1.103 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   1.104 +	  RS tls.ClientFinished) 2);
   1.105 +by possibility_tac;
   1.106 +result();
   1.107 +
   1.108 +(*Another one, for CertVerify (which is optional)*)
   1.109 +goal thy 
   1.110 + "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
   1.111 +\  Says A B (Crypt (priK A)                 \
   1.112 +\            (Hash{|Nonce NB,               \
   1.113 +\                   Crypt (priK Server)     \
   1.114 +\                         {|Agent B, Key (pubK B)|}|})) : set evs";
   1.115 +by (REPEAT (resolve_tac [exI,bexI] 1));
   1.116 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
   1.117 +by possibility_tac;
   1.118 +result();
   1.119 +
   1.120 +
   1.121 +(**** Inductive proofs about tls ****)
   1.122 +
   1.123 +(*Nobody sends themselves messages*)
   1.124 +goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   1.125 +by (etac tls.induct 1);
   1.126 +by (Auto_tac());
   1.127 +qed_spec_mp "not_Says_to_self";
   1.128 +Addsimps [not_Says_to_self];
   1.129 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   1.130 +
   1.131 +
   1.132 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   1.133 +    sends messages containing X! **)
   1.134 +
   1.135 +(*Spy never sees another agent's private key! (unless it's lost at start)*)
   1.136 +goal thy 
   1.137 + "!!evs. evs : tls \
   1.138 +\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
   1.139 +by (etac tls.induct 1);
   1.140 +by (prove_simple_subgoals_tac 1);
   1.141 +by (Fake_parts_insert_tac 1);
   1.142 +qed "Spy_see_priK";
   1.143 +Addsimps [Spy_see_priK];
   1.144 +
   1.145 +goal thy 
   1.146 + "!!evs. evs : tls \
   1.147 +\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
   1.148 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   1.149 +qed "Spy_analz_priK";
   1.150 +Addsimps [Spy_analz_priK];
   1.151 +
   1.152 +goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
   1.153 +\                  evs : tls |] ==> A:lost";
   1.154 +by (blast_tac (!claset addDs [Spy_see_priK]) 1);
   1.155 +qed "Spy_see_priK_D";
   1.156 +
   1.157 +bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
   1.158 +AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
   1.159 +
   1.160 +
   1.161 +(*Every Nonce that's hashed is already in past traffic. *)
   1.162 +goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
   1.163 +\                   evs : tls |]  \
   1.164 +\                ==> Nonce N : parts (sees lost Spy evs)";
   1.165 +by (etac rev_mp 1);
   1.166 +by (etac tls.induct 1);
   1.167 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.168 +by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.169 +		      addSEs partsEs) 1);
   1.170 +by (Fake_parts_insert_tac 1);
   1.171 +qed "Hash_imp_Nonce1";
   1.172 +
   1.173 +(*Lemma needed to prove Hash_Hash_imp_Nonce*)
   1.174 +goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
   1.175 +\                       : parts (sees lost Spy evs);     \
   1.176 +\                   evs : tls |]  \
   1.177 +\                ==> Nonce M : parts (sees lost Spy evs)";
   1.178 +by (etac rev_mp 1);
   1.179 +by (etac tls.induct 1);
   1.180 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.181 +by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.182 +		      addSEs partsEs) 1);
   1.183 +by (Fake_parts_insert_tac 1);
   1.184 +qed "Hash_imp_Nonce2";
   1.185 +AddSDs [Hash_imp_Nonce2];
   1.186 +
   1.187 +goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
   1.188 +\                      : parts (sees lost Spy evs);      \
   1.189 +\                   evs : tls |]                         \
   1.190 +\                ==> Nonce M : parts (sees lost Spy evs)";
   1.191 +by (etac rev_mp 1);
   1.192 +by (etac tls.induct 1);
   1.193 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.194 +by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.195 +		      addSEs partsEs) 1);
   1.196 +by (Fake_parts_insert_tac 1);
   1.197 +qed "Hash_Hash_imp_Nonce";
   1.198 +
   1.199 +
   1.200 +(*NEEDED??
   1.201 +  Every Nonce that's hashed is already in past traffic. 
   1.202 +  This general formulation is tricky to prove and hard to use, since the
   1.203 +  2nd premise is typically proved by simplification.*)
   1.204 +goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
   1.205 +\                   Nonce N : parts {X};  evs : tls |]  \
   1.206 +\                ==> Nonce N : parts (sees lost Spy evs)";
   1.207 +by (etac rev_mp 1);
   1.208 +by (etac tls.induct 1);
   1.209 +by (ALLGOALS Asm_simp_tac);
   1.210 +by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.211 +		      addSEs partsEs) 1);
   1.212 +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.213 +(*ServerFinished*)
   1.214 +by (Blast_tac 3);
   1.215 +(*ClientFinished*)
   1.216 +by (Blast_tac 2);
   1.217 +by (Fake_parts_insert_tac 1);
   1.218 +qed "Hash_imp_Nonce_seen";
   1.219 +
   1.220 +
   1.221 +(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   1.222 +
   1.223 +(*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   1.224 +  message is Fake.  We don't need guarantees for the Spy anyway.*)
   1.225 +goal thy 
   1.226 + "!!evs. [| X = Crypt (priK A)                          \
   1.227 +\                 (Hash{|Nonce NB,                                      \
   1.228 +\                        Crypt (priK Server) {|Agent B, Key KB|}|});    \
   1.229 +\           evs : tls;  A ~: lost;  B ~= Spy |]         \
   1.230 +\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
   1.231 +\                   Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
   1.232 +\        X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.233 +by (Asm_simp_tac 1);
   1.234 +by (etac tls.induct 1);
   1.235 +by (ALLGOALS Asm_simp_tac);
   1.236 +by (Fake_parts_insert_tac 1);
   1.237 +(*ServerHello*)
   1.238 +by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
   1.239 +	               addSEs sees_Spy_partsEs) 1);
   1.240 +qed_spec_mp "TrustCertVerify";
   1.241 +
   1.242 +
   1.243 +(*This lemma says that no false certificates exist.  One might extend the
   1.244 +  model to include bogus certificates for the lost agents, but there seems
   1.245 +  little point in doing so: the loss of their private keys is a worse
   1.246 +  breach of security.*)
   1.247 +goal thy 
   1.248 + "!!evs. evs : tls     \
   1.249 +\    ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \
   1.250 +\        --> KB = pubK B";
   1.251 +by (etac tls.induct 1);
   1.252 +by (ALLGOALS Asm_simp_tac);
   1.253 +by (Fake_parts_insert_tac 2);
   1.254 +by (Blast_tac 1);
   1.255 +bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   1.256 +
   1.257 +
   1.258 +(*Replace key KB in ClientCertKeyEx by (pubK B) *)
   1.259 +val ClientCertKeyEx_tac = 
   1.260 +    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
   1.261 +		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
   1.262 +    THEN' assume_tac
   1.263 +    THEN' hyp_subst_tac;
   1.264 +
   1.265 +fun analz_induct_tac i = 
   1.266 +    etac tls.induct i   THEN
   1.267 +    ClientCertKeyEx_tac  (i+4)  THEN
   1.268 +    ALLGOALS (asm_simp_tac 
   1.269 +              (!simpset addsimps [not_parts_not_analz]
   1.270 +                        setloop split_tac [expand_if]))  THEN
   1.271 +    (*Remove instances of pubK B:  the Spy already knows all public keys.
   1.272 +      Combining the two simplifier calls makes them run extremely slowly.*)
   1.273 +    ALLGOALS (asm_simp_tac 
   1.274 +              (!simpset addsimps [insert_absorb]
   1.275 +                        setloop split_tac [expand_if]));
   1.276 +
   1.277 +(*If A sends ClientCertKeyEx to an honest agent B, then M will stay secret.*)
   1.278 +goal thy 
   1.279 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |] ==> \
   1.280 +\    Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.281 +\               Crypt KB (Nonce M)|} : set evs -->  \
   1.282 +\    Nonce M ~: analz (sees lost Spy evs)";
   1.283 +by (analz_induct_tac 1);
   1.284 +(*ClientHello*)
   1.285 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   1.286 +(*Fake*)
   1.287 +by (spy_analz_tac 1);
   1.288 +(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.289 +by (REPEAT (blast_tac (!claset addSEs partsEs
   1.290 +			       addDs  [impOfSubs analz_subset_parts,
   1.291 +				       Says_imp_sees_Spy' RS analz.Inj]) 1));
   1.292 +bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
   1.293 +
   1.294 +
   1.295 +(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   1.296 +
   1.297 +(*In fact, nothing of the form clientK(NA,NB,M) or serverK(NA,NB,M) is ever
   1.298 +  sent!  These two theorems are too strong: the Spy is quite capable of
   1.299 +  forming many items of the form serverK(NA,NB,M).
   1.300 +  Additional Fake rules could model this capability.*)
   1.301 +
   1.302 +goal thy 
   1.303 + "!!evs. evs : tls ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.304 +by (etac tls.induct 1);
   1.305 +by (prove_simple_subgoals_tac 1);
   1.306 +by (Fake_parts_insert_tac 1);
   1.307 +qed "clientK_notin_parts";
   1.308 +
   1.309 +goal thy 
   1.310 + "!!evs. evs : tls ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.311 +by (etac tls.induct 1);
   1.312 +by (prove_simple_subgoals_tac 1);
   1.313 +by (Fake_parts_insert_tac 1);
   1.314 +qed "serverK_notin_parts";
   1.315 +
   1.316 +(*We need a version of AddIffs that takes CONDITIONAL equivalences*)
   1.317 +val ths = [clientK_notin_parts, clientK_notin_parts RS not_parts_not_analz,
   1.318 +	   serverK_notin_parts, serverK_notin_parts RS not_parts_not_analz];
   1.319 +Addsimps ths;
   1.320 +AddSEs (ths RLN (2, [rev_notE]));
   1.321 +
   1.322 +
   1.323 +(*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   1.324 +     and has used the quoted values XA, XB, etc.  Note that it is up to A
   1.325 +     to compare XA with what she originally sent.
   1.326 +***)
   1.327 +
   1.328 +(*Perhaps A~=Spy is unnecessary, but there's no obvious proof if the first
   1.329 +  message is Fake.  We don't need guarantees for the Spy anyway.*)
   1.330 +goal thy 
   1.331 + "!!evs. [| X = Crypt (serverK(NA,NB,M))                        \
   1.332 +\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.333 +\                        Nonce NA, Agent XA, Agent A,           \
   1.334 +\                        Nonce NB, Agent XB,                    \
   1.335 +\                        Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
   1.336 +\           evs : tls;  A~=Spy;  B ~: lost |] ==>               \
   1.337 +\    Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   1.338 +\               Crypt KB (Nonce M)|} : set evs -->              \
   1.339 +\    X : parts (sees lost Spy evs) --> Says B A X : set evs";
   1.340 +by (Asm_simp_tac 1);
   1.341 +by (etac tls.induct 1);
   1.342 +by (ALLGOALS Asm_simp_tac);
   1.343 +by (Fake_parts_insert_tac 1);
   1.344 +(*ClientCertKeyEx*)
   1.345 +by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   1.346 +                       addSEs sees_Spy_partsEs) 1);
   1.347 +qed_spec_mp "TrustServerFinished";
   1.348 +
   1.349 +
   1.350 +(*** Protocol goal: if B receives CLIENT FINISHED, then A  is present ??
   1.351 +     and has used the quoted values XA, XB, etc.  Note that it is up to B
   1.352 +     to compare XB with what he originally sent. ***)
   1.353 +
   1.354 +(*This result seems far too strong--it may be provable because the current
   1.355 +  model gives the Spy access to NO keys of the form clientK(NA,NB,M).*)
   1.356 +goal thy 
   1.357 + "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.358 +\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.359 +\                        Nonce NA, Agent XA,                    \
   1.360 +\                        Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.361 +\                        Nonce NB, Agent XB, Agent B|});        \
   1.362 +\           evs : tls |] ==>               \
   1.363 +\    X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.364 +by (Asm_simp_tac 1);
   1.365 +by (etac tls.induct 1);
   1.366 +by (ALLGOALS Asm_simp_tac);
   1.367 +by (Blast_tac 1);
   1.368 +by (Fake_parts_insert_tac 1);
   1.369 +qed_spec_mp "TrustClientFinished";
   1.370 +
   1.371 +
   1.372 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Jul 01 11:11:42 1997 +0200
     2.3 @@ -0,0 +1,141 @@
     2.4 +(*  Title:      HOL/Auth/TLS
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1997  University of Cambridge
     2.8 +
     2.9 +Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
    2.10 +
    2.11 +An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
    2.12 +to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
    2.13 +global signing authority.
    2.14 +
    2.15 +A is the client and B is the server, not to be confused with the constant
    2.16 +Server, who is in charge of all public keys.
    2.17 +
    2.18 +The model assumes that no fraudulent certificates are present.
    2.19 +
    2.20 +Protocol goals: 
    2.21 +* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    2.22 +     parties (though A is not necessarily authenticated).
    2.23 +
    2.24 +* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
    2.25 +    message is optional!)
    2.26 +
    2.27 +* A upon receiving SERVER FINISHED knows that B is present
    2.28 +
    2.29 +* Each party who has received a FINISHED message can trust that the other
    2.30 +  party agrees on all message components, including XA and XB (thus foiling
    2.31 +  rollback attacks).
    2.32 +*)
    2.33 +
    2.34 +TLS = Public + 
    2.35 +
    2.36 +consts
    2.37 +  (*Client, server write keys.  They implicitly include the MAC secrets.*)
    2.38 +  clientK, serverK :: "nat*nat*nat => key"
    2.39 +
    2.40 +rules
    2.41 +  (*clientK is collision-free and makes symmetric keys*)
    2.42 +  inj_clientK   "inj clientK"	
    2.43 +  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    2.44 +
    2.45 +  inj_serverK   "inj serverK"	
    2.46 +  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
    2.47 +
    2.48 +  (*Spy has access to his own key for spoof messages, but Server is secure*)
    2.49 +  Spy_in_lost     "Spy: lost"
    2.50 +  Server_not_lost "Server ~: lost"
    2.51 +
    2.52 +
    2.53 +consts  lost :: agent set        (*No need for it to be a variable*)
    2.54 +	tls  :: event list set
    2.55 +
    2.56 +inductive tls
    2.57 +  intrs 
    2.58 +    Nil  (*Initial trace is empty*)
    2.59 +         "[]: tls"
    2.60 +
    2.61 +    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    2.62 +         "[| evs: tls;  B ~= Spy;  
    2.63 +             X: synth (analz (sees lost Spy evs)) |]
    2.64 +          ==> Says Spy B X  # evs : tls"
    2.65 +
    2.66 +    ClientHello
    2.67 +	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    2.68 +	   It is uninterpreted but will be confirmed in the FINISHED messages.
    2.69 +	   As an initial simplification, SESSION_ID is identified with NA
    2.70 +           and reuse of sessions is not supported.*)
    2.71 +         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
    2.72 +          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
    2.73 +
    2.74 +    ServerHello
    2.75 +         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    2.76 +	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    2.77 +	   implied and a SERVER CERTIFICATE is always present.*)
    2.78 +         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    2.79 +             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    2.80 +          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
    2.81 +			 Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
    2.82 +                # evs  :  tls"
    2.83 +
    2.84 +    ClientCertKeyEx
    2.85 +         (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
    2.86 +           Note that A encrypts using the supplied KB, not pubK B.*)
    2.87 +         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    2.88 +             Says B' A {|Nonce NA, Nonce NB, Agent XB,
    2.89 +			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
    2.90 +          ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
    2.91 +			 Crypt KB (Nonce M)|}
    2.92 +                # evs  :  tls"
    2.93 +
    2.94 +    CertVerify
    2.95 +	(*The optional CERTIFICATE VERIFY message contains the specific
    2.96 +          components listed in the security analysis, Appendix F.1.1.2.
    2.97 +          By checking the signature, B is assured of A's existence:
    2.98 +          the only use of A's certificate.*)
    2.99 +         "[| evs: tls;  A ~= B;  
   2.100 +             Says B' A {|Nonce NA, Nonce NB, Agent XB,
   2.101 +			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
   2.102 +          ==> Says A B (Crypt (priK A)
   2.103 +			(Hash{|Nonce NB,
   2.104 +	 		       Crypt (priK Server) {|Agent B, Key KB|}|}))
   2.105 +                # evs  :  tls"
   2.106 +
   2.107 +	(*Finally come the FINISHED messages, confirming XA and XB among
   2.108 +          other things.  The master-secret is the hash of NA, NB and M.
   2.109 +          Either party may sent its message first.*)
   2.110 +
   2.111 +    ClientFinished
   2.112 +         "[| evs: tls;  A ~= B;
   2.113 +	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
   2.114 +             Says B' A {|Nonce NA, Nonce NB, Agent XB, 
   2.115 +			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs;
   2.116 +             Says A  B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
   2.117 +		         Crypt KB (Nonce M)|} : set evs |]
   2.118 +          ==> Says A B (Crypt (clientK(NA,NB,M))
   2.119 +			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   2.120 +			       Nonce NA, Agent XA,
   2.121 +			       Crypt (priK Server) {|Agent A, Key(pubK A)|}, 
   2.122 +			       Nonce NB, Agent XB, Agent B|}))
   2.123 +                # evs  :  tls"
   2.124 +
   2.125 +	(*Keeping A' and A'' distinct means B cannot even check that the
   2.126 +          two messages originate from the same source.*)
   2.127 +
   2.128 +    ServerFinished
   2.129 +         "[| evs: tls;  A ~= B;
   2.130 +	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
   2.131 +	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
   2.132 +		 	  Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
   2.133 +	       : set evs;
   2.134 +	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
   2.135 +          ==> Says B A (Crypt (serverK(NA,NB,M))
   2.136 +			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   2.137 +			       Nonce NA, Agent XA, Agent A, 
   2.138 +			       Nonce NB, Agent XB,
   2.139 +			       Crypt (priK Server) {|Agent B, Key(pubK B)|}|}))
   2.140 +                # evs  :  tls"
   2.141 +
   2.142 +  (**Oops message??**)
   2.143 +
   2.144 +end