diff -r f677f0bc1cdf -r 5b8c0c8f576e src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Sep 19 16:11:24 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Fri Sep 19 16:12:21 1997 +0200 @@ -7,10 +7,10 @@ * 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 +* B upon receiving CertVerify knows that A is present (But this message is optional!) -* A upon receiving SERVER FINISHED knows that B is present +* A upon receiving ServerFinished 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 @@ -86,34 +86,26 @@ **) - -(*Possibility property ending with ServerFinished.*) +(*Possibility property ending with ClientAccepts.*) goal thy "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ -\ A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls. \ -\ Says B A (Crypt (serverK(NA,NB,M)) \ -\ (Hash{|Nonce M, Number SID, \ -\ Nonce NA, Number XA, Agent A, \ -\ Nonce NB, Number XB, Agent B|})) \ -\ : set evs"; +\ A ~= B |] ==> EX SID M. EX evs: tls. \ +\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx - RS tls.ServerFinished) 2); + RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2); by possibility_tac; by (REPEAT (Blast_tac 1)); result(); -(*And one for ClientFinished. Either FINISHED message may come first.*) +(*And one for ServerAccepts. Either FINISHED message may come first.*) goal thy "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ \ A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls. \ -\ Says A B (Crypt (clientK(NA,NB,M)) \ -\ (Hash{|Nonce M, Number SID, \ -\ Nonce NA, Number XA, Agent A, \ -\ Nonce NB, Number XB, Agent B|})) : set evs"; +\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx - RS tls.ClientFinished) 2); + RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2); by possibility_tac; by (REPEAT (Blast_tac 1)); result(); @@ -131,6 +123,24 @@ by (REPEAT (Blast_tac 1)); result(); +(*Another one, for session resumption (both ServerResume and ClientResume) *) +goal thy + "!!A B. [| evs0 : tls; \ +\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ +\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ +\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] ==> EX NA XA NB XB. EX evs: tls. \ +\ Says A B (Crypt (clientK(NA,NB,M)) \ +\ (Hash{|Nonce M, Number SID, \ +\ Nonce NA, Number XA, Agent A, \ +\ Nonce NB, Number XB, Agent B|})) : set evs"; +by (REPEAT (resolve_tac [exI,bexI] 1)); +by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2); +by possibility_tac; +by (REPEAT (Blast_tac 1)); +result(); + + (**** Inductive proofs about tls ****) @@ -216,24 +226,7 @@ setloop split_tac [expand_if])); -(*** Hashing of nonces ***) - -(*Every Nonce that's hashed is already in past traffic. - This event occurs in CERTIFICATE VERIFY*) -goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs); \ -\ NB ~: range PRF; evs : tls |] \ -\ ==> Nonce NB : parts (spies evs)"; -by (etac rev_mp 1); -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies]))); -by (Fake_parts_insert_tac 1); -(*FINISHED messages are trivial because M : range PRF*) -by (REPEAT (Blast_tac 2)); -(*CERTIFICATE VERIFY is the only interesting case*) -by (blast_tac (!claset addSEs spies_partsEs) 1); -qed "Hash_Nonce_CV"; - +(*** Notes are made under controlled circumstances ***) goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \ \ ==> Crypt (pubK B) X : parts (spies evs)"; @@ -242,8 +235,65 @@ by (blast_tac (!claset addIs [parts_insertI]) 1); qed "Notes_Crypt_parts_spies"; +(*C might be either A or B*) +goal thy + "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce M|} : set evs; \ +\ evs : tls \ +\ |] ==> M : range PRF"; +by (etac rev_mp 1); +by (parts_induct_tac 1); +by (Auto_tac()); +qed "Notes_master_range_PRF"; -(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***) +(*C might be either A or B*) +goal thy + "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \ +\ : set evs; evs : tls \ +\ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; +by (etac rev_mp 1); +by (parts_induct_tac 1); +(*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"; + +(*Compared with the theorem above, both premise and conclusion are stronger*) +goal thy + "!!evs. [| Notes A {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \ +\ : set evs; evs : tls \ +\ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs"; +by (etac rev_mp 1); +by (parts_induct_tac 1); +(*ServerAccepts*) +by (Fast_tac 1); (*Blast_tac's very slow here*) +qed "Notes_master_imp_Notes_PMS"; + + +(*Every Nonce that's hashed is already in past traffic; this event + occurs in CertVerify. The condition NB ~: range PRF excludes the + MASTER SECRET from consideration; it is created using PRF.*) +goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs); \ +\ NB ~: range PRF; evs : tls |] \ +\ ==> Nonce NB : parts (spies evs)"; +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies]))); +(*Server/Client Resume: wrong sort of nonce!*) +by (REPEAT (blast_tac (!claset addSDs [Notes_master_range_PRF]) 5)); +(*FINISHED messages are trivial because M : range PRF*) +by (REPEAT (Blast_tac 3)); +(*CertVerify is the only interesting case*) +by (blast_tac (!claset addSEs spies_partsEs) 2); +by (Fake_parts_insert_tac 1); +qed "Hash_Nonce_CV"; + + + +(*** Protocol goal: if B receives CertVerify, then A sent it ***) (*B can check A's signature if he has received A's certificate. Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first @@ -265,7 +315,7 @@ qed_spec_mp "TrustCertVerify"; -(*If CERTIFICATE VERIFY is present then A has chosen PMS.*) +(*If CertVerify is present then A has chosen PMS.*) goal thy "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|}) \ \ : parts (spies evs); \ @@ -392,12 +442,14 @@ (*Fake*) by (asm_simp_tac (!simpset addsimps [parts_insert_spies]) 2); by (Fake_parts_insert_tac 2); -(*Base, ClientFinished, ServerFinished: trivial, e.g. by freshness*) +(*Base, ClientFinished, ServerFinished, ClientResume: + trivial, e.g. by freshness*) by (REPEAT - (blast_tac (!claset addSDs [Notes_Crypt_parts_spies] + (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)]; @@ -437,6 +489,11 @@ by (prove_unique_tac lemma 1); qed "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. +**) (*In A's internal Note, PMS determines A and B.*) goal thy @@ -467,7 +524,7 @@ "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ \ Nonce PMS ~: analz (spies evs)"; -by (analz_induct_tac 1); (*30 seconds???*) +by (analz_induct_tac 1); (*30 seconds??*) (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) by (REPEAT (fast_tac (!claset addss (!simpset)) 6)); (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) @@ -486,7 +543,15 @@ 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 @@ -516,12 +581,12 @@ bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); -(*** Protocol goals: if A receives SERVER FINISHED, then B is present +(*** 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. ***) -(*The mention of her name (A) in X assumes A that B knows who she is.*) +(*The mention of her name (A) in X assures A that B knows who she is.*) goal thy "!!evs. [| X = Crypt (serverK(Na,Nb,M)) \ \ (Hash{|Nonce M, Number SID, \ @@ -533,6 +598,8 @@ \ X : parts (spies evs) --> Says B A X : set evs"; 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); (*ClientCertKeyEx*) by (Blast_tac 2); (*Fake: the Spy doesn't have the critical session key!*) @@ -544,8 +611,8 @@ qed_spec_mp "TrustServerFinished"; -(*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 +(*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.*) @@ -558,6 +625,17 @@ by (hyp_subst_tac 1); by (analz_induct_tac 1); (*12 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); (*ClientCertKeyEx*) by (Blast_tac 2); (*Fake: the Spy doesn't have the critical session key!*) @@ -565,24 +643,13 @@ by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 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 PMS.*) -by (thin_tac "?PP-->?QQ" 1); -by (Step_tac 1); -by (subgoal_tac "Nonce PMS ~: analz(spies evsSF)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2); -by (blast_tac (!claset addSEs [MPair_parts] - addDs [Notes_Crypt_parts_spies, - Says_imp_spies RS parts.Inj, - unique_PMS]) 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 - CLIENT FINISHED, then B can then check the quoted values XA, XB, etc. + ClientFinished, then B can then check the quoted values XA, XB, etc. ***) goal thy "!!evs. [| evs : tls; A ~: bad; B ~: bad |] \ @@ -598,17 +665,21 @@ by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); -(*ClientFinished. If the message is old then apply induction hypothesis...*) -by (step_tac (!claset delrules [conjI]) 1); -by (subgoal_tac "Nonce PMS ~: analz (spies evsCF)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2); -by (blast_tac (!claset addSEs [MPair_parts] - addDs [Notes_unique_PMS]) 1); +(*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]) 2); +(*ClientFinished: by unicity of PMS*) +by (blast_tac (!claset delrules [conjI] + addSEs [MPair_parts] + addDs [good_Notes_unique_PMS]) 1); qed_spec_mp "TrustClientMsg"; -(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to - check a CERTIFICATE VERIFY from A, then A has used the quoted + +(*** Protocol goal: if B receives ClientFinished, and if B is able to + check a CertVerify from A, then A has used the quoted values XA, XB, etc. Even this one requires A to be uncompromised. ***) goal thy