# HG changeset patch # User paulson # Date 875096873 -7200 # Node ID 2f99d7a0dccc237e256d4be427bcbaa2580e4242 # Parent c5ae2d63dbaa04d77dda3b764dedc19b800d347b sessionK now indexed by nat instead of bool. Weaker Oops conditions on final guarantees diff -r c5ae2d63dbaa -r 2f99d7a0dccc src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Wed Sep 24 12:26:14 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Wed Sep 24 12:27:53 1997 +0200 @@ -17,6 +17,7 @@ rollback attacks). *) + open TLS; proof_timing:=true; @@ -162,7 +163,7 @@ REPEAT (FIRSTGOAL analz_mono_contra_tac) THEN fast_tac (!claset addss (!simpset)) i THEN - ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])); + ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])); (** Theorems of the form X ~: parts (spies evs) imply that NOBODY @@ -252,10 +253,10 @@ \ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; by (etac rev_mp 1); by (parts_induct_tac 1); +by clarify_tac; (*Fake*) by (blast_tac (!claset addIs [parts_insertI]) 1); (*Client, Server Accept*) -by (Step_tac 1); by (REPEAT (blast_tac (!claset addSEs spies_partsEs addSDs [Notes_Crypt_parts_spies]) 1)); qed "Notes_master_imp_Crypt_PMS"; @@ -424,16 +425,59 @@ (** Some lemmas about session keys, comprising clientK and serverK **) -(*Lemma: those 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!*) +(*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); (*30 seconds??*) +by (analz_induct_tac 1); (*30 seconds??*) (*Oops*) by (Blast_tac 4); (*SpyKeys*) @@ -442,40 +486,8 @@ by (spy_analz_tac 2); (*Base*) by (Blast_tac 1); -qed "sessionK_notin_parts"; -bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE)); - -Addsimps [sessionK_notin_parts]; -AddSEs [sessionK_in_partsE, - impOfSubs analz_subset_parts RS sessionK_in_partsE]; - - -(*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. [| ALL A. Says A Spy (Key (sessionK((Na, Nb, PRF(PMS,NA,NB)),b))) \ -\ ~: set evs; \ -\ Nonce PMS ~: parts (spies evs); evs : tls |] \ -\ ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (analz_induct_tac 1); -(*Fake*) -by (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]) 2); -by (Fake_parts_insert_tac 2); -(*Base, ClientFinished, ServerFinished, ClientResume: - trivial, e.g. by freshness*) -by (REPEAT - (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, - Notes_master_imp_Crypt_PMS] - addSEs spies_partsEs) 1)); -qed "Crypt_sessionK_notin_parts"; - -Addsimps [Crypt_sessionK_notin_parts]; -AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)]; +qed "sessionK_not_spied"; +Addsimps [sessionK_not_spied]; (*NEEDED??*) @@ -511,20 +523,19 @@ \ evs : tls |] \ \ ==> B=B'"; by (prove_unique_tac lemma 1); -qed "unique_PMS"; +qed "Crypt_unique_PMS"; + (** It is frustrating that we need two versions of the unicity results. - But Notes A {|Agent B, Nonce PMS|} determines both A and B, while - Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only - this weaker item is available. + But Notes A {|Agent B, Nonce PMS|} determines both A and B. Sometimes + we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which + determines B alone, and only if PMS is secret. **) (*In A's internal Note, PMS determines A and B.*) -goal thy - "!!evs. [| Nonce PMS ~: analz (spies evs); evs : tls |] \ -\ ==> EX A' B'. ALL A B. \ -\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; -by (etac rev_mp 1); +goal thy "!!evs. evs : tls \ +\ ==> EX A' B'. ALL A B. \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; by (parts_induct_tac 1); by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*) @@ -535,7 +546,6 @@ goal thy "!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \ \ Notes A' {|Agent B', Nonce PMS|} : set evs; \ -\ Nonce PMS ~: analz (spies evs); \ \ evs : tls |] \ \ ==> A=A' & B=B'"; by (prove_unique_tac lemma 1); @@ -564,17 +574,6 @@ bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp)); -(*Another way of showing unicity*) -goal thy - "!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \ -\ Notes A' {|Agent B', Nonce PMS|} : set evs; \ -\ A ~: bad; B ~: bad; \ -\ evs : tls |] \ -\ ==> A=A' & B=B'"; -by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1)); -qed "good_Notes_unique_PMS"; - - (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET will stay secret.*) goal thy @@ -601,6 +600,97 @@ bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); +(*** Weakening the Oops conditions for leakage of clientK ***) + +(*If A created PMS then nobody other than the Spy would send a message + using a clientK generated from that PMS.*) +goal thy + "!!evs. [| evs : tls; A' ~= Spy |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ +\ A = A'"; +by (analz_induct_tac 1); (*17 seconds*) +by clarify_tac; +(*ClientFinished, ClientResume: by unicity of PMS*) +by (REPEAT + (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS] + addIs [Notes_unique_PMS RS conjunct1]) 2)); +(*ClientCertKeyEx*) +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)] + addSDs [Says_imp_spies RS parts.Inj]) 1); +bind_thm ("Says_clientK_unique", + result() RSN(2,rev_mp) RSN(2,rev_mp)); + + +(*If A created PMS and has not leaked her clientK to the Spy, + then nobody has.*) +goal thy + "!!evs. evs : tls \ +\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; +by (etac tls.induct 1); +(*This roundabout proof sequence avoids looping in simplification*) +by (ALLGOALS Simp_tac); +by clarify_tac; +by (Fake_parts_insert_tac 1); +by (ALLGOALS Asm_simp_tac); +(*Oops*) +by (blast_tac (!claset addIs [Says_clientK_unique]) 2); +(*ClientCertKeyEx*) +by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) :: + spies_partsEs)) 1); +qed_spec_mp "clientK_Oops_ALL"; + + + +(*** Weakening the Oops conditions for leakage of serverK ***) + +(*If A created PMS for B, then nobody other than B or the Spy would + send a message using a serverK generated from that PMS.*) +goal thy + "!!evs. [| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ +\ B = B'"; +by (analz_induct_tac 1); (*17 seconds*) +by clarify_tac; +(*ServerResume, ServerFinished: by unicity of PMS*) +by (REPEAT + (blast_tac (!claset addSEs [MPair_parts] + addSDs [Notes_master_imp_Crypt_PMS, + Says_imp_spies RS parts.Inj] + addDs [Spy_not_see_PMS, + Notes_Crypt_parts_spies, + Crypt_unique_PMS]) 2)); +(*ClientCertKeyEx*) +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)] + addSDs [Says_imp_spies RS parts.Inj]) 1); +bind_thm ("Says_serverK_unique", + result() RSN(2,rev_mp) RSN(2,rev_mp)); + +(*If A created PMS for B, and B has not leaked his serverK to the Spy, + then nobody has.*) +goal thy + "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ +\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; +by (etac tls.induct 1); +(*This roundabout proof sequence avoids looping in simplification*) +by (ALLGOALS Simp_tac); +by clarify_tac; +by (Fake_parts_insert_tac 1); +by (ALLGOALS Asm_simp_tac); +(*Oops*) +by (blast_tac (!claset addIs [Says_serverK_unique]) 2); +(*ClientCertKeyEx*) +by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) :: + spies_partsEs)) 1); +qed_spec_mp "serverK_Oops_ALL"; + + + (*** Protocol goals: if A receives ServerFinished, 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. @@ -619,25 +709,44 @@ \ X : parts (spies evs) --> Says B A X : set evs"; by (etac rev_mp 1); by (hyp_subst_tac 1); -by (analz_induct_tac 1); (*16 seconds*) -(*ServerResume is trivial, but Blast_tac is too slow*) -by (Best_tac 3); +by (analz_induct_tac 1); (*27 seconds*) +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); +by clarify_tac; +(*ServerResume*) +by (Blast_tac 3); (*ClientCertKeyEx*) -by (Blast_tac 2); +by (fast_tac (*blast_tac gives PROOF FAILED*) + (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2); (*Fake: the Spy doesn't have the critical session key!*) -by (REPEAT (rtac impI 1)); 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()); + +(*Final version*) +goal thy + "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \ +\ (Hash{|Nonce M, Number SID, \ +\ Nonce NA, Number XA, Agent A, \ +\ Nonce NB, Number XB, Agent B|}); \ +\ M = PRF(PMS,NA,NB); \ +\ X : parts (spies evs); \ +\ Notes A {|Agent B, Nonce PMS|} : set evs; \ +\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Says B A X : set evs"; +by (blast_tac (!claset addIs [lemma] + addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); qed_spec_mp "TrustServerFinished"; + (*This version refers not to ServerFinished but to any message from B. We don't assume B has received CertVerify, 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. If CLIENT KEY EXCHANGE were augmented - to bind A's identity with M, then we could replace A' by A below.*) + 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; \ @@ -648,33 +757,47 @@ by (etac rev_mp 1); by (hyp_subst_tac 1); by (analz_induct_tac 1); (*20 seconds*) -by (REPEAT_FIRST (rtac impI)); -(*ServerResume, by unicity of PMS*) -by (blast_tac (!claset addSEs [MPair_parts] - addDs [Spy_not_see_PMS, - Notes_Crypt_parts_spies, - Notes_master_imp_Crypt_PMS, unique_PMS]) 4); -(*ServerFinished, by unicity of PMS (10 seconds)*) -by (blast_tac (!claset addSEs [MPair_parts] - addDs [Spy_not_see_PMS, - Notes_Crypt_parts_spies, - Says_imp_spies RS parts.Inj, - unique_PMS]) 3); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); +by clarify_tac; +(*ServerResume, ServerFinished: by unicity of PMS*) +by (REPEAT + (blast_tac (!claset addSEs [MPair_parts] + addSDs [Notes_master_imp_Crypt_PMS, + Says_imp_spies RS parts.Inj] + addDs [Spy_not_see_PMS, + Notes_Crypt_parts_spies, + Crypt_unique_PMS]) 3)); (*ClientCertKeyEx*) -by (Blast_tac 2); +by (blast_tac + (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 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()); + +(*Final version*) +goal thy + "!!evs. [| M = PRF(PMS,NA,NB); \ +\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \ +\ Notes A {|Agent B, Nonce PMS|} : set evs; \ +\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> 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"; + (*** Protocol goal: if B receives any message encrypted with clientK then A has sent it, ASSUMING that A chose PMS. Authentication is assumed here; B cannot verify it. But if the message is ClientFinished, then B can then check the quoted values XA, XB, etc. ***) + goal thy "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ \ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\ @@ -682,23 +805,30 @@ \ 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"; by (analz_induct_tac 1); (*23 seconds*) -by (REPEAT_FIRST (rtac impI)); -(*ClientResume: by unicity of PMS*) -by (blast_tac (!claset delrules [conjI] - addSEs [MPair_parts] - addSDs [Notes_master_imp_Notes_PMS] - addDs [good_Notes_unique_PMS]) 4); -(*ClientFinished: by unicity of PMS*) -by (blast_tac (!claset delrules [conjI] - addSEs [MPair_parts] - addDs [good_Notes_unique_PMS]) 3); +by clarify_tac; +(*ClientFinished, ClientResume: by unicity of PMS*) +by (REPEAT (blast_tac (!claset delrules [conjI] + addSDs [Notes_master_imp_Notes_PMS] + addDs [Notes_unique_PMS]) 3)); (*ClientCertKeyEx*) -by (Blast_tac 2); +by (fast_tac (*blast_tac gives PROOF FAILED*) + (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 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()); + +(*Final version*) +goal thy + "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) 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; \ +\ evs : tls; A ~: bad; B ~: bad |] \ +\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; +by (blast_tac (!claset addIs [lemma] + addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); qed_spec_mp "TrustClientMsg"; @@ -708,7 +838,7 @@ values XA, XB, etc. Even this one requires A to be uncompromised. ***) goal thy - "!!evs. [| ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\ + "!!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; \ \ Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|} \ \ : set evs; \ @@ -722,3 +852,5 @@ qed "AuthClientFinished"; (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) + + diff -r c5ae2d63dbaa -r 2f99d7a0dccc src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Wed Sep 24 12:26:14 1997 +0200 +++ b/src/HOL/Auth/TLS.thy Wed Sep 24 12:27:53 1997 +0200 @@ -45,10 +45,11 @@ (*Pseudo-random function of Section 5*) PRF :: "nat*nat*nat => nat" - (*Client, server write keys generated uniformly by function sessionK - to avoid duplicating their properties. - Theyimplicitly include the MAC secrets.*) - sessionK :: "(nat*nat*nat)*bool => key" + (*Client, server write keys are generated uniformly by function sessionK + to avoid duplicating their properties. They are indexed by a further + natural number, not a bool, to avoid the peculiarities of if-and-only-if. + Session keys implicitly include MAC secrets.*) + sessionK :: "(nat*nat*nat)*nat => key" certificate :: "[agent,key] => msg" @@ -60,8 +61,8 @@ clientK, serverK :: "nat*nat*nat => key" translations - "clientK (x)" == "sessionK(x,True)" - "serverK (x)" == "sessionK(x,False)" + "clientK (x)" == "sessionK(x,0)" + "serverK (x)" == "sessionK(x,1)" rules inj_PRF "inj PRF"