# HG changeset patch # User paulson # Date 989330233 -7200 # Node ID 7fe6593133d44e95028e634fff8662365a9a448e # Parent 0103ee3082bfb5242dd0cb98c77af297f8b141a0 fixed a slow proof; tidied diff -r 0103ee3082bf -r 7fe6593133d4 src/HOL/Auth/KerberosIV.ML --- a/src/HOL/Auth/KerberosIV.ML Tue May 08 15:56:57 2001 +0200 +++ b/src/HOL/Auth/KerberosIV.ML Tue May 08 15:57:13 2001 +0200 @@ -46,7 +46,7 @@ qed "spies_evs_rev"; bind_thm ("parts_spies_evs_revD2", spies_evs_rev RS equalityD2 RS parts_mono); -Goal "spies (takeWhile P evs) <= spies evs"; +Goal "spies (takeWhile P evs) <= spies evs"; by (induct_tac "evs" 1); by (induct_tac "a" 2); by Auto_tac; @@ -54,11 +54,6 @@ qed "spies_takeWhile"; bind_thm ("parts_spies_takeWhile_mono", spies_takeWhile RS parts_mono); -Goal "~P(x) --> takeWhile P (xs @ [x]) = takeWhile P xs"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "takeWhile_tail"; - (*****************LEMMAS ABOUT AuthKeys****************) @@ -264,8 +259,9 @@ (asm_full_simp_tac (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert, AuthKeys_empty, AuthKeys_simp]))); -by (blast_tac (claset()) 1); +by (Blast_tac 1); by Auto_tac; +(*Three subcases of Message 4*) by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1); by (blast_tac (claset() addSDs [SesKey_is_session_key]) 1); by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey]) 1); @@ -445,9 +441,8 @@ AddIffs [not_KeyCryptKey_Nil]; Goalw [KeyCryptKey_def] - "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \ -\ \\ set evs; \ -\ evs \\ kerberos |] ==> KeyCryptKey AuthKey ServKey evs"; + "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \\ set evs; \ +\ evs \\ kerberos |] ==> KeyCryptKey AuthKey ServKey evs"; by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); qed "KeyCryptKeyI"; @@ -466,8 +461,8 @@ (*A fresh AuthKey cannot be associated with any other (with respect to a given trace). *) Goalw [KeyCryptKey_def] - "[| Key AuthKey \\ used evs; evs \\ kerberos |] \ -\ ==> ~ KeyCryptKey AuthKey ServKey evs"; + "[| Key AuthKey \\ used evs; evs \\ kerberos |] \ +\ ==> ~ KeyCryptKey AuthKey ServKey evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by (Asm_full_simp_tac 1); @@ -481,10 +476,9 @@ by (Blast_tac 1); qed "Serv_fresh_not_KeyCryptKey"; -Goal - "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\ -\ \\ parts (spies evs); evs \\ kerberos |] \ -\ ==> ~ KeyCryptKey K AuthKey evs"; +Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\ +\ \\ parts (spies evs); evs \\ kerberos |] \ +\ ==> ~ KeyCryptKey K AuthKey evs"; by (etac rev_mp 1); by (parts_induct_tac 1); (*K4*) @@ -515,17 +509,17 @@ (*Long term keys are not issued as ServKeys*) Goalw [KeyCryptKey_def] - "evs \\ kerberos ==> ~ KeyCryptKey K (shrK A) evs"; + "evs \\ kerberos ==> ~ KeyCryptKey K (shrK A) evs"; by (parts_induct_tac 1); qed "shrK_not_KeyCryptKey"; (*The Tgs message associates ServKey with AuthKey and therefore not with any other key AuthKey.*) Goalw [KeyCryptKey_def] - "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \ -\ \\ set evs; \ -\ AuthKey' \\ AuthKey; evs \\ kerberos |] \ -\ ==> ~ KeyCryptKey AuthKey' ServKey evs"; + "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \ +\ \\ set evs; \ +\ AuthKey' \\ AuthKey; evs \\ kerberos |] \ +\ ==> ~ KeyCryptKey AuthKey' ServKey evs"; by (blast_tac (claset() addDs [unique_ServKeys]) 1); qed "Says_Tgs_KeyCryptKey"; @@ -533,9 +527,9 @@ \ ==> ~ KeyCryptKey ServKey K evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Step_tac 1); +by Safe_tac; +(*K4 splits into subcases*) by (ALLGOALS Asm_full_simp_tac); -(*K4 splits into subcases*) by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 4); (*ServKey is fresh and so could not have been used, by new_keys_not_used*) by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj, @@ -654,7 +648,7 @@ \ ==> Key K \\ analz (insert (Key SesKey) (spies evs)) = \ \ (K = SesKey | Key K \\ analz (spies evs))"; by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); -by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); +by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); qed "analz_insert_freshK1"; @@ -666,7 +660,7 @@ by (ftac not_AuthKeys_not_KeyCryptKey 1 THEN assume_tac 1 THEN assume_tac 1); -by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); +by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); qed "analz_insert_freshK2"; @@ -682,7 +676,7 @@ by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1); by (Blast_tac 1); by (assume_tac 1); -by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); +by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); qed "analz_insert_freshK3"; @@ -710,8 +704,7 @@ by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1); by (parts_induct_tac 1); by (ALLGOALS Blast_tac); -bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE)); -bind_thm ("ServKey_notin_AuthKeysD", result()); +qed "ServKey_notin_AuthKeysD"; (** If Spy sees the Authentication Key sent in msg K2, then @@ -728,9 +721,9 @@ by analz_sees_tac; by (ALLGOALS (asm_simp_tac - (simpset() addsimps ([Says_Kas_message_form, less_SucI, - analz_insert_eq, not_parts_not_analz, - analz_insert_freshK1] @ pushes)))); + (simpset() addsimps [Says_Kas_message_form, less_SucI, + analz_insert_eq, not_parts_not_analz, + analz_insert_freshK1] @ pushes))); (*Fake*) by (spy_analz_tac 1); (*K2*) @@ -738,8 +731,7 @@ (*K4*) by (Blast_tac 1); (*Level 8: K5*) -by (blast_tac (claset() addEs [ServKey_notin_AuthKeys] - addDs [Says_Kas_message_form] +by (blast_tac (claset() addDs [ServKey_notin_AuthKeysD, Says_Kas_message_form] addIs [less_SucI]) 1); (*Oops1*) by (blast_tac (claset() addSDs [unique_AuthKeys] addIs [less_SucI]) 1); @@ -763,15 +755,17 @@ (** If Spy sees the Service Key sent in msg K4, then the Key has expired **) -Goal "[| A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ -\ ==> Key AuthKey \\ analz (spies evs) --> \ -\ Says Tgs A \ +Goal "[| Says Tgs A \ \ (Crypt AuthKey \ \ {|Key ServKey, Agent B, Number Tt, \ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})\ -\ \\ set evs --> \ -\ Key ServKey \\ analz (spies evs) --> \ +\ \\ set evs; \ +\ Key AuthKey \\ analz (spies evs); \ +\ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ +\ ==> Key ServKey \\ analz (spies evs) --> \ \ ExpirServ Tt evs"; +by (etac rev_mp 1); +by (etac rev_mp 1); by (etac kerberos.induct 1); (*The Oops1 case is unusual: must simplify Authkey \\ analz (spies (ev#evs)) rather than weakening it to Authkey \\ analz (spies evs), for we then @@ -784,13 +778,13 @@ (simpset() addsimps [less_SucI, new_keys_not_analzd, Says_Kas_message_form, Says_Tgs_message_form, analz_insert_eq, not_parts_not_analz, - analz_insert_freshK1, analz_insert_freshK2] + analz_insert_freshK1, analz_insert_freshK2, + analz_insert_freshK3] @ pushes))); (*Fake*) by (spy_analz_tac 1); (*K2*) -by (blast_tac (claset() - addIs [parts_insertI, less_SucI]) 1); +by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 1); (*K4*) by (blast_tac (claset() addDs [A_trusts_AuthTicket, Confidentiality_Kas]) 1); by (ALLGOALS Clarify_tac); @@ -799,10 +793,10 @@ Key_unique_SesKey] addIs [less_SucI]) 3); (** Level 10 **) (*Oops1*) -by (blast_tac (claset() addDs [analz_insert_freshK3, - Says_Kas_message_form, Says_Tgs_message_form] - addIs [less_SucI]) 2); -(*K5*) +by (blast_tac (claset() addDs [Says_Kas_message_form, Says_Tgs_message_form] + addIs [less_SucI]) 2); +(*K5. Not clear how this step could be integrated with the main + simplification step.*) by (thin_tac "Says Aa Tgs ?X \\ set ?evs" 1); by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1); by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1); @@ -810,32 +804,31 @@ by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1); by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] addIs [less_SucI]) 1); -val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE); +qed_spec_mp "Confidentiality_lemma"; (* In the real world Tgs can't check wheter AuthKey is secure! *) -Goal - "[| Says Tgs A \ +Goal "[| Says Tgs A \ \ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \ -\ \\ set evs; \ -\ Key AuthKey \\ analz (spies evs); \ -\ ~ ExpirServ Tt evs; \ -\ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ -\ ==> Key ServKey \\ analz (spies evs)"; -by (blast_tac (claset() addDs [Says_Tgs_message_form, lemma]) 1); +\ \\ set evs; \ +\ Key AuthKey \\ analz (spies evs); \ +\ ~ ExpirServ Tt evs; \ +\ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ +\ ==> Key ServKey \\ analz (spies evs)"; +by (blast_tac + (claset() addDs [Says_Tgs_message_form, Confidentiality_lemma]) 1); qed "Confidentiality_Tgs1"; (* In the real world Tgs CAN check what Kas sends! *) -Goal - "[| Says Kas A \ +Goal "[| Says Kas A \ \ (Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|}) \ -\ \\ set evs; \ -\ Says Tgs A \ +\ \\ set evs; \ +\ Says Tgs A \ \ (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \ -\ \\ set evs; \ -\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ -\ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ -\ ==> Key ServKey \\ analz (spies evs)"; +\ \\ set evs; \ +\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ +\ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ +\ ==> Key ServKey \\ analz (spies evs)"; by (blast_tac (claset() addSDs [Confidentiality_Kas, Confidentiality_Tgs1]) 1); qed "Confidentiality_Tgs2"; @@ -891,15 +884,17 @@ Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\ -\ \\ set evs; evs \\ kerberos|] \ -\ ==> \\Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\ +\ \\ set evs; evs \\ kerberos|] \ +\ ==> \\Tk. Says Kas A \ +\ (Crypt (shrK A) \ +\ {|Key AuthKey, Agent Tgs, Number Tk,\ \ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\ -\ \\ set evs"; +\ \\ set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); by Auto_tac; by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS - A_trusts_AuthTicket]) 1); + A_trusts_AuthTicket]) 1); qed "K4_imp_K2"; Goal @@ -913,7 +908,7 @@ by (parts_induct_tac 1); by Auto_tac; by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS - A_trusts_AuthTicket]) 1); + A_trusts_AuthTicket]) 1); qed "K4_imp_K2_refined"; Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|} \ @@ -931,14 +926,16 @@ Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \ \ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ \ evs \\ kerberos |] \ -\ ==> \\AuthKey Tk. Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\ -\ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\ -\ \\ set evs"; +\ ==> \\AuthKey Tk. \ +\ Says Kas A \ +\ (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\ +\ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\ +\ \\ set evs"; by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1); qed "B_trusts_ServTicket_Kas"; Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \ -\ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ +\ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ \ evs \\ kerberos |] \ \ ==> \\AuthKey Tk. (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk,\ \ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}|})\ @@ -948,7 +945,7 @@ qed "B_trusts_ServTicket_Kas_refined"; Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \ -\ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ +\ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ \ evs \\ kerberos |] \ \==> \\Tk AuthKey. \ \ Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \ @@ -961,7 +958,7 @@ qed "B_trusts_ServTicket"; Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \ -\ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ +\ \\ parts (spies evs); B \\ Tgs; B \\ bad; \ \ evs \\ kerberos |] \ \==> \\Tk AuthKey. \ \ (Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, \ @@ -976,7 +973,7 @@ Goal "[| ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk |] \ -\ ==> ~ ExpirAuth Tk evs"; +\ ==> ~ ExpirAuth Tk evs"; by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1); qed "NotExpirServ_NotExpirAuth_refined"; @@ -1133,16 +1130,14 @@ Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|} \ \ \\ parts (spies evs); \ -\ Key AuthKey \\ analz (spies evs); AuthKey \\ range shrK; \ +\ Key AuthKey \\ analz (spies evs); AuthKey \\ range shrK; \ \ evs \\ kerberos |] \ \ ==> \\A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|})\ \ \\ set evs"; by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Blast_tac 1); -by (Blast_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "K4_trustworthy"; Goal "[| Crypt ServKey (Number Ta) \\ parts (spies evs); \ @@ -1209,7 +1204,7 @@ \ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ \ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; by (blast_tac (claset() addSDs [Confidentiality_B, - B_Knows_B_Knows_ServKey_lemma]) 1); + B_Knows_B_Knows_ServKey_lemma]) 1); qed "B_Knows_B_Knows_ServKey"; Goal "[| Says B A (Crypt ServKey (Number Ta)) \\ set evs; \