# HG changeset patch
# User paulson
# Date 875182481 -7200
# Node ID c13c2137e9ee23c97b0e4643885795ad2f79dc2e
# Parent  56facaebf3e38fdf16ae04583444a2112b581790
Tidied proofs, using Clarify_tac

diff -r 56facaebf3e3 -r c13c2137e9ee 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";
 
diff -r 56facaebf3e3 -r c13c2137e9ee src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Sep 25 12:13:18 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Sep 25 12:14:41 1997 +0200
@@ -98,7 +98,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);
@@ -108,7 +108,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();
@@ -117,7 +117,7 @@
  "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
 \           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
 \           Nonce NA ~: analz (spies evs);                            \
-\           evs : ns_public |]                                           \
+\           evs : ns_public |]                                        \
 \        ==> A=A' & B=B'";
 by (prove_unique_tac lemma 1);
 qed "unique_NA";
@@ -132,7 +132,7 @@
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
 goal thy 
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;     \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;   \
 \           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
 \        ==>  Nonce NA ~: analz (spies evs)";
 by (etac rev_mp 1);
@@ -157,30 +157,30 @@
 goal thy 
  "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
 \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;  \
-\           A ~: bad;  B ~: bad;  evs : ns_public |]                  \
+\           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
 \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS Clarify_tac);
+(*NS2*)
+by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
+			      Spy_not_see_NA, unique_NA]) 3);
 (*NS1*)
 by (blast_tac (!claset addSEs spies_partsEs) 2);
 (*Fake*)
 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
                        addDs  [Spy_not_see_NA, 
 			       impOfSubs analz_subset_parts]) 1);
-(*NS2; 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_NA, unique_NA]) 1);
 qed "A_trusts_NS2";
 
 (*If the encrypted message appears then it originated with Alice in NS1*)
 goal thy 
  "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
 \           Nonce NA ~: analz (spies evs);                            \
-\           evs : ns_public |]                                           \
+\           evs : ns_public |]                                        \
 \   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
@@ -196,8 +196,8 @@
   [proof closely follows that for unique_NA] *)
 goal thy 
  "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]  \
-\ ==> EX A' NA'. ALL A NA.                                         \
-\      Crypt (pubK A) {|Nonce NA, Nonce NB|}                       \
+\ ==> EX A' NA'. ALL A NA.                                      \
+\      Crypt (pubK A) {|Nonce NA, Nonce NB|}                    \
 \        : parts (spies evs)  -->  A=A' & NA=NA'";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
@@ -206,7 +206,7 @@
 (*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();
@@ -215,7 +215,7 @@
  "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(spies evs); \
 \           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \
 \           Nonce NB ~: analz (spies evs);                            \
-\           evs : ns_public |]                                           \
+\           evs : ns_public |]                                        \
 \        ==> A=A' & NA=NA'";
 by (prove_unique_tac lemma 1);
 qed "unique_NB";
@@ -231,7 +231,7 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by clarify_tac;
+by (ALLGOALS Clarify_tac);
 (*NS3: because NB determines A*)
 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
 (*NS2: by freshness and unicity of NB*)
@@ -259,7 +259,7 @@
 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
 by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
-by clarify_tac;
+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);
@@ -278,7 +278,7 @@
 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
 \     --> Nonce NB ~: analz (spies evs)";
 by (analz_induct_tac 1);
-by clarify_tac;
+by (ALLGOALS Clarify_tac);
 (*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)]