3474

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 publickey 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 keygenerating 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 strongit 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 
