# HG changeset patch # User paulson # Date 875867570 -7200 # Node ID 6ee707a73248772661c2a9561c36c2ec35db05f0 # Parent ede66fb9988049c6932ffe7183b76f9bc16c40d5 Routine tidying up diff -r ede66fb99880 -r 6ee707a73248 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Thu Oct 02 22:54:00 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Fri Oct 03 10:32:50 1997 +0200 @@ -23,30 +23,8 @@ proof_timing:=true; HOL_quantifiers := false; -(** We mostly DO NOT unfold the definition of "certificate". The attached - lemmas unfold it lazily, when "certificate B KB" occurs in appropriate - contexts. -**) - -goalw thy [certificate_def] - "parts (insert (certificate B KB) H) = \ -\ parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)"; -by (rtac refl 1); -qed "parts_insert_certificate"; - -goalw thy [certificate_def] - "analz (insert (certificate B KB) H) = \ -\ analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)"; -by (rtac refl 1); -qed "analz_insert_certificate"; -Addsimps [parts_insert_certificate, analz_insert_certificate]; - -goalw thy [certificate_def] - "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)"; -by (Blast_tac 1); -qed "eq_certificate_iff"; -AddIffs [eq_certificate_iff]; - +(*Automatically unfold the definition of "certificate"*) +Addsimps [certificate_def]; (*Injectiveness of key-generating functions*) AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq]; @@ -75,15 +53,14 @@ (**** Protocol Proofs ****) -(*A "possibility property": there are traces that reach the end. - This protocol has three end points and six messages to consider.*) +(*Possibility properties state that some traces run the protocol to the end. + Four paths and 12 rules are considered.*) -(** These proofs make the further assumption that the Nonce_supply nonces +(** These proofs assume that the Nonce_supply nonces (which have the form @ N. Nonce N ~: used evs) - lie outside the range of PRF. This assumption seems reasonable, but - as it is needed only for the possibility theorems, it is not taken - as an axiom. + lie outside the range of PRF. It seems reasonable, but as it is needed + only for the possibility theorems, it is not taken as an axiom. **) @@ -202,15 +179,17 @@ 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 (spies evs) --> KB = pubK B"; + "!!evs. [| certificate B KB : parts (spies evs); evs : tls |] \ +\ ==> pubK B = KB"; +by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp)); +qed "certificate_valid"; (*Replace key KB in ClientKeyExch by (pubK B) *) val ClientKeyExch_tac = - forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB] + forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid] THEN' assume_tac THEN' hyp_subst_tac; @@ -268,9 +247,9 @@ (*B can check A's signature if he has received A's certificate.*) goal thy - "!!evs. [| X : parts (spies evs); \ -\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ -\ evs : tls; A ~: bad |] \ + "!!evs. [| X : parts (spies evs); \ +\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ +\ evs : tls; A ~: bad |] \ \ ==> Says A B X : set evs"; by (etac rev_mp 1); by (hyp_subst_tac 1); @@ -280,20 +259,20 @@ (*Final version: B checks X using the distributed KA instead of priK A*) goal thy - "!!evs. [| X : parts (spies evs); \ -\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ -\ certificate A KA : parts (spies evs); \ -\ evs : tls; A ~: bad |] \ + "!!evs. [| X : parts (spies evs); \ +\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ +\ certificate A KA : parts (spies evs); \ +\ evs : tls; A ~: bad |] \ \ ==> Says A B X : set evs"; -by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1); +by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1); qed "TrustCertVerify"; (*If CertVerify is present then A has chosen PMS.*) goal thy - "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \ -\ : parts (spies evs); \ -\ evs : tls; A ~: bad |] \ + "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \ +\ : parts (spies evs); \ +\ evs : tls; A ~: bad |] \ \ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; be rev_mp 1; by (parts_induct_tac 1); @@ -302,83 +281,15 @@ (*Final version using the distributed KA instead of priK A*) goal thy - "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \ -\ : parts (spies evs); \ -\ certificate A KA : parts (spies evs); \ -\ evs : tls; A ~: bad |] \ + "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \ +\ : parts (spies evs); \ +\ certificate A KA : parts (spies evs); \ +\ evs : tls; A ~: bad |] \ \ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; -by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1); +by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1); qed "UseCertVerify"; -(*Key compromise lemma needed to prove analz_image_keys. - 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 (spies evs))) = \ -\ (priK B : KK | B : bad)"; -by (etac tls.induct 1); -by (ALLGOALS - (asm_simp_tac (analz_image_keys_ss - addsimps (analz_insert_certificate::keys_distinct)))); -(*Fake*) -by (spy_analz_tac 2); -(*Base*) -by (Blast_tac 1); -qed_spec_mp "analz_image_priK"; - - -(*slightly speeds up the big simplification below*) -goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK"; -by (Blast_tac 1); -val range_sessionkeys_not_priK = result(); - -(*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(); - -(** It is a mystery to me why the following formulation is actually slower - in simplification: - -\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ -\ (Nonce N : analz (spies evs))"; - -More so as it can take advantage of unconditional rewrites such as - priK B ~: sessionK``Z -**) - -goal thy - "!!evs. evs : tls ==> \ -\ ALL KK. KK <= range sessionK --> \ -\ (Nonce N : analz (Key``KK Un (spies evs))) = \ -\ (Nonce N : analz (spies evs))"; -by (etac tls.induct 1); -by (ClientKeyExch_tac 7); -by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac lemma)); -by (ALLGOALS (*23 seconds*) - (asm_simp_tac (analz_image_keys_ss - addsimps [range_sessionkeys_not_priK, - analz_image_priK, analz_insert_certificate]))); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); -(*Fake*) -by (spy_analz_tac 2); -(*Base*) -by (Blast_tac 1); -qed_spec_mp "analz_image_keys"; - -(*Knowing some session keys is no help in getting new nonces*) -goal thy - "!!evs. evs : tls ==> \ -\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ -\ (Nonce N : analz (spies evs))"; -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); -qed "analz_insert_key"; -Addsimps [analz_insert_key]; - goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs"; by (parts_induct_tac 1); (*ClientKeyExch: PMS is assumed to differ from any PRF.*) @@ -402,75 +313,6 @@ -(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***) - -(** Some lemmas about session keys, comprising clientK and serverK **) - - -(*Lemma: session keys are never used if PMS is fresh. - Nonces don't have to agree, allowing session resumption. - Converse doesn't hold; revealing PMS doesn't force the keys to be sent. - THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*) -goal thy - "!!evs. [| Nonce PMS ~: parts (spies evs); \ -\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \ -\ evs : tls |] \ -\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; -by (etac rev_mp 1); -by (hyp_subst_tac 1); -by (analz_induct_tac 1); -(*SpyKeys*) -by (blast_tac (!claset addSEs spies_partsEs) 3); -(*Fake*) -by (simp_tac (!simpset addsimps [parts_insert_spies]) 2); -by (Fake_parts_insert_tac 2); -(** LEVEL 6 **) -(*Oops*) -by (fast_tac (!claset addSEs [MPair_parts] - addDs [Says_imp_spies RS parts.Inj] - addss (!simpset)) 6); -by (REPEAT - (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, - Notes_master_imp_Crypt_PMS] - addSEs spies_partsEs) 1)); -val lemma = result(); - -goal thy - "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \ -\ ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)"; -by (blast_tac (!claset addDs [lemma]) 1); -qed "PMS_sessionK_not_spied"; - -goal thy - "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \ -\ ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)"; -by (blast_tac (!claset addDs [lemma]) 1); -qed "PMS_Crypt_sessionK_not_spied"; - - -(*Lemma: write keys are never sent if M (MASTER SECRET) is secure. - Converse doesn't hold; betraying M doesn't force the keys to be sent! - The strong Oops condition can be weakened later by unicity reasoning, - with some effort.*) -goal thy - "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \ -\ Nonce M ~: analz (spies evs); evs : tls |] \ -\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (analz_induct_tac 1); (*17 seconds*) -(*Oops*) -by (Blast_tac 4); -(*SpyKeys*) -by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3); -(*Fake*) -by (spy_analz_tac 2); -(*Base*) -by (Blast_tac 1); -qed "sessionK_not_spied"; -Addsimps [sessionK_not_spied]; - - (*** Unicity results for PMS, the pre-master-secret ***) (*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) @@ -525,6 +367,144 @@ +(**** Secrecy Theorems ****) + +(*Key compromise lemma needed to prove analz_image_keys. + 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 (spies evs))) = \ +\ (priK B : KK | B : bad)"; +by (etac tls.induct 1); +by (ALLGOALS + (asm_simp_tac (analz_image_keys_ss + addsimps (certificate_def::keys_distinct)))); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); +qed_spec_mp "analz_image_priK"; + + +(*slightly speeds up the big simplification below*) +goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK"; +by (Blast_tac 1); +val range_sessionkeys_not_priK = result(); + +(*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(); + +(** Strangely, the following version doesn't work: +\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ +\ (Nonce N : analz (spies evs))"; +**) + +goal thy + "!!evs. evs : tls ==> \ +\ ALL KK. KK <= range sessionK --> \ +\ (Nonce N : analz (Key``KK Un (spies evs))) = \ +\ (Nonce N : analz (spies evs))"; +by (etac tls.induct 1); +by (ClientKeyExch_tac 7); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac lemma)); +by (ALLGOALS (*24 seconds*) + (asm_simp_tac (analz_image_keys_ss + addsimps [range_sessionkeys_not_priK, + analz_image_priK, certificate_def]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); +qed_spec_mp "analz_image_keys"; + +(*Knowing some session keys is no help in getting new nonces*) +goal thy + "!!evs. evs : tls ==> \ +\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ +\ (Nonce N : analz (spies evs))"; +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); +qed "analz_insert_key"; +Addsimps [analz_insert_key]; + + +(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***) + +(** Some lemmas about session keys, comprising clientK and serverK **) + + +(*Lemma: session keys are never used if PMS is fresh. + Nonces don't have to agree, allowing session resumption. + Converse doesn't hold; revealing PMS doesn't force the keys to be sent. + THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*) +goal thy + "!!evs. [| Nonce PMS ~: parts (spies evs); \ +\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \ +\ evs : tls |] \ +\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; +by (etac rev_mp 1); +by (hyp_subst_tac 1); +by (analz_induct_tac 1); +(*SpyKeys*) +by (blast_tac (!claset addSEs spies_partsEs) 3); +(*Fake*) +by (simp_tac (!simpset addsimps [parts_insert_spies]) 2); +by (Fake_parts_insert_tac 2); +(** LEVEL 6 **) +(*Oops*) +by (fast_tac (!claset addSEs [MPair_parts] + addDs [Says_imp_spies RS parts.Inj] + addss (!simpset)) 6); +by (REPEAT + (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, + Notes_master_imp_Crypt_PMS] + addSEs spies_partsEs) 1)); +val lemma = result(); + +goal thy + "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \ +\ ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)"; +by (blast_tac (!claset addDs [lemma]) 1); +qed "PMS_sessionK_not_spied"; +bind_thm ("PMS_sessionK_spiedE", + PMS_sessionK_not_spied RSN (2,rev_notE)); + +goal thy + "!!evs. [| Nonce PMS ~: parts (spies evs); evs : tls |] \ +\ ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)"; +by (blast_tac (!claset addDs [lemma]) 1); +qed "PMS_Crypt_sessionK_not_spied"; +bind_thm ("PMS_Crypt_sessionK_spiedE", + PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)); + +(*Lemma: write keys are never sent if M (MASTER SECRET) is secure. + Converse doesn't hold; betraying M doesn't force the keys to be sent! + The strong Oops condition can be weakened later by unicity reasoning, + with some effort.*) +goal thy + "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \ +\ Nonce M ~: analz (spies evs); evs : tls |] \ +\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)"; +by (etac rev_mp 1); +by (etac rev_mp 1); +by (analz_induct_tac 1); (*17 seconds*) +(*Oops*) +by (Blast_tac 4); +(*SpyKeys*) +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3); +(*Fake*) +by (spy_analz_tac 2); +(*Base*) +by (Blast_tac 1); +qed "sessionK_not_spied"; +Addsimps [sessionK_not_spied]; + + (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*) goal thy "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ @@ -588,7 +568,7 @@ (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS] addIs [Notes_unique_PMS RS conjunct1]) 2)); (*ClientKeyExch*) -by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)] +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE] addSDs [Says_imp_spies RS parts.Inj]) 1); bind_thm ("Says_clientK_unique", result() RSN(2,rev_mp) RSN(2,rev_mp)); @@ -610,8 +590,7 @@ (*Oops*) by (blast_tac (!claset addIs [Says_clientK_unique]) 2); (*ClientKeyExch*) -by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) :: - spies_partsEs)) 1); +by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1); qed_spec_mp "clientK_Oops_ALL"; @@ -636,7 +615,7 @@ Notes_Crypt_parts_spies, Crypt_unique_PMS]) 2)); (*ClientKeyExch*) -by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)] +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE] addSDs [Says_imp_spies RS parts.Inj]) 1); bind_thm ("Says_serverK_unique", result() RSN(2,rev_mp) RSN(2,rev_mp)); @@ -657,8 +636,7 @@ (*Oops*) by (blast_tac (!claset addIs [Says_serverK_unique]) 2); (*ClientKeyExch*) -by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) :: - spies_partsEs)) 1); +by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1); qed_spec_mp "serverK_Oops_ALL"; @@ -670,16 +648,15 @@ (*The mention of her name (A) in X assures A that B knows who she is.*) goal thy - "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ -\ X = Crypt (serverK(Na,Nb,M)) \ + "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \ \ (Hash{|Number SID, Nonce M, \ \ Nonce Na, Number PA, Agent A, \ \ Nonce Nb, Number PB, Agent B|}); \ \ M = PRF(PMS,NA,NB); \ -\ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ X : parts (spies evs) --> Says B A X : set evs"; -by (etac rev_mp 1); +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ X : parts (spies evs) --> Says B A X : set evs"; by (hyp_subst_tac 1); by (analz_induct_tac 1); (*22 seconds*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); @@ -687,13 +664,13 @@ by (ALLGOALS Clarify_tac); (*ClientKeyExch*) by (fast_tac (*blast_tac gives PROOF FAILED*) - (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2); + (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2); (*Fake: the Spy doesn't have the critical session key!*) by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); -val lemma = normalize_thm [RSspec, RSmp] (result()); +val lemma = normalize_thm [RSmp] (result()); (*Final version*) goal thy @@ -719,13 +696,11 @@ that B sends his message to A. If CLIENT KEY EXCHANGE were augmented to bind A's identity with PMS, then we could replace A' by A below.*) goal thy - "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ -\ evs : tls; A ~: bad; B ~: bad; \ -\ M = PRF(PMS,NA,NB) |] \ -\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ + "!!evs. [| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ +\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ \ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \ \ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)"; -by (etac rev_mp 1); by (hyp_subst_tac 1); by (analz_induct_tac 1); (*20 seconds*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); @@ -740,13 +715,13 @@ Crypt_unique_PMS]) 3)); (*ClientKeyExch*) by (blast_tac - (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2); + (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2); (*Fake: the Spy doesn't have the critical session key!*) by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); -val lemma = normalize_thm [RSspec, RSmp] (result()); +val lemma = normalize_thm [RSmp] (result()); (*Final version*) goal thy @@ -758,7 +733,6 @@ \ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs"; by (blast_tac (!claset addIs [lemma] addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); - qed_spec_mp "TrustServerMsg"; @@ -770,11 +744,12 @@ ***) goal thy - "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ -\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ -\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) --> \ -\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; + "!!evs. [| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ +\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \ +\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; +by (hyp_subst_tac 1); by (analz_induct_tac 1); (*15 seconds*) by (ALLGOALS Clarify_tac); (*ClientFinished, ClientResume: by unicity of PMS*) @@ -783,24 +758,25 @@ addDs [Notes_unique_PMS]) 3)); (*ClientKeyExch*) by (fast_tac (*blast_tac gives PROOF FAILED*) - (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2); + (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2); (*Fake: the Spy doesn't have the critical session key!*) by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); -val lemma = normalize_thm [RSspec, RSmp] (result()); +val lemma = normalize_thm [RSmp] (result()); (*Final version*) goal thy - "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs); \ + "!!evs. [| M = PRF(PMS,NA,NB); \ +\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ \ Notes A {|Agent B, Nonce PMS|} : set evs; \ -\ Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs; \ +\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ \ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; +\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; by (blast_tac (!claset addIs [lemma] addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); -qed_spec_mp "TrustClientMsg"; +qed "TrustClientMsg"; @@ -809,13 +785,14 @@ values PA, PB, etc. Even this one requires A to be uncompromised. ***) goal thy - "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\ -\ Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \ + "!!evs. [| M = PRF(PMS,NA,NB); \ +\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ +\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ \ certificate A KA : parts (spies evs); \ \ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\ \ : set evs; \ \ evs : tls; A ~: bad; B ~: bad |] \ -\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; +\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] addDs [Says_imp_spies RS parts.Inj]) 1); qed "AuthClientFinished";