# HG changeset patch # User paulson # Date 868620601 -7200 # Node ID d8a71f6eaf40e424400359cec1bc965dc2e60dd5 # Parent eb16b8e8d87217f6798bd1d2b20c4e1c6902a70d Now uses the Notes constructor to distinguish the Client (who has chosen M) from the Spy (who may have replayed her messages) diff -r eb16b8e8d872 -r d8a71f6eaf40 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Jul 11 13:28:53 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Fri Jul 11 13:30:01 1997 +0200 @@ -3,15 +3,6 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory 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 he encrypts M with B's public key before sending -it. 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). @@ -84,9 +75,9 @@ by (Blast_tac 1); qed "clientK_neq_serverK"; -val ths = [pubK_neq_clientK, pubK_neq_serverK, - priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; -AddIffs (ths @ (ths RL [not_sym])); +val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, + priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; +AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); (**** Protocol Proofs ****) @@ -155,6 +146,7 @@ \ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; by (etac tls.induct 1); by (prove_simple_subgoals_tac 1); +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2); by (Fake_parts_insert_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; @@ -175,16 +167,56 @@ AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; +(*This lemma says that no false certificates exist. One might extend the + model to include bogus certificates for the lost agents, but there seems + little point in doing so: the loss of their private keys is a worse + breach of security.*) +goalw thy [certificate_def] + "!!evs. evs : tls \ +\ ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B"; +by (etac tls.induct 1); +by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]))); +by (Fake_parts_insert_tac 2); +by (Blast_tac 1); +bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp)); + + +(*Replace key KB in ClientCertKeyEx by (pubK B) *) +val ClientCertKeyEx_tac = + forward_tac [Says_imp_sees_Spy' RS parts.Inj RS + parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] + THEN' assume_tac + THEN' hyp_subst_tac; + +fun analz_induct_tac i = + etac tls.induct i THEN + ClientCertKeyEx_tac (i+7) THEN (*ClientFinished*) + ClientCertKeyEx_tac (i+6) THEN (*CertVerify*) + ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) + rewrite_goals_tac [certificate_def] THEN + ALLGOALS (asm_simp_tac + (!simpset addsimps [not_parts_not_analz] + setloop split_tac [expand_if])) THEN + (*Remove instances of pubK B: the Spy already knows all public keys. + Combining the two simplifier calls makes them run extremely slowly.*) + ALLGOALS (asm_simp_tac + (!simpset addsimps [insert_absorb] + setloop split_tac [expand_if])); + + +(*** Hashing of nonces ***) + (*Every Nonce that's hashed is already in past traffic. *) goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs); \ \ evs : tls |] \ \ ==> Nonce N : parts (sees lost Spy evs)"; by (etac rev_mp 1); by (etac tls.induct 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addSEs partsEs) 1); -by (Fake_parts_insert_tac 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] + setloop split_tac [expand_if]))); +by (Fake_parts_insert_tac 2); +by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addSEs partsEs) 1)); qed "Hash_imp_Nonce1"; (*Lemma needed to prove Hash_Hash_imp_Nonce*) @@ -194,23 +226,36 @@ \ ==> Nonce M : parts (sees lost Spy evs)"; by (etac rev_mp 1); by (etac tls.induct 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addSEs partsEs) 1); -by (Fake_parts_insert_tac 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] + setloop split_tac [expand_if]))); +by (Fake_parts_insert_tac 2); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addSEs partsEs) 1); qed "Hash_imp_Nonce2"; AddSDs [Hash_imp_Nonce2]; + +goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \ +\ ==> Crypt (pubK B) X : parts (sees lost Spy evs)"; +by (etac rev_mp 1); +by (analz_induct_tac 1); +by (blast_tac (!claset addIs [parts_insertI]) 1); +qed "Notes_Crypt_parts_sees"; + + +(*NEEDED??*) goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |} \ \ : parts (sees lost Spy evs); \ \ evs : tls |] \ \ ==> Nonce M : parts (sees lost Spy evs)"; by (etac rev_mp 1); by (etac tls.induct 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] + setloop split_tac [expand_if]))); +by (Fake_parts_insert_tac 2); +by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, + Says_imp_sees_Spy' RS parts.Inj] addSEs partsEs) 1); -by (Fake_parts_insert_tac 1); qed "Hash_Hash_imp_Nonce"; @@ -223,8 +268,9 @@ \ ==> Nonce N : parts (sees lost Spy evs)"; by (etac rev_mp 1); by (etac tls.induct 1); -by (ALLGOALS Asm_simp_tac); -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); +by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, + Says_imp_sees_Spy' RS parts.Inj] addSEs partsEs) 1); by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees]))); by (Fake_parts_insert_tac 1); @@ -248,7 +294,7 @@ \ 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 (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); by (Fake_parts_insert_tac 1); (*ServerHello: nonce NB cannot be in X because it's fresh!*) by (blast_tac (!claset addSDs [Hash_imp_Nonce1] @@ -256,68 +302,19 @@ qed_spec_mp "TrustCertVerify"; +(*If CERTIFICATE VERIFY is present then A has chosen M.*) goal thy - "!!evs. [| evs : tls; A ~= Spy |] \ -\ ==> Says A B (Crypt (priK A) \ -\ (Hash{|Nonce NB, certificate B KB, Nonce M|})) : set evs \ -\ --> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} : set evs"; + "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|}) \ +\ : parts (sees lost Spy evs); \ +\ evs : tls; A ~: lost |] \ +\ ==> Notes A {|Agent B, Nonce M|} : set evs"; +be rev_mp 1; by (etac tls.induct 1); -by (ALLGOALS Asm_full_simp_tac); -bind_thm ("UseCertVerify", result() RSN (2, rev_mp)); - - -(*This lemma says that no false certificates exist. One might extend the - model to include bogus certificates for the lost agents, but there seems - little point in doing so: the loss of their private keys is a worse - breach of security.*) -goalw thy [certificate_def] - "!!evs. evs : tls \ -\ ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B"; -by (etac tls.induct 1); -by (ALLGOALS Asm_simp_tac); +by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]))); by (Fake_parts_insert_tac 2); by (Blast_tac 1); -bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp)); - - -(*Replace key KB in ClientCertKeyEx by (pubK B) *) -val ClientCertKeyEx_tac = - forward_tac [Says_imp_sees_Spy' RS parts.Inj RS - parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] - THEN' assume_tac - THEN' hyp_subst_tac; +qed "UseCertVerify"; -fun analz_induct_tac i = - etac tls.induct i THEN - ClientCertKeyEx_tac (i+5) THEN - ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz] - setloop split_tac [expand_if])) THEN - (*Remove instances of pubK B: the Spy already knows all public keys. - Combining the two simplifier calls makes them run extremely slowly.*) - ALLGOALS (asm_simp_tac - (!simpset addsimps [insert_absorb] - setloop split_tac [expand_if])); - -(*** 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 @@ -325,7 +322,9 @@ \ 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)); +by (ALLGOALS + (asm_simp_tac (analz_image_keys_ss + addsimps (certificate_def::keys_distinct)))); (*Fake*) by (spy_analz_tac 2); (*Base*) @@ -349,11 +348,14 @@ 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]))); +by (REPEAT_FIRST (rtac lemma)); +writeln"SLOW simplification: 50 secs!??"; +by (ALLGOALS + (asm_simp_tac (analz_image_keys_ss + addsimps (analz_image_priK::certificate_def:: + keys_distinct)))); +by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*) by (Blast_tac 3); (*Fake*) @@ -363,33 +365,37 @@ 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.*) -goalw thy [certificate_def] - "!!evs. [| evs : tls; A~=Spy; B ~: lost |] \ -\ ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \ -\ : set evs --> Nonce M ~: analz (sees lost Spy evs)"; +(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*) +goal thy + "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ +\ ==> Notes A {|Agent B, 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) 3); +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] + 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*) by (REPEAT (blast_tac (!claset addSEs partsEs - addDs [impOfSubs analz_subset_parts, + addDs [Notes_Crypt_parts_sees, + impOfSubs analz_subset_parts, Says_imp_sees_Spy' RS analz.Inj]) 1)); bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp)); (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***) -(*The two proofs are identical*) +(** First, some lemmas about those write keys. The proofs for serverK are + nearly identical to those for clientK. **) + +(*Lemma: those write keys are never sent if M is secure. + Converse doesn't hold; betraying M doesn't force the keys to be sent!*) + goal thy - "!!evs. [| Nonce M ~: analz (sees lost Spy evs); \ -\ evs : tls |] \ + "!!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); @@ -402,9 +408,11 @@ by (Blast_tac 1); qed "clientK_notin_parts"; +Addsimps [clientK_notin_parts]; +AddSEs [clientK_notin_parts RSN (2, rev_notE)]; + goal thy - "!!evs. [| Nonce M ~: analz (sees lost Spy evs); \ -\ evs : tls |] \ + "!!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); @@ -417,65 +425,198 @@ by (Blast_tac 1); qed "serverK_notin_parts"; +Addsimps [serverK_notin_parts]; +AddSEs [serverK_notin_parts RSN (2, rev_notE)]; + +(*Lemma: those write keys are never used if M is fresh. + Converse doesn't hold; betraying M doesn't force the keys to be sent! + NOT suitable as safe elim rules.*) + +goal thy + "!!evs. [| Nonce M ~: used evs; evs : tls |] \ +\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)"; +by (etac rev_mp 1); +by (analz_induct_tac 1); +(*ClientFinished: since M is fresh, a different instance of clientK was used.*) +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] + addSEs sees_Spy_partsEs) 3); +by (Fake_parts_insert_tac 2); +(*Base*) +by (Blast_tac 1); +qed "Crypt_clientK_notin_parts"; + +Addsimps [Crypt_clientK_notin_parts]; +AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)]; + +goal thy + "!!evs. [| Nonce M ~: used evs; evs : tls |] \ +\ ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)"; +by (etac rev_mp 1); +by (analz_induct_tac 1); +(*ServerFinished: since M is fresh, a different instance of serverK was used.*) +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] + addSEs sees_Spy_partsEs) 3); +by (Fake_parts_insert_tac 2); +(*Base*) +by (Blast_tac 1); +qed "Crypt_serverK_notin_parts"; + +Addsimps [Crypt_serverK_notin_parts]; +AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)]; + + +(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*) +goal thy + "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs; \ +\ A ~: lost; evs : tls |] ==> KB = pubK B"; +be rev_mp 1; +by (analz_induct_tac 1); +qed "A_Crypt_pubB"; + + +(*** Unicity results for M, the pre-master-secret ***) + +(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ... + It simplifies the proof by discarding needless information about + analz (insert X (sees lost Spy evs)) +*) +fun analz_mono_parts_induct_tac i = + etac tls.induct i THEN + ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) + REPEAT_FIRST analz_mono_contra_tac; + + +(*M determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) +goal thy + "!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \ +\ ==> EX B'. ALL B. \ +\ Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'"; +by (etac rev_mp 1); +by (analz_mono_parts_induct_tac 1); +by (prove_simple_subgoals_tac 1); +by (asm_simp_tac (!simpset addsimps [all_conj_distrib] + setloop split_tac [expand_if]) 2); +(*ClientCertKeyEx*) +by (expand_case_tac "M = ?y" 2 THEN + REPEAT (blast_tac (!claset addSEs partsEs) 2)); +by (Fake_parts_insert_tac 1); +val lemma = result(); + +goal thy + "!!evs. [| Crypt(pubK B) (Nonce M) : parts (sees lost Spy evs); \ +\ Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \ +\ Nonce M ~: analz (sees lost Spy evs); \ +\ evs : tls |] \ +\ ==> B=B'"; +by (prove_unique_tac lemma 1); +qed "unique_M"; + + +(*In A's note to herself, M determines A and B.*) +goal thy + "!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \ +\ ==> EX A' B'. ALL A B. \ +\ Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'"; +by (etac rev_mp 1); +by (analz_mono_parts_induct_tac 1); +by (prove_simple_subgoals_tac 1); +by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); +(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*) +by (expand_case_tac "M = ?y" 1 THEN + blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1); +val lemma = result(); + +goal thy + "!!evs. [| Notes A {|Agent B, Nonce M|} : set evs; \ +\ Notes A' {|Agent B', Nonce M|} : set evs; \ +\ Nonce M ~: analz (sees lost Spy evs); \ +\ evs : tls |] \ +\ ==> A=A' & B=B'"; +by (prove_unique_tac lemma 1); +qed "Notes_unique_M"; + + (*** 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. ***) -goalw thy [certificate_def] - "!!evs. [| X = Crypt (serverK(NA,NB,M)) \ -\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ -\ Nonce NA, Agent XA, Agent A, \ +(*The mention of her name (A) in X assumes A that B knows who she is.*) +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, certificate B (pubK B)|}); \ -\ evs : tls; A~=Spy; B ~: lost |] \ -\ ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \ -\ : set evs --> \ +\ evs : tls; A ~: lost; B ~: lost |] \ +\ ==> Notes A {|Agent B, 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); +by (analz_induct_tac 1); +by (REPEAT_FIRST (rtac impI)); (*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); qed_spec_mp "TrustServerFinished"; -(*** Protocol goal: if B receives CLIENT FINISHED, then A has used the - quoted values XA, XB, etc., which B can then check. BUT NOTE: - B has no way of knowing that A is the sender of CLIENT CERTIFICATE! +(*This version refers not to SERVER FINISHED but to any message from B. + We don't assume B has received CERTIFICATE VERIFY, and an intruder could + have changed A's identity in all other messages, so we can't be sure + that B sends his message to A.*) +goal thy + "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ +\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ +\ Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs) --> \ +\ (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)"; +by (analz_induct_tac 1); +by (REPEAT_FIRST (rtac impI)); +(*Fake: the Spy doesn't have the critical session key!*) +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, + not_parts_not_analz]) 2); +by (Fake_parts_insert_tac 1); +(*ServerFinished. If the message is old then apply induction hypothesis...*) +by (rtac conjI 1 THEN Blast_tac 2); +(*...otherwise delete induction hyp and use unicity of M.*) +by (thin_tac "?PP-->?QQ" 1); +by (Step_tac 1); +by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); +by (blast_tac (!claset addSEs [MPair_parts] + addDs [Notes_Crypt_parts_sees, + Says_imp_sees_Spy' RS parts.Inj, + unique_M]) 1); +qed_spec_mp "TrustServerMsg"; + + +(*** Protocol goal: if B receives any message encrypted with clientK + then A has sent it, ASSUMING that A chose M. Authentication is + assumed here; B cannot verify it. But if the message is + CLIENT FINISHED, then B can then check the quoted values XA, XB, etc. ***) -goalw thy [certificate_def] - "!!evs. [| X = Crypt (clientK(NA,NB,M)) \ -\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ -\ Nonce NA, Agent XA, \ -\ certificate A (pubK A), \ -\ Nonce NB, Agent XB, Agent B|}); \ -\ evs : tls; A~=Spy; B ~: lost |] \ -\ ==> Says A B {|certificate A (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); -(*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); +goal thy + "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ +\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ +\ Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) --> \ +\ Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; +by (analz_induct_tac 1); +by (REPEAT_FIRST (rtac impI)); (*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"; +(*ClientFinished. If the message is old then apply induction hypothesis...*) +by (step_tac (!claset delrules [conjI]) 1); +by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); +by (blast_tac (!claset addSEs [MPair_parts] + addDs [Notes_unique_M]) 1); +qed_spec_mp "TrustClientMsg"; (*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to @@ -483,22 +624,14 @@ values XA, XB, etc. Even this one requires A to be uncompromised. ***) goal thy - "!!evs. [| X = Crypt (clientK(NA,NB,M)) \ -\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ -\ Nonce NA, Agent XA, \ -\ certificate A (pubK A), \ -\ Nonce NB, Agent XB, Agent B|}); \ -\ Says A' B X : set evs; \ -\ Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \ -\ : set evs; \ -\ Says A'' B (Crypt (priK A) \ -\ (Hash{|Nonce NB, certificate B KB, Nonce M|})) \ -\ : set evs; \ -\ evs : tls; A ~: lost; B ~: lost |] \ -\ ==> Says A B X : set evs"; -br TrustClientFinished 1; -br (TrustCertVerify RS UseCertVerify) 5; -by (REPEAT_FIRST (ares_tac [refl])); -by (ALLGOALS - (asm_full_simp_tac (!simpset addsimps [Says_imp_sees_Spy RS parts.Inj]))); -qed_spec_mp "AuthClientFinished"; + "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs; \ +\ Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \ +\ : set evs; \ +\ Says A'' B (Crypt (priK A) \ +\ (Hash{|Nonce NB, certificate B KB, Nonce M|})) \ +\ : set evs; \ +\ evs : tls; A ~: lost; B ~: lost |] \ +\ ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; +by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] + addDs [Says_imp_sees_Spy RS parts.Inj]) 1); +qed "AuthClientFinished"; diff -r eb16b8e8d872 -r d8a71f6eaf40 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Fri Jul 11 13:28:53 1997 +0200 +++ b/src/HOL/Auth/TLS.thy Fri Jul 11 13:30:01 1997 +0200 @@ -18,6 +18,19 @@ 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 + +NOTE. The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx, +CertVerify, ClientFinished to record that A knows M. It is a note from A to +herself. Nobody else can see it. In ClientCertKeyEx, the Spy can substitute +his own certificate for A's, but he cannot replace A's note by one for himself. + +The note is needed because of a weakness in the public-key model. Each +agent's state is recorded as the trace of messages. When the true client (A) +invents M, he encrypts M with B's public key before sending it. The model +does not distinguish the original occurrence of such a message from a replay. + +In the shared-key model, the ability to encrypt implies the ability to +decrypt, so the problem does not arise. *) TLS = Public + @@ -77,7 +90,7 @@ ServerHello (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. - Na is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is + NA is returned in its role as SESSION_ID. A CERTIFICATE_REQUEST is implied and a SERVER CERTIFICATE is always present.*) "[| evs: tls; A ~= B; Nonce NB ~: used evs; Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |] @@ -86,13 +99,16 @@ # evs : tls" ClientCertKeyEx - (*CLIENT CERTIFICATE and KEY EXCHANGE. M is the pre-master-secret. - Note that A encrypts using the supplied KB, not pubK B.*) + (*CLIENT CERTIFICATE and KEY EXCHANGE. The client, A, chooses M, + the pre-master-secret. She encrypts M using the supplied KB, + which ought to be pubK B, and also with her own public key, + to record in the trace that she knows M (see NOTE at top).*) "[| evs: tls; A ~= B; Nonce M ~: used evs; Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} : set evs |] ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} - # evs : tls" + # Notes A {|Agent B, Nonce M|} + # evs : tls" CertVerify (*The optional CERTIFICATE VERIFY message contains the specific @@ -102,8 +118,7 @@ "[| evs: tls; A ~= B; Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} : set evs; - Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} - : set evs |] + Notes A {|Agent B, Nonce M|} : set evs |] ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})) # evs : tls" @@ -112,13 +127,18 @@ other things. The master-secret is the hash of NA, NB and M. Either party may sent its message first.*) + (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the + rule's applying when the Spy has satisfied the "Says A B" by + repaying messages sent by the true client; in that case, the + Spy does not know M and could not sent CLIENT FINISHED. One + could simply put A~=Spy into the rule, but one should not + expect the spy to be well-behaved.*) ClientFinished "[| evs: tls; A ~= B; Says A B {|Agent A, Nonce NA, Agent XA|} : set evs; Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} : set evs; - Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} - : set evs |] + Notes A {|Agent B, Nonce M|} : set evs |] ==> Says A B (Crypt (clientK(NA,NB,M)) (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, Nonce NA, Agent XA, @@ -127,15 +147,16 @@ # evs : tls" (*Keeping A' and A'' distinct means B cannot even check that the - two messages originate from the same source.*) - + two messages originate from the same source. B does not attempt + to read A's encrypted "note to herself".*) ServerFinished "[| evs: tls; A ~= B; Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs; Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B (pubK B)|} : set evs; - Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |] + Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|} + : set evs |] ==> Says B A (Crypt (serverK(NA,NB,M)) (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, Nonce NA, Agent XA, Agent A,