# HG changeset patch
# User paulson
# Date 898676986 -7200
# Node ID 61e4403023a2bb0f2b99e6060ff5ed84e355fdfd
# Parent  255324b49a1cdcf3cddc941d906d9313c9e2e214
Tidying; renaming of Says_Server_message_form to
Says_Server_not_range;  removal of junk from analz_spies_tac;
removal of  B~:bad  premise from no_nonce_YM1_YM2

diff -r 255324b49a1c -r 61e4403023a2 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Jun 23 18:09:16 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Wed Jun 24 10:29:46 1998 +0200
@@ -20,7 +20,7 @@
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
-\        ==> EX X NB K. EX evs: yahalom.     \
+\        ==> EX X NB K. EX evs: yahalom.          \
 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
@@ -124,15 +124,13 @@
 by (etac yahalom.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
-qed "Says_Server_message_form";
+qed "Says_Server_not_range";
+
+Addsimps [Says_Server_not_range];
 
 
 (*For proofs involving analz.*)
-val analz_spies_tac = 
-    forward_tac [YM4_analz_spies] 6 THEN
-    forward_tac [Says_Server_message_form] 7 THEN
-    assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
-
+val analz_spies_tac = forward_tac [YM4_analz_spies] 6;
 
 (****
  The following is to prove theorems of the form
@@ -146,23 +144,24 @@
 (** Session keys are not used to encrypt other session keys **)
 
 goal thy  
- "!!evs. evs : yahalom ==>                                 \
-\  ALL K KK. KK <= Compl (range shrK) -->                       \
+ "!!evs. evs : yahalom ==>                              \
+\  ALL K KK. KK <= Compl (range shrK) -->               \
 \            (Key K : analz (Key``KK Un (spies evs))) = \
 \            (K : KK | Key K : analz (spies evs))";
 by (etac yahalom.induct 1);
 by analz_spies_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
-by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+by (ALLGOALS (asm_simp_tac
+	      (analz_image_freshK_ss addsimps [Says_Server_not_range])));
 (*Fake*) 
 by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 goal thy
- "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (spies evs)) =       \
-\        (K = KAB | Key K : analz (spies evs))";
+ "!!evs. [| evs : yahalom;  KAB ~: range shrK |]              \
+\         ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
+\             (K = KAB | Key K : analz (spies evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -171,9 +170,9 @@
 
 goal thy 
  "!!evs. 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|}        \
+\      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])));
@@ -235,7 +234,6 @@
 \           Notes Spy {|na, nb, Key K|} ~: set evs;               \
 \           A ~: bad;  B ~: bad;  evs : yahalom |]                \
 \        ==> Key K ~: analz (spies evs)";
-by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (claset() addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
 
@@ -382,13 +380,13 @@
 (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   we get (~ KeyWithNonce K NB evsa); then simplification can apply the
   induction hypothesis with KK = {K}.*)
-by (ALLGOALS  (*12 seconds*)
+by (ALLGOALS  (*4 seconds*)
     (asm_simp_tac 
      (analz_image_freshK_ss 
        addsimps split_ifs
        addsimps [all_conj_distrib, analz_image_freshK,
 		 KeyWithNonce_Says, KeyWithNonce_Notes,
-		 fresh_not_KeyWithNonce, 
+		 fresh_not_KeyWithNonce, Says_Server_not_range,
 		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
 		 Says_Server_KeyWithNonce])));
 (*Fake*) 
@@ -462,8 +460,8 @@
 (** A nonce value is never used both as NA and as NB **)
 
 goal thy 
- "!!evs. [| B ~: bad;  evs : yahalom  |]          \
-\ ==> Nonce NB ~: analz (spies evs) -->           \
+ "!!evs. evs : yahalom                     \
+\ ==> Nonce NB ~: analz (spies evs) -->    \
 \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
 \     Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(spies evs)";
 by (parts_induct_tac 1);
@@ -524,13 +522,12 @@
 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
 by (not_bad_tac "Aa" 1);
 by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
-by (forward_tac [Says_Server_message_form] 3);
-by (forward_tac [Says_Server_imp_YM2] 4);
+by (forward_tac [Says_Server_imp_YM2] 3);
 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
 (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
 by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
 			       impOfSubs Fake_analz_insert]) 1);
-(** LEVEL 14 **)
+(** LEVEL 13 **)
 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   covered by the quantified Oops assumption.*)
 by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1);