# HG changeset patch # User paulson # Date 847458836 -3600 # Node ID c5e460f1ebb4336cf77e5dd0cc52f503bf34b747 # Parent 31ba286f2307462a6baf08c02626b31dbe8286d6 Ran expandshort diff -r 31ba286f2307 -r c5e460f1ebb4 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Fri Nov 08 14:07:56 1996 +0100 +++ b/src/HOL/Auth/Message.ML Fri Nov 08 14:13:56 1996 +0100 @@ -664,7 +664,7 @@ \ Key K ~: analz G |] \ \ ==> Crypt Y K : parts G Un parts H"; by (dtac (impOfSubs Fake_parts_insert) 1); -ba 1; +by (assume_tac 1); by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] addss (!simpset)) 1); qed "Crypt_Fake_parts_insert"; diff -r 31ba286f2307 -r c5e460f1ebb4 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Fri Nov 08 14:07:56 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Fri Nov 08 14:13:56 1996 +0100 @@ -70,9 +70,9 @@ (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] addss (!simpset)) 2)) THEN (*Base case*) fast_tac (!claset addss (!simpset)) 1 THEN @@ -143,10 +143,10 @@ by (parts_induct_tac 1); by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, Suc_leD] - addss (!simpset)))); + addSDs [Says_imp_sees_Spy RS parts.Inj] + addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un, Suc_leD] + addss (!simpset)))); qed_spec_mp "new_nonces_not_seen"; Addsimps [new_nonces_not_seen]; @@ -230,7 +230,7 @@ by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1); by (fast_tac (!claset addEs partsEs addSDs [A_trust_NS2, Says_Server_message_form] - addIs [Says_imp_old_keys] + addIs [Says_imp_old_keys] addss (!simpset)) 1); qed "Says_S_message_form"; @@ -342,7 +342,7 @@ (*Duplicate the assumption*) by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1); by (fast_tac (!claset addSDs [ spec] - delrules [conjI] addss (!simpset)) 1); + delrules [conjI] addss (!simpset)) 1); qed "unique_session_keys"; @@ -373,16 +373,16 @@ (*NS3 and Oops subcases*) (**LEVEL 7 **) by (step_tac (!claset delrules [impCE]) 1); by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); -be conjE 2; +by (etac conjE 2); by (mp_tac 2); (**LEVEL 11 **) by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 2); -ba 3; +by (assume_tac 3); by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2); by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2); (*NS3*) by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 1); -ba 2; +by (assume_tac 2); by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1); by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -460,10 +460,10 @@ by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); (*Contradiction from the assumption Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *) -bd Crypt_imp_invKey_keysFor 1; +by (dtac Crypt_imp_invKey_keysFor 1); (**LEVEL 10**) by (Asm_full_simp_tac 1); -br disjI1 1; +by (rtac disjI1 1); by (thin_tac "?PP-->?QQ" 1); by (case_tac "Ba : lost" 1); by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1); @@ -480,5 +480,5 @@ \ A ~: lost; B ~: lost; evs : ns_shared lost |] \ \ ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs"; by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp] - addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1); + addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1); qed "A_trust_NS4"; diff -r 31ba286f2307 -r c5e460f1ebb4 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Fri Nov 08 14:07:56 1996 +0100 +++ b/src/HOL/Auth/Yahalom.ML Fri Nov 08 14:13:56 1996 +0100 @@ -79,9 +79,9 @@ (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] addss (!simpset)) 2)) THEN (*Base case*) fast_tac (!claset addss (!simpset)) 1 THEN @@ -164,10 +164,10 @@ (*Fake and Oops: these messages send unknown (X) components*) by (EVERY (map (fast_tac - (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] + (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono), + Suc_leD] addss (!simpset))) [3,1])); (*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*) by (fast_tac @@ -340,8 +340,8 @@ by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); (*Oops*) (** LEVEL 6 **) by (fast_tac (!claset delrules [disjE] - addDs [unique_session_keys] - addss (!simpset)) 1); + addDs [unique_session_keys] + addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -465,8 +465,8 @@ REPEAT_DETERM (etac MPair_analz 1) THEN THEN_BEST_FIRST (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1) - (has_fewer_prems 1, size_of_thm) - (Step_tac 1)); + (has_fewer_prems 1, size_of_thm) + (Step_tac 1)); (*Variant useful for proving secrecy of NB*) @@ -496,12 +496,12 @@ dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' mp_tac)); by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2); + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); by (ALLGOALS Asm_simp_tac); by (fast_tac (!claset addss (!simpset)) 1); by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj] - addSIs [parts_insertI] + addSIs [parts_insertI] addSEs partsEs addEs [Says_imp_old_nonces RS less_irrefl] addss (!simpset)) 1); @@ -539,7 +539,7 @@ by (Step_tac 1); by (lost_tac "A" 1); by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS - A_trust_YM3]) 1); + A_trust_YM3]) 1); val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp); @@ -571,7 +571,7 @@ by (Step_tac 1); by (lost_tac "A" 1); by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS - A_trust_YM3]) 1); + A_trust_YM3]) 1); result() RS mp RSN (2, rev_mp); @@ -609,8 +609,8 @@ (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE' assume_tac ORELSE' depth_tac (!claset delrules [conjI] - addSIs [exI, impOfSubs (subset_insertI RS analz_mono), - impOfSubs (Un_upper2 RS analz_mono)]) 2)) i; + addSIs [exI, impOfSubs (subset_insertI RS analz_mono), + impOfSubs (Un_upper2 RS analz_mono)]) 2)) i; (*The only nonces that can be found with the help of session keys are those distributed as nonce NB by the Server. The form of the theorem @@ -628,8 +628,8 @@ (asm_simp_tac (!simpset addsimps ([analz_subset_parts RS contra_subsetD, analz_image_newK, - insert_Key_singleton, insert_Key_image] - @ pushes) + insert_Key_singleton, insert_Key_image] + @ pushes) setloop split_tac [expand_if]))); (*Base*) by (fast_tac (!claset addss (!simpset)) 1); @@ -639,20 +639,20 @@ by (EVERY (map grind_tac [3,2,1])); (*Oops*) by (Full_simp_tac 2); -by (REPEAT ((eresolve_tac [bexE] ORELSE' hyp_subst_tac) 2)); +by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2)); by (simp_tac (!simpset addsimps [insert_Key_image]) 2); by (grind_tac 2); by (fast_tac (!claset delrules [bexI] - addDs [unique_session_keys] - addss (!simpset)) 2); + addDs [unique_session_keys] + addss (!simpset)) 2); (*YM4*) (** LEVEL 11 **) -br (impI RS allI) 1; +by (rtac (impI RS allI) 1); by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN Fast_tac 1); by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1); by (asm_simp_tac (!simpset addsimps [analz_image_newK] - setloop split_tac [expand_if]) 1); + setloop split_tac [expand_if]) 1); (** LEVEL 15 **) by (grind_tac 1); by (REPEAT (dtac not_analz_insert 1)); @@ -661,8 +661,8 @@ THEN REPEAT (assume_tac 1)); by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1); by (fast_tac (!claset delrules [conjI] - addIs [impOfSubs (subset_insertI RS analz_mono)] - addss (!simpset)) 1); + addIs [impOfSubs (subset_insertI RS analz_mono)] + addss (!simpset)) 1); val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard; @@ -679,7 +679,7 @@ by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1); by (dtac Nonce_secrecy 1 THEN assume_tac 1); by (fast_tac (!claset addDs [unique_session_keys] - addss (!simpset)) 1); + addss (!simpset)) 1); val single_Nonce_secrecy = result(); @@ -719,7 +719,7 @@ by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1); (** LEVEL 14 **) by (lost_tac "Aa" 1); -bd (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1; +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1); by (forward_tac [Says_Server_message_form] 3); by (forward_tac [Says_Server_imp_YM2] 4); by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE]))); @@ -727,11 +727,11 @@ (** LEVEL 20 **) by (REPEAT_FIRST hyp_subst_tac); by (lost_tac "Ba" 1); -bd (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1; +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1); by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] addSEs [MPair_parts]) 1); by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); -bd Spy_not_see_encrypted_key 1; +by (dtac Spy_not_see_encrypted_key 1); by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); by (spy_analz_tac 1); (*Oops case*) (** LEVEL 28 **) @@ -740,7 +740,7 @@ by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); by (expand_case_tac "NB = NBa" 1); by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1); -br conjI 1; +by (rtac conjI 1); by (no_nonce_tac 1); (** LEVEL 35 **) by (thin_tac "?PP|?QQ" 1); (*subsumption!*) @@ -769,10 +769,10 @@ by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN dtac B_trusts_YM4_shrK 1); -bd B_trusts_YM4_newK 3; +by (dtac B_trusts_YM4_newK 3); by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); -by (dresolve_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1)); +by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1); qed "B_trust_YM4"; diff -r 31ba286f2307 -r c5e460f1ebb4 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Fri Nov 08 14:07:56 1996 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Fri Nov 08 14:13:56 1996 +0100 @@ -80,9 +80,9 @@ (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] addss (!simpset)) 2)) THEN (*Base case*) fast_tac (!claset addss (!simpset)) 1 THEN @@ -157,16 +157,16 @@ \ length evs <= length evs' --> \ \ newK evs' ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (dresolve_tac [YM4_Key_parts_sees_Spy] 5); +by (dtac YM4_Key_parts_sees_Spy 5); (*YM1, YM2 and YM3*) by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); (*Fake and Oops: these messages send unknown (X) components*) by (EVERY (map (fast_tac - (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] + (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono), + Suc_leD] addss (!simpset))) [3,1])); (*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*) by (fast_tac @@ -307,8 +307,8 @@ by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); (*Oops*) by (fast_tac (!claset delrules [disjE] - addDs [unique_session_keys] - addss (!simpset)) 1); + addDs [unique_session_keys] + addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -392,6 +392,6 @@ \ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \ \ Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \ \ : set_of_list evs"; -be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1; +by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1); by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1); qed "B_trust_YM4";