--- a/src/HOL/Auth/Message.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Message.ML Mon Sep 29 11:47:01 1997 +0200
@@ -28,7 +28,7 @@
(** Inverse of keys **)
goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
-by (Step_tac 1);
+by Safe_tac;
by (rtac box_equals 1);
by (REPEAT (rtac invKey 2));
by (Asm_simp_tac 1);
@@ -135,7 +135,7 @@
val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
goal thy "parts{} = {}";
-by (Step_tac 1);
+by Safe_tac;
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
qed "parts_empty";
@@ -373,7 +373,7 @@
(** General equational properties **)
goal thy "analz{} = {}";
-by (Step_tac 1);
+by Safe_tac;
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
qed "analz_empty";
@@ -554,7 +554,7 @@
(*If there are no pairs or encryptions then analz does nothing*)
goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \
\ analz H = H";
-by (Step_tac 1);
+by Safe_tac;
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
qed "analz_trivial";
--- a/src/HOL/Auth/NS_Shared.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Mon Sep 29 11:47:01 1997 +0200
@@ -230,7 +230,7 @@
\ --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by Safe_tac;
(*NS3*)
by (ex_strip_tac 2);
by (Blast_tac 2);
@@ -278,7 +278,7 @@
(*Fake*)
by (spy_analz_tac 1);
(*NS3, Server sub-case*) (**LEVEL 6 **)
-by (step_tac (!claset delrules [impCE]) 1);
+by (clarify_tac (!claset delrules [impCE]) 1);
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
by (assume_tac 2);
by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
--- a/src/HOL/Auth/OtwayRees.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Mon Sep 29 11:47:01 1997 +0200
@@ -196,7 +196,7 @@
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
(*Remaining cases: OR3 and OR4*)
by (ex_strip_tac 2);
by (Best_tac 2);
@@ -286,22 +286,21 @@
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
-(*OR3 and OR4*)
-(*OR4*)
-by (REPEAT (Safe_step_tac 2));
-by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
-by (blast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs spies_partsEs) 2);
-(*OR3*) (** LEVEL 5 **)
+(*OR3 and OR4*)
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
-by (step_tac (!claset delrules [disjCI, impCE]) 1);
+by (rtac conjI 1);
+by (ALLGOALS Clarify_tac);
+(*OR4*)
+by (blast_tac (!claset addSIs [Crypt_imp_OR1]
+ addEs spies_partsEs) 3);
+(*OR3, two cases*) (** LEVEL 5 **)
by (blast_tac (!claset addSEs [MPair_parts]
- addSDs [Says_imp_spies RS parts.Inj]
- addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)]
- delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
+ addSDs [Says_imp_spies RS parts.Inj]
+ addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)]
+ delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
- addSEs [MPair_parts]
- addIs [unique_NA]) 1);
+ addSEs [MPair_parts]
+ addIs [unique_NA]) 1);
qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -426,7 +425,7 @@
(*OR4*)
by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
(*OR3*)
-by (step_tac (!claset delrules [disjCI, impCE]) 1);
+by (safe_tac (!claset delrules [disjCI, impCE]));
by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3);
by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
--- a/src/HOL/Auth/OtwayRees_AN.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Mon Sep 29 11:47:01 1997 +0200
@@ -190,7 +190,7 @@
\ --> A=A' & B=B' & NA=NA' & NB=NB'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
(*Remaining cases: OR3 and OR4*)
by (ex_strip_tac 2);
by (Blast_tac 2);
--- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Mon Sep 29 11:47:01 1997 +0200
@@ -199,7 +199,7 @@
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
(*Remaining cases: OR3 and OR4*)
by (ex_strip_tac 2);
by (Blast_tac 2);
@@ -290,26 +290,25 @@
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (blast_tac (!claset addSIs [parts_insertI]
- addSEs spies_partsEs) 1);
+ addSEs spies_partsEs) 1);
+(*OR3 and OR4*)
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
+by (ALLGOALS Clarify_tac);
(*OR4*)
-by (REPEAT (Safe_step_tac 2));
-by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
by (blast_tac (!claset addSIs [Crypt_imp_OR1]
addEs spies_partsEs) 2);
(*OR3*) (** LEVEL 5 **)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
-by (step_tac (!claset delrules [disjCI, impCE]) 1);
-(*The hypotheses at this point suggest an attack in which nonce NA is used
+(*The hypotheses at this point suggest an attack in which nonce NB is used
in two different roles:
Says B' Server
- {|Nonce NAa, Agent Aa, Agent A,
- Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
- Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
- : set evsa;
+ {|Nonce NA, Agent Aa, Agent A,
+ Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
+ Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
+ : set evs3;
Says A B
- {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
- : set evsa
+ {|Nonce NB, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
+ : set evs3;
*)
writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
--- a/src/HOL/Auth/Public.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Public.ML Mon Sep 29 11:47:01 1997 +0200
@@ -16,7 +16,7 @@
AddIffs [inj_pubK RS inj_eq];
goal thy "!!A B. (priK A = priK B) = (A=B)";
-by (Step_tac 1);
+by Safe_tac;
by (dres_inst_tac [("f","invKey")] arg_cong 1);
by (Full_simp_tac 1);
qed "priK_inj_eq";
@@ -89,7 +89,7 @@
THEN_BEST_FIRST
(dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
(has_fewer_prems 1, size_of_thm)
- (Step_tac 1));
+ Safe_tac);
(*** Fresh nonces ***)
@@ -115,7 +115,7 @@
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [used_Cons]
setloop split_tac [expand_event_case, expand_if])));
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
val lemma = result();
--- a/src/HOL/Auth/Recur.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Mon Sep 29 11:47:01 1997 +0200
@@ -303,7 +303,7 @@
by (Fake_parts_insert_tac 1);
by (etac responses.induct 3);
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
-by (step_tac (!claset addSEs partsEs) 1);
+by (clarify_tac (!claset addSEs partsEs) 1);
(*RA1,2: creation of new Nonce. Move assertion into global context*)
by (ALLGOALS (expand_case_tac "NA = ?y"));
by (REPEAT_FIRST (ares_tac [exI]));
@@ -388,7 +388,7 @@
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib])));
(*Base case*)
by (Blast_tac 1);
-by (Step_tac 1);
+by Safe_tac;
by (expand_case_tac "K = KBC" 1);
by (dtac respond_Key_in_parts 1);
by (blast_tac (!claset addSIs [exI]
@@ -429,7 +429,7 @@
by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib])));
(** LEVEL 5 **)
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
-by (step_tac (!claset addSEs [MPair_parts]) 1);
+by (safe_tac (!claset addSEs [MPair_parts]));
by (REPEAT (blast_tac (!claset addSDs [respond_certificate]
addDs [resp_analz_insert]
addIs [impOfSubs analz_subset_parts]) 4));
@@ -446,14 +446,15 @@
goal thy
"!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
-\ A ~: bad; A' ~: bad; evs : recur |] \
+\ A ~: bad; A' ~: bad; evs : recur |] \
\ ==> Key K ~: analz (spies evs)";
by (etac rev_mp 1);
by (etac recur.induct 1);
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [parts_insert_spies, analz_insert_freshK]
+ (!simpset addsimps [analz_insert_eq, parts_insert_spies,
+ analz_insert_freshK]
setloop split_tac [expand_if])));
(*RA4*)
by (spy_analz_tac 5);
@@ -464,11 +465,11 @@
(*Base*)
by (Blast_tac 1);
(*RA3 remains*)
-by (step_tac (!claset delrules [impCE]) 1);
+by (safe_tac (!claset delrules [impCE]));
(*RA3, case 2: K is an old key*)
by (blast_tac (!claset addSDs [resp_analz_insert]
addSEs partsEs
- addDs [Key_in_parts_respond]) 2);
+ addDs [Key_in_parts_respond]) 2);
(*RA3, case 1: use lemma previously proved by induction*)
by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
(2,rev_notE)]) 1);
--- a/src/HOL/Auth/Shared.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Mon Sep 29 11:47:01 1997 +0200
@@ -112,7 +112,7 @@
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [used_Cons]
setloop split_tac [expand_event_case, expand_if])));
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
val lemma = result();
--- a/src/HOL/Auth/WooLam.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML Mon Sep 29 11:47:01 1997 +0200
@@ -175,6 +175,6 @@
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
-by (Step_tac 1);
+by Safe_tac;
by (blast_tac (!claset addSEs partsEs) 1);
**)
--- a/src/HOL/Auth/Yahalom2.ML Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Mon Sep 29 11:47:01 1997 +0200
@@ -190,7 +190,7 @@
\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
by (etac yahalom.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (Clarify_tac 1);
(*Remaining case: YM3*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));