src/HOL/Auth/NS_Public.ML

--- 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";