# HG changeset patch # User paulson # Date 874927049 -7200 # Node ID fb7d096d788493e6a95256c52c0953bf0a8f0d12 # Parent 4b484805b4c48fb36994b65a99f9875971654031 Simplified SpyKeys to use sessionK instead of clientK and serverK Proved and used analz_insert_key, shortening scripts diff -r 4b484805b4c4 -r fb7d096d7884 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Sep 19 18:27:31 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Mon Sep 22 13:17:29 1997 +0200 @@ -327,11 +327,12 @@ qed "UseCertVerify"; -(*No collection of keys can help the spy get new private keys*) +(*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)"; +\ (priK B : KK | B : bad)"; by (etac tls.induct 1); by (ALLGOALS (asm_simp_tac (analz_image_keys_ss @@ -355,7 +356,16 @@ by (Blast_tac 1); val range_sessionkeys_not_priK = result(); -(*Knowing some session keys is no help in getting new nonces*) +(** 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 --> \ @@ -378,6 +388,14 @@ 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); @@ -417,10 +435,8 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*30 seconds??*) (*Oops*) -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 4); by (Blast_tac 4); (*SpyKeys*) -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3); (*Fake*) by (spy_analz_tac 2); @@ -533,20 +549,15 @@ \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ \ Nonce PMS ~: analz (spies evs)"; by (analz_induct_tac 1); (*30 seconds??*) -(*oops*) -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9); (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6])); -(*ServerHello, ClientCertKeyEx, ServerResume: mostly freshness reasoning*) +(*ClientHello, ServerHello, ClientCertKeyEx, ServerResume: + mostly freshness reasoning*) by (REPEAT (blast_tac (!claset addSEs partsEs addDs [Notes_Crypt_parts_spies, impOfSubs analz_subset_parts, - Says_imp_spies RS analz.Inj]) 4)); -(*ClientHello*) -by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies] - addSEs spies_partsEs) 3); + Says_imp_spies RS analz.Inj]) 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); @@ -571,8 +582,6 @@ \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ \ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; by (analz_induct_tac 1); (*35 seconds*) -(*Oops*) -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9); (*ClientAccepts and ServerAccepts: because PMS was already visible*) by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, Says_imp_spies RS analz.Inj, @@ -580,7 +589,6 @@ (*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_spies RS analz.Inj]) 2); (*Fake*) @@ -712,3 +720,5 @@ by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] addDs [Says_imp_spies RS parts.Inj]) 1); qed "AuthClientFinished"; + +(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) diff -r 4b484805b4c4 -r fb7d096d7884 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Fri Sep 19 18:27:31 1997 +0200 +++ b/src/HOL/Auth/TLS.thy Mon Sep 22 13:17:29 1997 +0200 @@ -66,7 +66,8 @@ rules inj_PRF "inj PRF" - (*sessionK is collision-free and makes symmetric keys*) + (*sessionK is collision-free and makes symmetric keys. Also, no clientK + clashes with any serverK.*) inj_sessionK "inj sessionK" isSym_sessionK "isSymKey (sessionK x)" @@ -75,9 +76,6 @@ inj_serverK "inj serverK" isSym_serverK "isSymKey (serverK x)" - (*Clashes with pubK and priK are impossible, but this axiom is needed.*) - clientK_range "range clientK <= Compl (range serverK)" - consts tls :: event list set inductive tls @@ -90,12 +88,11 @@ X: synth (analz (spies evs)) |] ==> Says Spy B X # evs : tls" - SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*) + SpyKeys (*The spy may apply PRF & sessionK 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" + Key (sessionK((NA,NB,M),b)) |} # evsSK : tls" ClientHello (*(7.4.1.2) @@ -196,7 +193,8 @@ ClientAccepts (*Having transmitted ClientFinished and received an identical message encrypted with serverK, the client stores the parameters - needed to resume this session.*) + needed to resume this session. The "Notes A ..." premise is + used to prove Notes_master_imp_Crypt_PMS.*) "[| evsCA: tls; Notes A {|Agent B, Nonce PMS|} : set evsCA; M = PRF(PMS,NA,NB); @@ -211,7 +209,8 @@ ServerAccepts (*Having transmitted ServerFinished and received an identical message encrypted with clientK, the server stores the parameters - needed to resume this session.*) + needed to resume this session. The "Says A'' B ..." premise is + used to prove Notes_master_imp_Crypt_PMS.*) "[| evsSA: tls; Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|} : set evsSA;