--- a/src/HOL/Auth/NS_Public.ML Thu Sep 25 12:13:18 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Thu Sep 25 12:14:41 1997 +0200
@@ -95,7 +95,7 @@
(*Unicity for NS1: nonce NA identifies agents A and B*)
goal thy
"!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \
-\ ==> EX A' B'. ALL A B. \
+\ ==> EX A' B'. ALL A B. \
\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
\ A=A' & B=B'";
by (etac rev_mp 1);
@@ -105,7 +105,7 @@
(*NS1*)
by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
-by (step_tac (!claset addSIs [analz_insertI]) 1);
+by (Clarify_tac 1);
by (ex_strip_tac 1);
by (Fake_parts_insert_tac 1);
val lemma = result();
@@ -191,8 +191,8 @@
[unicity of B makes Lowe's fix work]
[proof closely follows that for unique_NA] *)
goal thy
- "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \
-\ ==> EX A' NA' B'. ALL A NA B. \
+ "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \
+\ ==> EX A' NA' B'. ALL A NA B. \
\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
\ --> A=A' & NA=NA' & B=B'";
by (etac rev_mp 1);
@@ -202,17 +202,17 @@
(*NS2*)
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
(*Fake*)
-by (step_tac (!claset addSIs [analz_insertI]) 1);
+by (Clarify_tac 1);
by (ex_strip_tac 1);
by (Fake_parts_insert_tac 1);
val lemma = result();
goal thy
"!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \
-\ : parts(spies evs); \
+\ : parts(spies evs); \
\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
-\ : parts(spies evs); \
-\ Nonce NB ~: analz (spies evs); \
+\ : parts(spies evs); \
+\ Nonce NB ~: analz (spies evs); \
\ evs : ns_public |] \
\ ==> A=A' & NA=NA' & B=B'";
by (prove_unique_tac lemma 1);
@@ -229,16 +229,15 @@
by (analz_induct_tac 1);
(*NS3*)
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
+(*NS2: by freshness and unicity of NB*)
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
+ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
+ addEs partsEs
+ addIs [impOfSubs analz_subset_parts]) 3);
(*NS1*)
by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
-(*NS2*)
-by (Step_tac 1);
-by (blast_tac (!claset addSEs spies_partsEs) 3);
-by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
-by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
qed "Spy_not_see_NB";
@@ -254,16 +253,16 @@
(*prepare induction over Crypt (pubK B) NB : parts H*)
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (parts_induct_tac 1);
-(*NS1*)
+by (ALLGOALS Clarify_tac);
+(*NS3: because NB determines A*)
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
+ Spy_not_see_NB, unique_NB]) 3);
+(*NS1: by freshness*)
by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
addDs [Spy_not_see_NB,
impOfSubs analz_subset_parts]) 1);
-(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
-by (Step_tac 1);
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
- Spy_not_see_NB, unique_NB]) 1);
qed "B_trusts_NS3";
@@ -287,20 +286,15 @@
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
-(*Fake, NS2, NS3*)
+by (ALLGOALS Clarify_tac);
+(*NS3: because NB determines A*)
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
+ Spy_not_see_NB, unique_NB]) 3);
(*NS1*)
by (blast_tac (!claset addSEs spies_partsEs) 2);
(*Fake*)
-by (REPEAT_FIRST (resolve_tac [impI, conjI]));
-by (Blast_tac 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addSIs [disjI2]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
-(*NS3*)
-by (Step_tac 1);
-by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
-by (blast_tac (!claset addSDs [Says_imp_spies' RS parts.Inj]
- addDs [unique_NB]) 1);
+by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+ addDs [Spy_not_see_NB,
+ impOfSubs analz_subset_parts]) 1);
qed "B_trusts_protocol";