src/HOL/Auth/Yahalom.ML

--- a/src/HOL/Auth/Yahalom.ML	Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Tue Feb 13 13:16:27 2001 +0100
@@ -168,23 +168,6 @@
 
 (*** The Key K uniquely identifies the Server's  message. **)
 
-Goal "evs : yahalom ==>                                     \
-\   EX A' B' na' nb' X'. ALL A B na nb X.                   \
-\       Says Server A                                       \
-\        {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}   \
-\       : 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 (ALLGOALS Clarify_tac);
-by (ex_strip_tac 2);
-by (Blast_tac 2);
-(*Remaining case: YM3*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs
-                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
-val lemma = result();
 
 Goal "[| Says Server A                                                 \
 \         {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
@@ -192,7 +175,14 @@
 \         {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
 \       evs : yahalom |]                                    \
 \    ==> A=A' & B=B' & na=na' & nb=nb'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*YM4*)
+by (Blast_tac 2);
+(*YM3, by freshness*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
 qed "unique_session_keys";
 
 
@@ -411,26 +401,16 @@
 
 (*** The Nonce NB uniquely identifies B's message. ***)
 
-Goal "evs : yahalom ==>                                         \
-\EX NA' A' B'. ALL NA A B.                                      \
-\   Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(knows Spy evs) \
-\   --> B ~: bad --> NA = NA' & A = A' & B = B'";
-by (parts_induct_tac 1);
-(*Fake*)
-by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
-    THEN Fake_parts_insert_tac 1);
-by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
-(*YM2: creation of new Nonce.  Move assertion into global context*)
-by (expand_case_tac "nb = ?y" 1);
-by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-val lemma = result();
-
 Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (knows Spy evs);    \
 \        Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (knows Spy evs); \
 \       evs : yahalom;  B ~: bad;  B' ~: bad |]  \
 \     ==> NA' = NA & A' = A & B' = B";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
+(*YM2, by freshness*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
 qed "unique_NB";