# HG changeset patch # User paulson # Date 985345805 -3600 # Node ID 72c5997e11451ca27ebc9be1076032a3ed779b47 # Parent 60c6e91f60792e9e917cd4c0098060338602fe85 shortening and streamlining of proofs diff -r 60c6e91f6079 -r 72c5997e1145 src/HOL/Auth/KerberosIV.ML --- a/src/HOL/Auth/KerberosIV.ML Fri Mar 23 10:12:12 2001 +0100 +++ b/src/HOL/Auth/KerberosIV.ML Fri Mar 23 12:10:05 2001 +0100 @@ -3,9 +3,13 @@ Author: Giampaolo Bella, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -The Kerberos protocol, version IV. +The Kerberos protocol, version IV. Proofs streamlined by lcp. *) + +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; + Pretty.setdepth 20; set timing; @@ -95,7 +99,7 @@ Goalw [AuthKeys_def] "K \\ AuthKeys evs ==> Key K \\ used evs"; by (Simp_tac 1); -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "AuthKeys_used"; @@ -104,12 +108,12 @@ (*--For reasoning about the encrypted portion of message K3--*) Goal "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \ \ \\ set evs ==> AuthTicket \\ parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "K3_msg_in_parts_spies"; Goal "Says Kas A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|}) \ \ \\ set evs ==> AuthKey \\ parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Oops_parts_spies1"; Goal "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|}) \ @@ -123,12 +127,12 @@ (*--For reasoning about the encrypted portion of message K5--*) Goal "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\ \ \\ set evs ==> ServTicket \\ parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "K5_msg_in_parts_spies"; Goal "Says Tgs A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})\ \ \\ set evs ==> ServKey \\ parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Oops_parts_spies2"; Goal "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}) \ @@ -141,7 +145,7 @@ Goal "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \\ set evs \ \ ==> Ticket \\ parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Says_ticket_in_parts_spies"; (*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*) @@ -158,13 +162,12 @@ (*Spy never sees another agent's shared key! (unless it's lost at start)*) Goal "evs \\ kerberos ==> (Key (shrK A) \\ parts (spies evs)) = (A \\ bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; Goal "evs \\ kerberos ==> (Key (shrK A) \\ analz (spies evs)) = (A \\ bad)"; -by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset())); +by Auto_tac; qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -181,7 +184,7 @@ (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); (*Others*) -by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); +by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; Addsimps [new_keys_not_used]; @@ -223,7 +226,7 @@ \ ==> SesKey \\ range shrK"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "SesKey_is_session_key"; Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|} \ @@ -234,10 +237,8 @@ \ \\ set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -(*Fake*) -by (Fake_parts_insert_tac 1); -(*K4*) -by (Blast_tac 1); +(*Fake, K4*) +by (ALLGOALS Blast_tac); qed "A_trusts_AuthTicket"; Goal "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}\ @@ -263,13 +264,11 @@ (asm_full_simp_tac (simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert, AuthKeys_empty, AuthKeys_simp]))); -by (blast_tac (claset() addEs spies_partsEs) 1); +by (blast_tac (claset()) 1); by Auto_tac; by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1); -by (blast_tac (claset() addSDs [SesKey_is_session_key] - addEs spies_partsEs) 1); -by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey] - addEs spies_partsEs) 1); +by (blast_tac (claset() addSDs [SesKey_is_session_key]) 1); +by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey]) 1); qed "Says_Tgs_message_form"; (*If a certain encrypted message appears then it originated with Kas*) @@ -281,10 +280,9 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*Fake*) -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*K4*) -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst, - A_trusts_AuthTicket RS Says_Kas_message_form]) +by (blast_tac (claset() addSDs [A_trusts_AuthTicket RS Says_Kas_message_form]) 1); qed "A_trusts_AuthKey"; @@ -301,7 +299,7 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*Fake*) -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*K2*) by (Blast_tac 1); (*K4*) @@ -316,8 +314,7 @@ \ AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "AuthTicket_form"; (* This form holds also over an AuthTicket, but is not needed below. *) @@ -330,7 +327,7 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "ServTicket_form"; Goal "[| Says Kas' A (Crypt (shrK A) \ @@ -340,10 +337,8 @@ \ AuthTicket = \ \ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}\ \ | AuthTicket \\ analz (spies evs)"; -by (case_tac "A \\ bad" 1); -by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1); -by (forward_tac [Says_imp_spies RS parts.Inj] 1); -by (blast_tac (claset() addSDs [AuthTicket_form]) 1); +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, + AuthTicket_form]) 1); qed "Says_kas_message_form"; (* Essentially the same as AuthTicket_form *) @@ -354,10 +349,8 @@ \ (\\A. ServTicket = \ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) \ \ | ServTicket \\ analz (spies evs)"; -by (case_tac "Key AuthKey \\ analz (spies evs)" 1); -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1); -by (forward_tac [Says_imp_spies RS parts.Inj] 1); -by (blast_tac (claset() addSDs [ServTicket_form]) 1); +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, + ServTicket_form]) 1); qed "Says_tgs_message_form"; (* This form MUST be used in analz_sees_tac below *) @@ -379,8 +372,7 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*Fake, K2, K4*) -by (Fake_parts_insert_tac 1); -by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); +by (ALLGOALS Blast_tac); qed "unique_CryptKey"; (*An AuthKey is encrypted by one and only one Shared key. @@ -397,8 +389,7 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*Fake, K2, K4*) -by (Fake_parts_insert_tac 1); -by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); +by (ALLGOALS Blast_tac); qed "Key_unique_SesKey"; @@ -429,7 +420,7 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*K2*) -by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); +by (Blast_tac 1); qed "unique_AuthKeys"; (* ServKey uniquely identifies the message from Tgs *) @@ -442,7 +433,7 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*K4*) -by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); +by (Blast_tac 1); qed "unique_ServKeys"; @@ -457,9 +448,7 @@ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \ \ \\ set evs; \ \ evs \\ kerberos |] ==> KeyCryptKey AuthKey ServKey evs"; -by (ftac Says_Tgs_message_form 1); -by (assume_tac 1); -by (Blast_tac 1); +by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); qed "KeyCryptKeyI"; Goalw [KeyCryptKey_def] @@ -482,14 +471,14 @@ by (etac rev_mp 1); by (parts_induct_tac 1); by (Asm_full_simp_tac 1); -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Auth_fresh_not_KeyCryptKey"; (*A fresh ServKey cannot be associated with any other (with respect to a given trace). *) Goalw [KeyCryptKey_def] "Key ServKey \\ used evs ==> ~ KeyCryptKey AuthKey ServKey evs"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Serv_fresh_not_KeyCryptKey"; Goal @@ -499,11 +488,10 @@ by (etac rev_mp 1); by (parts_induct_tac 1); (*K4*) -by (blast_tac (claset() addEs spies_partsEs) 3); +by (Blast_tac 3); (*K2: by freshness*) by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); -by (blast_tac (claset() addEs spies_partsEs) 2); -by (Fake_parts_insert_tac 1); +by (ALLGOALS Blast_tac); qed "AuthKey_not_KeyCryptKey"; (*A secure serverkey cannot have been used to encrypt others*) @@ -515,19 +503,14 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*K4 splits into distinct subcases*) by Auto_tac; (*ServKey can't have been enclosed in two certificates*) -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] - addSEs [MPair_parts] - addDs [unique_CryptKey]) 4); +by (blast_tac (claset() addDs [unique_CryptKey]) 2); (*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, - Crypt_imp_invKey_keysFor], - simpset() addsimps [KeyCryptKey_def]) 2); -(*Others by freshness*) -by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); +by (force_tac (claset() addSDs [Crypt_imp_invKey_keysFor], + simpset() addsimps [KeyCryptKey_def]) 1); qed "ServKey_not_KeyCryptKey"; (*Long term keys are not issued as ServKeys*) @@ -553,14 +536,13 @@ by (Step_tac 1); by (ALLGOALS Asm_full_simp_tac); (*K4 splits into subcases*) -by (blast_tac (claset() addEs spies_partsEs - addSDs [AuthKey_not_KeyCryptKey]) 4); +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, Crypt_imp_invKey_keysFor], - simpset() addsimps [KeyCryptKey_def]) 2); + simpset() addsimps [KeyCryptKey_def]) 2); (*Others by freshness*) -by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); +by (ALLGOALS Blast_tac); qed "KeyCryptKey_not_KeyCryptKey"; (*The only session keys that can be found with the help of session keys are @@ -648,8 +630,7 @@ (*K3*) by (Blast_tac 1); (*K4*) -by (blast_tac (claset() addEs spies_partsEs - addSDs [AuthKey_not_KeyCryptKey]) 1); +by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 1); (*K5*) by (case_tac "Key ServKey \\ analz (spies evs5)" 1); (*If ServKey is compromised then the result follows directly...*) @@ -659,7 +640,7 @@ (*...therefore ServKey is uncompromised.*) (*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*) by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)] - addEs spies_partsEs delrules [allE, ballE]) 1); + delrules [allE, ballE]) 1); (** Level 13: Oops1 **) by (Asm_full_simp_tac 1); by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1); @@ -728,8 +709,7 @@ by (etac rev_mp 1); by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); +by (ALLGOALS Blast_tac); bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE)); bind_thm ("ServKey_notin_AuthKeysD", result()); @@ -754,17 +734,15 @@ (*Fake*) by (spy_analz_tac 1); (*K2*) -by (blast_tac (claset() addSEs spies_partsEs - addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1); +by (Blast_tac 1); (*K4*) -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); (*Level 8: K5*) by (blast_tac (claset() addEs [ServKey_notin_AuthKeys] - addDs [Says_Kas_message_form, - Says_imp_spies RS parts.Inj] + addDs [Says_Kas_message_form] addIs [less_SucI]) 1); (*Oops1*) -by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1); +by (blast_tac (claset() addSDs [unique_AuthKeys] addIs [less_SucI]) 1); (*Oops2*) by (blast_tac (claset() addDs [Says_Tgs_message_form, Says_Kas_message_form]) 1); @@ -777,8 +755,7 @@ \ ~ ExpirAuth Tk evs; \ \ A \\ bad; evs \\ kerberos |] \ \ ==> Key AuthKey \\ analz (spies evs)"; -by (ftac Says_Kas_message_form 1 THEN assume_tac 1); -by (blast_tac (claset() addSDs [lemma]) 1); +by (blast_tac (claset() addDs [Says_Kas_message_form, lemma]) 1); qed "Confidentiality_Kas"; @@ -812,37 +789,27 @@ (*Fake*) by (spy_analz_tac 1); (*K2*) -by (blast_tac (claset() addSEs spies_partsEs +by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 1); (*K4*) -by (case_tac "A \\ Aa" 1); -by (blast_tac (claset() addSEs spies_partsEs - addIs [less_SucI]) 1); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst, - A_trusts_AuthTicket, - Confidentiality_Kas, - impOfSubs analz_subset_parts]) 1); +by (blast_tac (claset() addDs [A_trusts_AuthTicket, Confidentiality_Kas]) 1); by (ALLGOALS Clarify_tac); (*Oops2*) by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] addIs [less_SucI]) 3); -(** Level 12 **) +(** Level 10 **) (*Oops1*) -by (ftac Says_Kas_message_form 2); -by (assume_tac 2); by (blast_tac (claset() addDs [analz_insert_freshK3, Says_Kas_message_form, Says_Tgs_message_form] addIs [less_SucI]) 2); -(** Level 16 **) +(*K5*) 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); by (rotate_tac ~1 1); by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1); -by (etac disjE 1); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, - Key_unique_SesKey]) 1); -by (blast_tac (claset() addIs [less_SucI]) 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); @@ -855,8 +822,7 @@ \ ~ ExpirServ Tt evs; \ \ A \\ bad; B \\ bad; B \\ Tgs; evs \\ kerberos |] \ \ ==> Key ServKey \\ analz (spies evs)"; -by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); -by (blast_tac (claset() addDs [lemma]) 1); +by (blast_tac (claset() addDs [Says_Tgs_message_form, lemma]) 1); qed "Confidentiality_Tgs1"; (* In the real world Tgs CAN check what Kas sends! *) @@ -896,10 +862,9 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*K2 and K4 remain*) -by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts] - addSDs [unique_CryptKey]) 2); +by (blast_tac (claset() addSDs [unique_CryptKey]) 2); by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, AuthKeys_used]) 1); qed "A_trusts_K4_bis"; @@ -960,8 +925,7 @@ \ \\ set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "B_trusts_ServKey"; Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \ @@ -993,11 +957,7 @@ \ & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \ \ \\ set evs"; -by (ftac B_trusts_ServKey 1); -by (etac exE 4); -by (ftac K4_imp_K2 4); -by (Blast_tac 5); -by (ALLGOALS assume_tac); +by (blast_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2]) 1); qed "B_trusts_ServTicket"; Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} \ @@ -1011,11 +971,7 @@ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \ \ \\ set evs \ \ & ServLife + Tt <= AuthLife + Tk)"; -by (ftac B_trusts_ServKey 1); -by (etac exE 4); -by (ftac K4_imp_K2_refined 4); -by (Blast_tac 5); -by (ALLGOALS assume_tac); +by (blast_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2_refined]) 1); qed "B_trusts_ServTicket_refined"; @@ -1037,15 +993,12 @@ by (ftac A_trusts_AuthKey 1); by (ftac Confidentiality_Kas 3); by (ftac B_trusts_ServTicket 6); -by (etac exE 9); -by (etac exE 9); -by (ftac Says_Kas_message_form 9); -by (blast_tac (claset() addDs [A_trusts_K4, - unique_ServKeys, unique_AuthKeys, - Confidentiality_Tgs2]) 10); +by (blast_tac (claset() addSDs [Confidentiality_Tgs2] + addDs [Says_Kas_message_form, A_trusts_K4, + unique_ServKeys, unique_AuthKeys]) 9); by (ALLGOALS assume_tac); (* -The proof above executes in 8 secs. It can be done in one command in 50 secs: +The proof above is fast. It can be done in one command in 50 secs: by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4, Says_Kas_message_form, B_trusts_ServTicket, unique_ServKeys, unique_AuthKeys, @@ -1081,8 +1034,8 @@ \ ~ ExpirAuth Tk evs; A \\ bad; evs \\ kerberos |] \ \==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\ \ \\ set evs"; -by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1); -by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1); +by (blast_tac (claset() addDs [A_trusts_AuthKey, Confidentiality_Auth_A, + A_trusts_K4_bis]) 1); qed "A_trusts_ServKey"; (*Note: requires a temporal check*) @@ -1112,16 +1065,15 @@ by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*K3*) -by (blast_tac (claset() addEs spies_partsEs - addDs [A_trusts_AuthKey, +by (blast_tac (claset() addDs [A_trusts_AuthKey, Says_Kas_message_form, Says_Tgs_message_form]) 1); (*K4*) by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); (*K5*) -by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1); +by (blast_tac (claset() addDs [Key_unique_SesKey]) 1); qed "Says_Auth"; (*The second assumption tells B what kind of key ServKey is.*) @@ -1136,12 +1088,9 @@ \ B \\ Tgs; A \\ bad; B \\ bad; evs \\ kerberos |] \ \ ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\ \ Crypt ServKey {|Agent A, Number Ta|} |} \\ set evs"; -by (ftac Confidentiality_B 1); -by (ftac B_trusts_ServKey 9); -by (etac exE 12); -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] - addSIs [Says_Auth]) 12); -by (ALLGOALS assume_tac); +by (blast_tac (claset() addIs [Says_Auth] + addDs [Confidentiality_B, Key_unique_SesKey, + B_trusts_ServKey]) 1); qed "A_Authenticity"; (*Stronger form in the refined model*) @@ -1152,12 +1101,9 @@ \ B \\ Tgs; A \\ bad; B \\ bad; evs \\ kerberos |] \ \ ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\ \ Crypt ServKey {|Agent A, Number Ta2|} |} \\ set evs"; -by (ftac Confidentiality_B_refined 1); -by (ftac B_trusts_ServKey 6); -by (etac exE 9); -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] - addSIs [Says_Auth]) 9); -by (ALLGOALS assume_tac); +by (blast_tac (claset() addDs [Confidentiality_B_refined, B_trusts_ServKey, + Key_unique_SesKey] + addIs [Says_Auth]) 1); qed "A_Authenticity_refined"; @@ -1177,12 +1123,12 @@ by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS Asm_simp_tac); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); by (Clarify_tac 1); by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); by (Clarify_tac 1); (*PROOF FAILED if omitted*) -by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1); +by (blast_tac (claset() addDs [unique_CryptKey]) 1); qed "Says_K6"; Goal "[| Crypt AuthKey {|Key ServKey, Agent B, T, ServTicket|} \ @@ -1194,7 +1140,7 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (Blast_tac 1); by (Blast_tac 1); qed "K4_trustworthy"; @@ -1214,9 +1160,10 @@ by (Blast_tac 8); by (etac exE 9); by (ftac K4_imp_K2 9); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] +(*Yes the proof's a mess, but I don't know how to improve it.*) +by (blast_tac (claset() addDs [Key_unique_SesKey] addSIs [Says_K6] - addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10); + addDs [Confidentiality_Tgs1]) 10); by (ALLGOALS assume_tac); qed "B_Authenticity"; @@ -1240,14 +1187,13 @@ by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*K6 requires numerous lemmas*) by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); by (blast_tac (claset() addDs [B_trusts_ServTicket, impOfSubs parts_spies_takeWhile_mono, impOfSubs parts_spies_evs_revD2] - addIs [Says_K6] - addEs spies_partsEs) 1); + addIs [Says_K6]) 1); qed "B_Knows_B_Knows_ServKey_lemma"; (*Key ServKey \\ analz (spies evs) could be relaxed by Confidentiality_B but this is irrelevant because B knows what he knows! *) @@ -1298,7 +1244,7 @@ \ \\ set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (Blast_tac 1); by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS A_trusts_AuthKey]) 1); @@ -1318,7 +1264,7 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_AuthTicket, unique_AuthKeys]) 1); @@ -1347,15 +1293,11 @@ by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); (*Level 15: case study necessary because the assumption doesn't state the form of ServTicket. The guarantee becomes stronger.*) -by (case_tac "Key AuthKey \\ analz (spies evs5)" 1); -by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS - analz.Decrypt RS analz.Fst], - simpset()) 1); -by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy', +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz_Decrypt', + K3_imp_K2, K4_trustworthy', impOfSubs parts_spies_takeWhile_mono, impOfSubs parts_spies_evs_revD2] - addIs [Says_Auth] - addEs spies_partsEs) 1); + addIs [Says_Auth]) 1); by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); qed "A_Knows_A_Knows_ServKey_lemma";