# HG changeset patch # User paulson # Date 867771462 -7200 # Node ID d59bbf0532580d493b7d62d723c09822667db023 # Parent 2aacd6f106545db4b7882746d0368a51216b4687 More realistic model: the Spy can compute clientK and serverK diff -r 2aacd6f10654 -r d59bbf053258 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Tue Jul 01 17:36:42 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Tue Jul 01 17:37:42 1997 +0200 @@ -4,17 +4,36 @@ Copyright 1997 University of Cambridge The public-key model has a weakness, especially concerning anonymous sessions. -The Spy's state is recorded as the trace of message. But if he himself is -the Client and invents M, then the event he sends contains M encrypted with B's -public key. From the trace there is no reason to believe that the spy knows -M, and yet the spy actually chose M! So, in any property concerning the -secrecy of some item, one must somehow establish that the spy didn't choose -the item. In practice, this weakness does little harm, since one can expect -few guarantees when communicating directly with an enemy. +The Spy's state is recorded as the trace of message. But if he himself is the +Client and invents M, then he sends contains M encrypted with B's public key. +This message gives no evidence that the spy knows M, and yet the spy actually +chose M! So, in any property concerning the secrecy of some item, one must +establish that the spy didn't choose the item. Guarantees normally assume +that the other party is uncompromised (otherwise, one can prove little). + +Protocol goals: +* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two + parties (though A is not necessarily authenticated). + +* B upon receiving CERTIFICATE VERIFY knows that A is present (But this + message is optional!) -The model, at present, doesn't recognize that if the Spy has NA, NB and M then -he also has clientK(NA,NB,M) and serverK(NA,NB,M). Maybe this doesn't really -matter, since one can prove that he doesn't get M. +* A upon receiving SERVER FINISHED knows that B is present + +* Each party who has received a FINISHED message can trust that the other + party agrees on all message components, including XA and XB (thus foiling + rollback attacks). + +A curious property found in these proofs is that CERTIFICATE VERIFY actually +gives weaker authentication than CLIENT FINISHED. The theorem for CERTIFICATE +VERIFY is subject to A~:lost, since if A's private key is known to the spy +then he can forge A's signature. But the theorem for CLIENT FINISHED merely +assumes that A is not the spy himself, since the model assumes that all other +agents tell the truth. + +In the real world, there are agents who are not active attackers, and yet +still cannot be trusted to identify themselves. There may well be more such +agents than there are compromised private keys. *) open TLS; @@ -24,13 +43,18 @@ AddIffs [Spy_in_lost, Server_not_lost]; +goal thy "!!A. A ~: lost ==> A ~= Spy"; +by (Blast_tac 1); +qed "not_lost_not_eq_Spy"; +Addsimps [not_lost_not_eq_Spy]; + (*Injectiveness of key-generating functions*) AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq]; (* invKey(clientK x) = clientK x and similarly for serverK*) Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK, isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK]; - + (*Replacing the variable by a constant improves search speed by 50%!*) val Says_imp_sees_Spy' = @@ -63,8 +87,14 @@ by (Full_simp_tac 1); qed "priK_neq_serverK"; +(*clientK and serverK have disjoint ranges*) +goal thy "clientK arg ~= serverK arg'"; +by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1); +by (Blast_tac 1); +qed "clientK_neq_serverK"; + val ths = [pubK_neq_clientK, pubK_neq_serverK, - priK_neq_clientK, priK_neq_serverK]; + priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; AddIffs (ths @ (ths RL [not_sym])); @@ -218,7 +248,8 @@ (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***) (*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first - message is Fake. We don't need guarantees for the Spy anyway.*) + message is Fake. We don't need guarantees for the Spy anyway. We must + assume A~:lost; otherwise, the Spy can forge A's signature.*) goal thy "!!evs. [| X = Crypt (priK A) \ \ (Hash{|Nonce NB, \ @@ -227,11 +258,11 @@ \ ==> Says B A {|Nonce NA, Nonce NB, Agent XB, \ \ Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \ \ X : parts (sees lost Spy evs) --> Says A B X : set evs"; -by (Asm_simp_tac 1); +by (hyp_subst_tac 1); by (etac tls.induct 1); by (ALLGOALS Asm_simp_tac); by (Fake_parts_insert_tac 1); -(*ServerHello*) +(*ServerHello: nonce NB cannot be in X because it's fresh!*) by (blast_tac (!claset addSDs [Hash_imp_Nonce1] addSEs sees_Spy_partsEs) 1); qed_spec_mp "TrustCertVerify"; @@ -261,7 +292,7 @@ fun analz_induct_tac i = etac tls.induct i THEN - ClientCertKeyEx_tac (i+4) THEN + ClientCertKeyEx_tac (i+5) THEN ALLGOALS (asm_simp_tac (!simpset addsimps [not_parts_not_analz] setloop split_tac [expand_if])) THEN @@ -271,15 +302,83 @@ (!simpset addsimps [insert_absorb] setloop split_tac [expand_if])); -(*If A sends ClientCertKeyEx to an honest agent B, then M will stay secret.*) +(*** Specialized rewriting for the analz_image_... theorems ***) + +goal thy "insert (Key K) H = Key `` {K} Un H"; +by (Blast_tac 1); +qed "insert_Key_singleton"; + +goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; +by (Blast_tac 1); +qed "insert_Key_image"; + +(*Reverse the normal simplification of "image" to build up (not break down) + the set of keys. Based on analz_image_freshK_ss, but simpler.*) +val analz_image_keys_ss = + !simpset delsimps [image_insert, image_Un] + addsimps [image_insert RS sym, image_Un RS sym, + rangeI, + insert_Key_singleton, + insert_Key_image, Un_assoc RS sym] + setloop split_tac [expand_if]; + +(*No collection of keys can help the spy get new private keys*) +goal thy + "!!evs. evs : tls ==> \ +\ ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (priK B : KK | B : lost)"; +by (etac tls.induct 1); +by (ALLGOALS (asm_simp_tac analz_image_keys_ss)); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); +qed_spec_mp "analz_image_priK"; + + +(*Lemma for the trivial direction of the if-and-only-if*) +goal thy + "!!evs. (X : analz (G Un H)) --> (X : analz H) ==> \ +\ (X : analz (G Un H)) = (X : analz H)"; +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); +val lemma = result(); + +(*Knowing some clientKs and serverKs is no help in getting new nonces*) +goal thy + "!!evs. evs : tls ==> \ +\ ALL KK. KK <= (range clientK Un range serverK) --> \ +\ (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (Nonce N : analz (sees lost Spy evs))"; +by (etac tls.induct 1); +by (ClientCertKeyEx_tac 6); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac lemma )); + (*SLOW: 30s!*) +by (ALLGOALS (asm_simp_tac analz_image_keys_ss)); +by (ALLGOALS (asm_simp_tac + (!simpset addsimps [analz_image_priK, insert_absorb]))); +(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*) +by (Blast_tac 3); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); +qed_spec_mp "analz_image_keys"; + + +(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret. + The assumption is A~=Spy, not A~:lost, since A doesn't use her private key + here.*) goal thy - "!!evs. [| evs : tls; A ~: lost; B ~: lost |] ==> \ -\ Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ -\ Crypt KB (Nonce M)|} : set evs --> \ -\ Nonce M ~: analz (sees lost Spy evs)"; + "!!evs. [| evs : tls; A~=Spy; B ~: lost |] \ +\ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ +\ Crypt KB (Nonce M)|} : set evs --> \ +\ Nonce M ~: analz (sees lost Spy evs)"; by (analz_induct_tac 1); (*ClientHello*) -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); +(*SpyKeys*) +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); (*Fake*) by (spy_analz_tac 1); (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) @@ -291,79 +390,96 @@ (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***) -(*In fact, nothing of the form clientK(NA,NB,M) or serverK(NA,NB,M) is ever - sent! These two theorems are too strong: the Spy is quite capable of - forming many items of the form serverK(NA,NB,M). - Additional Fake rules could model this capability.*) - +(*The two proofs are identical*) goal thy - "!!evs. evs : tls ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)"; -by (etac tls.induct 1); -by (prove_simple_subgoals_tac 1); -by (Fake_parts_insert_tac 1); + "!!evs. [| Nonce M ~: analz (sees lost Spy evs); \ +\ evs : tls |] \ +\ ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)"; +by (etac rev_mp 1); +by (analz_induct_tac 1); +(*SpyKeys*) +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); qed "clientK_notin_parts"; goal thy - "!!evs. evs : tls ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)"; -by (etac tls.induct 1); -by (prove_simple_subgoals_tac 1); -by (Fake_parts_insert_tac 1); + "!!evs. [| Nonce M ~: analz (sees lost Spy evs); \ +\ evs : tls |] \ +\ ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)"; +by (etac rev_mp 1); +by (analz_induct_tac 1); +(*SpyKeys*) +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); qed "serverK_notin_parts"; -(*We need a version of AddIffs that takes CONDITIONAL equivalences*) -val ths = [clientK_notin_parts, clientK_notin_parts RS not_parts_not_analz, - serverK_notin_parts, serverK_notin_parts RS not_parts_not_analz]; -Addsimps ths; -AddSEs (ths RLN (2, [rev_notE])); - (*** Protocol goals: if A receives SERVER FINISHED, then B is present and has used the quoted values XA, XB, etc. Note that it is up to A to compare XA with what she originally sent. ***) -(*Perhaps A~=Spy is unnecessary, but there's no obvious proof if the first - message is Fake. We don't need guarantees for the Spy anyway.*) goal thy - "!!evs. [| X = Crypt (serverK(NA,NB,M)) \ -\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ -\ Nonce NA, Agent XA, Agent A, \ -\ Nonce NB, Agent XB, \ + "!!evs. [| X = Crypt (serverK(NA,NB,M)) \ +\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ +\ Nonce NA, Agent XA, Agent A, \ +\ Nonce NB, Agent XB, \ \ Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \ -\ evs : tls; A~=Spy; B ~: lost |] ==> \ -\ Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ -\ Crypt KB (Nonce M)|} : set evs --> \ -\ X : parts (sees lost Spy evs) --> Says B A X : set evs"; -by (Asm_simp_tac 1); +\ evs : tls; A~=Spy; B ~: lost |] \ +\ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ +\ Crypt KB (Nonce M)|} : set evs --> \ +\ X : parts (sees lost Spy evs) --> Says B A X : set evs"; +by (hyp_subst_tac 1); by (etac tls.induct 1); by (ALLGOALS Asm_simp_tac); +(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*) +by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce] + addSEs sees_Spy_partsEs) 2); +(*Fake: the Spy doesn't have the critical session key!*) +by (REPEAT (rtac impI 1)); +by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, + serverK_notin_parts, + not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); -(*ClientCertKeyEx*) -by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce] - addSEs sees_Spy_partsEs) 1); qed_spec_mp "TrustServerFinished"; -(*** Protocol goal: if B receives CLIENT FINISHED, then A is present ?? +(*** Protocol goal: if B receives CLIENT FINISHED, then A is present and has used the quoted values XA, XB, etc. Note that it is up to B to compare XB with what he originally sent. ***) -(*This result seems far too strong--it may be provable because the current - model gives the Spy access to NO keys of the form clientK(NA,NB,M).*) +(*This result seems too strong: A need not have sent CERTIFICATE VERIFY. + But we assume (as always) that the other party is honest...*) goal thy "!!evs. [| X = Crypt (clientK(NA,NB,M)) \ \ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ \ Nonce NA, Agent XA, \ \ Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ \ Nonce NB, Agent XB, Agent B|}); \ -\ evs : tls |] ==> \ -\ X : parts (sees lost Spy evs) --> Says A B X : set evs"; -by (Asm_simp_tac 1); +\ evs : tls; A~=Spy; B ~: lost |] \ +\ ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \ +\ Crypt KB (Nonce M)|} : set evs --> \ +\ X : parts (sees lost Spy evs) --> Says A B X : set evs"; +by (hyp_subst_tac 1); by (etac tls.induct 1); by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); +(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*) +by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce] + addSEs sees_Spy_partsEs) 2); +(*Fake: the Spy doesn't have the critical session key!*) +by (REPEAT (rtac impI 1)); +by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, + clientK_notin_parts, + not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); qed_spec_mp "TrustClientFinished"; - - - diff -r 2aacd6f10654 -r d59bbf053258 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Tue Jul 01 17:36:42 1997 +0200 +++ b/src/HOL/Auth/TLS.thy Tue Jul 01 17:37:42 1997 +0200 @@ -12,20 +12,12 @@ A is the client and B is the server, not to be confused with the constant Server, who is in charge of all public keys. -The model assumes that no fraudulent certificates are present. - -Protocol goals: -* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two - parties (though A is not necessarily authenticated). +The model assumes that no fraudulent certificates are present, but it does +assume that some private keys are lost to the spy. -* B upon receiving CERTIFICATE VERIFY knows that A is present (But this - message is optional!) - -* A upon receiving SERVER FINISHED knows that B is present - -* Each party who has received a FINISHED message can trust that the other - party agrees on all message components, including XA and XB (thus foiling - rollback attacks). +Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher +Allen, Transport Layer Security Working Group, 21 May 1997, +INTERNET-DRAFT draft-ietf-tls-protocol-03.txt *) TLS = Public + @@ -39,9 +31,13 @@ inj_clientK "inj clientK" isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) + (*serverK is similar*) inj_serverK "inj serverK" isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) + (*Clashes with pubK and priK are impossible, but this axiom is needed.*) + clientK_range "range clientK <= Compl (range serverK)" + (*Spy has access to his own key for spoof messages, but Server is secure*) Spy_in_lost "Spy: lost" Server_not_lost "Server ~: lost" @@ -58,7 +54,13 @@ Fake (*The spy, an active attacker, MAY say anything he CAN say.*) "[| evs: tls; B ~= Spy; X: synth (analz (sees lost Spy evs)) |] - ==> Says Spy B X # evs : tls" + ==> Says Spy B X # evs : tls" + + SpyKeys (*The spy may apply clientK & serverK to nonces he's found*) + "[| evs: tls; + Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |] + ==> Says Spy B {| Key (clientK(NA,NB,M)), + Key (serverK(NA,NB,M)) |} # evs : tls" ClientHello (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.