# HG changeset patch # User paulson # Date 874409542 -7200 # Node ID 56e4365a0c99a66fca6aeee7935820358b0e6cf1 # Parent 8326f03d667cf09e3115f96399629d91a3c46e51 TLS now with a distinction between premaster secret and master secret diff -r 8326f03d667c -r 56e4365a0c99 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Sep 12 10:45:51 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Tue Sep 16 13:32:22 1997 +0200 @@ -48,7 +48,7 @@ (*Injectiveness of key-generating functions*) -AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq]; +AddIffs [inj_PRF RS inj_eq, 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, @@ -97,43 +97,56 @@ (*A "possibility property": there are traces that reach the end. This protocol has three end points and six messages to consider.*) + +(** These proofs make the further assumption 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. +**) + + + (*Possibility property ending with ServerFinished.*) goal thy - "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ -\ Says B A (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)|})) \ + "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] ==> EX NA XA NB XB M. EX evs: tls. \ +\ Says B A (Crypt (serverK(NA,NB,M)) \ +\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \ +\ Nonce NB, Number XB, Agent B|})) \ \ : 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); by possibility_tac; +by (REPEAT (Blast_tac 1)); result(); (*And one for ClientFinished. Either FINISHED message may come first.*) goal thy - "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ + "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] ==> EX NA XA NB XB M. EX evs: tls. \ \ Says A B (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|})) : set evs"; +\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \ +\ Nonce NB, Number XB, Agent B|})) : 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); by possibility_tac; +by (REPEAT (Blast_tac 1)); result(); (*Another one, for CertVerify (which is optional)*) goal thy - "!!A B. A ~= B ==> EX NB M. EX evs: tls. \ + "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ +\ A ~= B |] ==> EX NB PMS. EX evs: tls. \ \ Says A B (Crypt (priK A) \ -\ (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs"; +\ (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx RS tls.CertVerify) 2); by possibility_tac; +by (REPEAT (Blast_tac 1)); result(); @@ -211,40 +224,33 @@ ClientCertKeyEx_tac (i+6) THEN (*CertVerify*) ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz] + (!simpset addcongs [if_weak_cong] 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] + (!simpset addcongs [if_weak_cong] + 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 Spy evs); \ -\ evs : tls |] \ -\ ==> Nonce N : parts (sees Spy evs)"; +(*Every Nonce that's hashed is already in past traffic. + This event occurs in CERTIFICATE VERIFY*) +goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs); \ +\ NB ~: range PRF; evs : tls |] \ +\ ==> Nonce NB : parts (sees Spy 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_sees]))); by (Fake_parts_insert_tac 1); -by (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*) -goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|} \ -\ : parts (sees Spy evs); \ -\ evs : tls |] \ -\ ==> Nonce M : parts (sees Spy evs)"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1); -by (Fake_parts_insert_tac 1); -qed "Hash_imp_Nonce2"; -AddSDs [Hash_imp_Nonce2]; +(*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 sees_Spy_partsEs) 1); +qed "Hash_Nonce_CV"; goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \ @@ -255,38 +261,25 @@ qed "Notes_Crypt_parts_sees"; -(*NEEDED??*) -goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |} \ -\ : parts (sees Spy evs); \ -\ evs : tls |] \ -\ ==> Nonce M : parts (sees Spy evs)"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); -by (Fake_parts_insert_tac 1); -by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees, - Says_imp_sees_Spy RS parts.Inj] - addSEs partsEs) 1)); -qed "Hash_Hash_imp_Nonce"; - - -(*NEEDED?? - Every Nonce that's hashed is already in past traffic. - This general formulation is tricky to prove and hard to use, since the - 2nd premise is typically proved by simplification.*) -goal thy "!!evs. [| Hash X : parts (sees Spy evs); \ -\ Nonce N : parts {X}; evs : tls |] \ -\ ==> Nonce N : parts (sees Spy evs)"; -by (etac rev_mp 1); -by (parts_induct_tac 1); -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); -(*CertVerify, ClientFinished, ServerFinished (?)*) -by (REPEAT (Blast_tac 1)); -qed "Hash_imp_Nonce_seen"; +(***************** + (*NEEDED? TRUE??? + Every Nonce that's hashed is already in past traffic. + This general formulation is tricky to prove and hard to use, since the + 2nd premise is typically proved by simplification.*) + goal thy "!!evs. [| Hash X : parts (sees Spy evs); \ + \ Nonce N : parts {X}; evs : tls |] \ + \ ==> Nonce N : parts (sees Spy evs)"; + by (etac rev_mp 1); + by (parts_induct_tac 1); + 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); + (*CertVerify, ClientFinished, ServerFinished (?)*) + by (REPEAT (Blast_tac 1)); + qed "Hash_imp_Nonce_seen"; +****************************************************************) (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***) @@ -297,26 +290,26 @@ assume A~:lost; otherwise, the Spy can forge A's signature.*) goal thy "!!evs. [| X = Crypt (priK A) \ -\ (Hash{|Nonce NB, certificate B KB, Nonce M|}); \ +\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|}); \ \ evs : tls; A ~: lost; B ~= Spy |] \ -\ ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \ +\ ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} \ \ : set evs --> \ \ X : parts (sees Spy evs) --> Says A B X : set evs"; by (hyp_subst_tac 1); by (parts_induct_tac 1); 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] +by (blast_tac (!claset addSDs [Hash_Nonce_CV] addSEs sees_Spy_partsEs) 1); qed_spec_mp "TrustCertVerify"; -(*If CERTIFICATE VERIFY is present then A has chosen M.*) +(*If CERTIFICATE VERIFY is present then A has chosen PMS.*) goal thy - "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|}) \ + "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|}) \ \ : parts (sees Spy evs); \ \ evs : tls; A ~: lost |] \ -\ ==> Notes A {|Agent B, Nonce M|} : set evs"; +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; be rev_mp 1; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); @@ -356,12 +349,11 @@ by (ClientCertKeyEx_tac 6); by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac lemma)); -writeln"SLOW simplification: 50 secs!??"; +writeln"SLOW simplification: 60 secs!??"; by (ALLGOALS (asm_simp_tac (analz_image_keys_ss - addsimps (analz_image_priK::certificate_def:: + 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); @@ -372,17 +364,26 @@ qed_spec_mp "analz_image_keys"; -(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*) +goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs"; +by (parts_induct_tac 1); +(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*) +by (Blast_tac 1); +qed "no_Notes_A_PRF"; +Addsimps [no_Notes_A_PRF]; + + +(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*) goal thy "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ -\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ -\ Nonce M ~: analz (sees Spy evs)"; -by (analz_induct_tac 1); +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Nonce PMS ~: analz (sees Spy evs)"; +by (analz_induct_tac 1); (*47 seconds???*) (*ClientHello*) 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); +by (fast_tac (!claset addss (!simpset)) 2); (*Fake*) by (spy_analz_tac 1); (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) @@ -390,7 +391,52 @@ 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)); +bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp)); + + + +goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs); \ +\ evs : tls |] \ +\ ==> Nonce PMS : parts (sees Spy evs)"; +by (etac rev_mp 1); +by (parts_induct_tac 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); +by (Fake_parts_insert_tac 1); +(*Client key exchange*) +by (Blast_tac 4); +(*Server Hello: by freshness*) +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); +(*Client Hello: trivial*) +by (Blast_tac 2); +(*SpyKeys*) +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); +qed "MS_imp_PMS"; +AddSDs [MS_imp_PMS]; + + +(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET + will stay secret.*) +goal thy + "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)"; +by (analz_induct_tac 1); (*47 seconds???*) +(*ClientHello*) +by (Blast_tac 3); +(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); +by (blast_tac (!claset addSDs [Spy_not_see_PMS, + Says_imp_sees_Spy RS analz.Inj]) 2); +(*Fake*) +by (spy_analz_tac 1); +(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) +by (REPEAT (blast_tac (!claset addSEs partsEs + addDs [MS_imp_PMS, + Notes_Crypt_parts_sees, + impOfSubs analz_subset_parts, + Says_imp_sees_Spy RS analz.Inj]) 1)); +bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); + (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***) @@ -398,7 +444,7 @@ (** 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. +(*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!*) goal thy @@ -414,9 +460,10 @@ (*Base*) by (Blast_tac 1); qed "clientK_notin_parts"; - +bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE)); Addsimps [clientK_notin_parts]; -AddSEs [clientK_notin_parts RSN (2, rev_notE)]; +AddSEs [clientK_in_partsE, + impOfSubs analz_subset_parts RS clientK_in_partsE]; goal thy "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \ @@ -431,33 +478,35 @@ (*Base*) by (Blast_tac 1); qed "serverK_notin_parts"; - +bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE)); Addsimps [serverK_notin_parts]; -AddSEs [serverK_notin_parts RSN (2, rev_notE)]; +AddSEs [serverK_in_partsE, + impOfSubs analz_subset_parts RS serverK_in_partsE]; -(*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.*) + +(*Lemma: those write 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 M ~: used evs; evs : tls |] \ -\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees Spy evs)"; + "!!evs. [| Nonce PMS ~: used evs; evs : tls |] \ +\ ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees 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); + 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 Spy evs)"; + "!!evs. [| Nonce PMS ~: used evs; evs : tls |] \ +\ ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)"; by (etac rev_mp 1); by (analz_induct_tac 1); (*ServerFinished: since M is fresh, a different instance of serverK was used.*) @@ -481,54 +530,54 @@ qed "A_Crypt_pubB"; -(*** Unicity results for M, the pre-master-secret ***) +(*** Unicity results for PMS, the pre-master-secret ***) -(*M determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) +(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) goal thy - "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \ + "!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \ \ ==> EX B'. ALL B. \ -\ Crypt (pubK B) (Nonce M) : parts (sees Spy evs) --> B=B'"; +\ Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); (*ClientCertKeyEx*) by (ClientCertKeyEx_tac 1); by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); -by (expand_case_tac "M = ?y" 1 THEN +by (expand_case_tac "PMS = ?y" 1 THEN blast_tac (!claset addSEs partsEs) 1); val lemma = result(); goal thy - "!!evs. [| Crypt(pubK B) (Nonce M) : parts (sees Spy evs); \ -\ Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \ -\ Nonce M ~: analz (sees Spy evs); \ + "!!evs. [| Crypt(pubK B) (Nonce PMS) : parts (sees Spy evs); \ +\ Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \ +\ Nonce PMS ~: analz (sees Spy evs); \ \ evs : tls |] \ \ ==> B=B'"; by (prove_unique_tac lemma 1); -qed "unique_M"; +qed "unique_PMS"; -(*In A's note to herself, M determines A and B.*) +(*In A's note to herself, PMS determines A and B.*) goal thy - "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \ + "!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \ \ ==> EX A' B'. ALL A B. \ -\ Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'"; +\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; by (etac rev_mp 1); by (parts_induct_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 +(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*) +by (expand_case_tac "PMS = ?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 Spy evs); \ + "!!evs. [| Notes A {|Agent B, Nonce PMS|} : set evs; \ +\ Notes A' {|Agent B', Nonce PMS|} : set evs; \ +\ Nonce PMS ~: analz (sees Spy evs); \ \ evs : tls |] \ \ ==> A=A' & B=B'"; by (prove_unique_tac lemma 1); -qed "Notes_unique_M"; +qed "Notes_unique_PMS"; @@ -539,20 +588,20 @@ (*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. [| X = Crypt (serverK(Na,Nb,M)) \ +\ (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \ +\ Nonce NB, Number XB, Agent B|}); \ +\ M = PRF(PMS,NA,NB); \ \ evs : tls; A ~: lost; B ~: lost |] \ -\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ \ X : parts (sees Spy evs) --> Says B A X : set evs"; by (hyp_subst_tac 1); 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 Spy evsa)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, +by (subgoal_tac + "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, not_parts_not_analz]) 2); by (Fake_parts_insert_tac 1); qed_spec_mp "TrustServerFinished"; @@ -562,56 +611,60 @@ 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. If CLIENT KEY EXCHANGE were augmented - to bind A's identify with M, then we could replace A' by A below.*) + to bind A's identity with M, then we could replace A' by A below.*) 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 Spy evs) --> \ -\ (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)"; + "!!evs. [| evs : tls; A ~: lost; B ~: lost; \ +\ M = PRF(PMS,NA,NB) |] \ +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs) --> \ +\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)"; +by (hyp_subst_tac 1); 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 Spy evsa)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, +by (subgoal_tac + "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1); +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 M.*) +(*...otherwise delete induction hyp and use unicity of PMS.*) by (thin_tac "?PP-->?QQ" 1); by (Step_tac 1); -by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); +by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2); by (blast_tac (!claset addSEs [MPair_parts] addDs [Notes_Crypt_parts_sees, Says_imp_sees_Spy RS parts.Inj, - unique_M]) 1); + 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 M. Authentication is + 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. ***) 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 Spy evs) --> \ -\ Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; +\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ +\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) --> \ +\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) 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 (clientK(NA,NB,M)) ~: analz (sees Spy evsa)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, +by (subgoal_tac + "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1); +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 M ~: analz (sees Spy evsa)" 1); -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); +by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1); +by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2); by (blast_tac (!claset addSEs [MPair_parts] - addDs [Notes_unique_M]) 1); + addDs [Notes_unique_PMS]) 1); qed_spec_mp "TrustClientMsg"; @@ -620,14 +673,14 @@ values XA, XB, etc. Even this one requires A to be uncompromised. ***) goal thy - "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs; \ -\ Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \ + "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \ +\ Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} \ \ : set evs; \ \ Says A'' B (Crypt (priK A) \ -\ (Hash{|Nonce NB, certificate B KB, Nonce M|})) \ +\ (Hash{|Nonce NB, certificate B KB, Nonce PMS|})) \ \ : set evs; \ \ evs : tls; A ~: lost; B ~: lost |] \ -\ ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; +\ ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] addDs [Says_imp_sees_Spy RS parts.Inj]) 1); qed "AuthClientFinished"; diff -r 8326f03d667c -r 56e4365a0c99 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Fri Sep 12 10:45:51 1997 +0200 +++ b/src/HOL/Auth/TLS.thy Tue Sep 16 13:32:22 1997 +0200 @@ -4,6 +4,12 @@ Copyright 1997 University of Cambridge Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol. +This protocol is essentially the same as SSL 3.0. + +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. Section numbers below refer +to that memo. An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a @@ -15,18 +21,14 @@ The model assumes that no fraudulent certificates are present, but it does assume that some private keys are to the spy. -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, +REMARK. The event "Notes A {|Agent B, Nonce PMS|}" 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 +The Note event avoids 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 +invents PMS, he encrypts PMS 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 @@ -36,8 +38,12 @@ TLS = Public + consts - (*Client, server write keys. They implicitly include the MAC secrets.*) + (*Pseudo-random function of Section 5*) + PRF :: "nat*nat*nat => nat" + + (*Client, server write keys implicitly include the MAC secrets.*) clientK, serverK :: "nat*nat*nat => key" + certificate :: "[agent,key] => msg" defs @@ -45,6 +51,8 @@ "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}" rules + inj_PRF "inj PRF" + (*clientK is collision-free and makes symmetric keys*) inj_clientK "inj clientK" isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) @@ -68,95 +76,105 @@ X: synth (analz (sees Spy evs)) |] ==> 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" + SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*) + "[| evsSK: tls; + Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |] + ==> Says Spy B {| Nonce (PRF(M,NA,NB)), + Key (clientK(NA,NB,M)), + Key (serverK(NA,NB,M)) |} # evsSK : tls" ClientHello - (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. + (*(7.4.1.2) + XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. It is uninterpreted but will be confirmed in the FINISHED messages. As an initial simplification, SESSION_ID is identified with NA - and reuse of sessions is not supported.*) - "[| evs: tls; A ~= B; Nonce NA ~: used evs |] - ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs : tls" + and reuse of sessions is not supported. + May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes + while MASTER SECRET is 48 byptes (6.1)*) + "[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |] + ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH : tls" ServerHello - (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. - 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 |] - ==> Says B A {|Nonce NA, Nonce NB, Agent XB, + (*7.4.1.3 of the TLS Internet-Draft + XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. + NA is returned in its role as SESSION_ID. + SERVER CERTIFICATE (7.4.2) is always present. + CERTIFICATE_REQUEST (7.4.4) is implied.*) + "[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF; + Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |] + ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B (pubK B)|} - # evs : tls" + # evsSH : tls" ClientCertKeyEx - (*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)|} - # Notes A {|Agent B, Nonce M|} - # evs : tls" + (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7). + The client, A, chooses PMS, the PREMASTER SECRET. + She encrypts PMS using the supplied KB, which ought to be pubK B. + We assume PMS ~: range PRF because a clash betweem the PMS + and another MASTER SECRET is highly unlikely (even though + both items have the same length, 48 bytes). + The Note event records in the trace that she knows PMS + (see REMARK at top).*) + "[| evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF; + Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} + : set evsCX |] + ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|} + # Notes A {|Agent B, Nonce PMS|} + # evsCX : tls" CertVerify - (*The optional CERTIFICATE VERIFY message contains the specific - components listed in the security analysis, Appendix F.1.1.2; - it also contains the pre-master-secret. Checking the signature, - which is the only use of A's certificate, assures B of A's presence*) - "[| evs: tls; A ~= B; - Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} - : set evs; - Notes A {|Agent B, Nonce M|} : set evs |] + (*The optional CERTIFICATE VERIFY (7.4.8) message contains the + specific components listed in the security analysis, F.1.1.2. + It adds the pre-master-secret, which is also essential! + Checking the signature, which is the only use of A's certificate, + assures B of A's presence*) + "[| evsCV: tls; A ~= B; + Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} + : set evsCV; + Notes A {|Agent B, Nonce PMS|} : set evsCV |] ==> Says A B (Crypt (priK A) - (Hash{|Nonce NB, certificate B KB, Nonce M|})) - # evs : tls" + (Hash{|Nonce NB, certificate B KB, Nonce PMS|})) + # evsCV : tls" - (*Finally come the FINISHED messages, confirming XA and XB among - other things. The master-secret is the hash of NA, NB and M. + (*Finally come the FINISHED messages (7.4.8), confirming XA and XB + among other things. The master-secret is PRF(PMS,NA,NB). Either party may sent its message first.*) - (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the + (*The occurrence of Notes A {|Agent B, Nonce PMS|} 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 + Spy does not know PMS 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; - Notes A {|Agent B, Nonce M|} : set evs |] + "[| evsCF: tls; + Says A B {|Agent A, Nonce NA, Number XA|} : set evsCF; + Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|} + : set evsCF; + Notes A {|Agent B, Nonce PMS|} : set evsCF; + M = PRF(PMS,NA,NB) |] ==> Says A B (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" + (Hash{|Nonce M, + Nonce NA, Number XA, Agent A, + Nonce NB, Number XB, Agent B|})) + # evsCF : tls" (*Keeping A' and A'' distinct means B cannot even check that the - two messages originate from the same source. B does not attempt - to read A's encrypted "note to herself".*) + two messages originate from the same source. *) 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, + "[| evsSF: tls; + Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSF; + Says B A {|Nonce NA, Nonce NB, Number XB, certificate B (pubK B)|} - : set evs; - Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|} - : set evs |] + : set evsSF; + Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|} + : set evsSF; + M = PRF(PMS,NA,NB) |] ==> Says B A (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" + (Hash{|Nonce M, + Nonce NA, Number XA, Agent A, + Nonce NB, Number XB, Agent B|})) + # evsSF : tls" (**Oops message??**)