# HG changeset patch # User paulson # Date 898523369 -7200 # Node ID 77bd19f782e6526c07f332dbe8ca2a1c234db08a # Parent d45ec8d00ab031eaacf6a306560b77f1cf67538a simplified and tidied the proofs diff -r d45ec8d00ab0 -r 77bd19f782e6 src/HOL/Auth/Kerberos_BAN.ML --- a/src/HOL/Auth/Kerberos_BAN.ML Mon Jun 22 15:25:06 1998 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.ML Mon Jun 22 15:49:29 1998 +0200 @@ -8,6 +8,8 @@ From page 251 of Burrows, Abadi and Needham. A Logic of Authentication. Proc. Royal Soc. 426 (1989) + +Tidied by lcp. *) open Kerberos_BAN; @@ -27,9 +29,7 @@ AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; -AddSIs [SesKeyLife_LB, AutLife_LB]; - -Addsimps [SesKeyLife_LB, AutLife_LB]; +AddIffs [SesKeyLife_LB, AutLife_LB]; (*A "possibility property": there are traces that reach the end.*) @@ -263,41 +263,29 @@ **) goal thy - "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] \ -\ ==> Says Server A \ -\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ -\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ -\ : set evs --> \ + "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |] \ +\ ==> Says Server A \ +\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ +\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ +\ : set evs --> \ \ Key K : analz (spies evs) --> Expired Ts evs"; by (etac kerberos_ban.induct 1); by analz_spies_tac; by (ALLGOALS - (asm_simp_tac (simpset() - addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes @ split_ifs)))); + (asm_simp_tac (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] + @ pushes)))); (*Oops*) by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4); (*Kb2*) -by (fast_tac (claset() addIs [parts_insertI, less_SucI]) 2); +by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2); (*Fake*) by (spy_analz_tac 1); (**LEVEL 6 **) -by (clarify_tac (claset() delrules [impCE]) 1); -by (case_tac "Ba : bad" 1); -by (blast_tac (claset() addIs [less_SucI]) 2); -(**LEVEL 9**) -by (rotate_tac 10 1); -by (forward_tac [mp] 1 THEN assume_tac 1); -by (etac disjE 1); -by (blast_tac (claset() addIs [less_SucI]) 2); -(**LEVEL 13**) -by (Clarify_tac 1); +(*Kb3*) by (case_tac "Aa : bad" 1); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, - A_trusts_K_by_Kb2, unique_session_keys]) 2); -(**LEVEL 16**) -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS - Crypt_Spy_analz_bad RS analz.Snd RS - analz.Snd RS analz.Fst] +by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2); +by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, + Crypt_Spy_analz_bad, analz.Fst, analz.Snd] addIs [less_SucI]) 1); val lemma = result() RS mp RS mp RSN(1,rev_notE); @@ -313,8 +301,7 @@ \ A ~: bad; B ~: bad; evs : kerberos_ban \ \ |] ==> Key K ~: analz (spies evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); -by (Clarify_tac 1); -by (rtac ccontr 1); +by (Clarify_tac 1); (*prevents PROOF FAILED*) by (blast_tac (claset() addSEs [lemma]) 1); qed "Confidentiality_S"; @@ -330,8 +317,7 @@ \ ~ Expired T evs; \ \ A ~: bad; B ~: bad; evs : kerberos_ban \ \ |] ==> Key K ~: analz (spies evs)"; -by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, - Confidentiality_S]) 1); +by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1); qed "Confidentiality_A"; @@ -359,21 +345,18 @@ by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); by (dtac Kb3_msg_in_parts_spies 5); by (forward_tac [Oops_parts_spies] 7); -by (TRYALL (rtac impI)); -by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD))); +by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -(**LEVEL 7**) +(**LEVEL 6**) by (Blast_tac 1); -by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); +by (Clarify_tac 1); (* Subgoal 1: contradiction from the assumptions Key K ~: used evs2 and Crypt K (Number Ta) : parts (spies evs2) *) by (dtac Crypt_imp_invKey_keysFor 1); by (Asm_full_simp_tac 1); -(* the two tactics above detectthe contradiction*) -by (rtac disjI1 1); -by (thin_tac "?PP-->?QQ" 1); (*deletes the matching assumptions*) +(* the two tactics above detect the contradiction*) by (case_tac "Ba : bad" 1); (*splits up the subgoal by the stated case*) by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS B_trusts_K_by_Kb3, @@ -409,39 +392,24 @@ by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); by (forward_tac [Kb3_msg_in_parts_spies] 5); by (forward_tac [Oops_parts_spies] 7); -by (TRYALL (rtac impI)); -by (REPEAT_FIRST (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD))); +by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -(**LEVEL 7**) +(**LEVEL 6**) by (Blast_tac 1); -by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); +by (Clarify_tac 1); by (dtac Crypt_imp_invKey_keysFor 1); by (Asm_full_simp_tac 1); -by (rtac disjI1 1); -(*Last Subgoal! ...to be refined...*) -by (thin_tac "Says ?A Server ?X : set evs3" 1); -by (dresolve_tac [Says_imp_spies RS parts.Inj] 1); -by (dresolve_tac [Says_imp_spies RS parts.Inj] 1); -by (dtac A_trusts_K_by_Kb2 1); -by (assume_tac 1); -by (assume_tac 1); -by (dtac A_trusts_K_by_Kb2 1); -by (assume_tac 1); -by (assume_tac 1); -by (dtac unique_session_keys 1); -by (assume_tac 1); -by (assume_tac 1); -by (Blast_tac 1); +by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1); val lemma_A = result(); (*AUTHENTICATION OF A TO B*) goal thy - "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \ -\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ -\ : parts (spies evs); \ -\ ~ Expired Ts evs; \ -\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ + "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \ +\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ +\ : parts (spies evs); \ +\ ~ Expired Ts evs; \ +\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ \ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \ \ Crypt K {|Agent A, Number Ta|}|} : set evs"; by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]