src/HOL/Auth/OtwayRees_Bad.ML

 
 
 (*** Future keys can't be seen or used! ***)
 
 (*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : otway ==>               \
-\                length evs <= length evs' --> \
-\                Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway ==>               \
+\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
 				    addDs [impOfSubs analz_subset_parts,
 					   impOfSubs parts_insert_subset_Un,
 					   Suc_leD]

 qed_spec_mp "new_keys_not_seen";
 Addsimps [new_keys_not_seen];
 
 (*Variant: old messages must contain old keys!*)
 goal thy 
- "!!evs. [| Says A B X : set_of_list evs;  \
-\           Key (newK evt) : parts {X};    \
-\           evs : otway                 \
-\        |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs;          \
+\           Key (newK i) : parts {X};    \
+\           evs : otway                            \
+\        |] ==> i < length evs";
 by (rtac ccontr 1);
 by (dtac leI 1);
 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
                       addIs  [impOfSubs parts_mono]) 1);
 qed "Says_imp_old_keys";
 
 
 (*** Future nonces can't be seen or used! ***)
 
-goal thy "!!evs. evs : otway ==> \
-\                length evs <= length evs' --> \
-\                Nonce (newN evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway ==>               \
+\              length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT_FIRST
     (fast_tac (!claset addSEs partsEs
 	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
 		       addEs [leD RS notE]

 qed_spec_mp "new_nonces_not_seen";
 Addsimps [new_nonces_not_seen];
 
 (*Variant: old messages must contain old nonces!*)
 goal thy 
- "!!evs. [| Says A B X : set_of_list evs;    \
-\           Nonce (newN evt) : parts {X};    \
-\           evs : otway                 \
-\        |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs;            \
+\           Nonce (newN i) : parts {X};    \
+\           evs : otway                              \
+\        |] ==> i < length evs";
 by (rtac ccontr 1);
 by (dtac leI 1);
 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
                       addIs  [impOfSubs parts_mono]) 1);
 qed "Says_imp_old_nonces";
 
 
 (*Nobody can have USED keys that will be generated in the future.
   ...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway ==> \
-\                length evs <= length evs' --> \
-\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : otway ==>               \
+\           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
 by (parts_induct_tac 1);
 (*OR1 and OR3*)
 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
 (*Fake, OR2, OR4: these messages send unknown (X) components*)
 by (REPEAT

 (*Describes the form of K and NA when the Server sends this message.  Also
   for Oops case.*)
 goal thy 
  "!!evs. [| Says Server B \
 \            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
-\           evs : otway |]                                   \
-\        ==> (EX evt: otway. K = Key(newK evt)) &            \
+\           evs : otway |]                                           \
+\        ==> (EX n. K = Key(newK n)) &                               \
 \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
 qed "Says_Server_message_form";

 val analz_Fake_tac = 
     dtac OR2_analz_sees_Spy 4 THEN 
     dtac OR4_analz_sees_Spy 6 THEN
     forward_tac [Says_Server_message_form] 7 THEN
     assume_tac 7 THEN Full_simp_tac 7 THEN
-    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
+    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
 
 
 (****
  The following is to prove theorems of the form
 
-          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
-          Key K : analz (sees lost Spy evs)
+  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+  Key K : analz (sees lost Spy evs)
 
  A more general formula must be proved inductively.
 
 ****)
 

 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
 by analz_Fake_tac;
 by (REPEAT_FIRST (ares_tac [allI, lemma]));
-by (ALLGOALS
+by (ALLGOALS (*Takes 18 secs*)
     (asm_simp_tac 
-     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
-                         @ pushes)
+     (!simpset addsimps [Un_assoc RS sym, 
+			 insert_Key_singleton, insert_Key_image, pushKey_newK]
                setloop split_tac [expand_if])));
-(** LEVEL 7 **)
 (*OR4, OR2, Fake*) 
 by (EVERY (map spy_analz_tac [5,3,2]));
 (*Oops, OR3, Base*)
 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
 qed_spec_mp "analz_image_newK";
 
 
 goal thy
  "!!evs. evs : otway ==>                               \
-\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\        (K = newK evt | Key K : analz (sees lost Spy evs))";
+\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\        (K = newK i | Key K : analz (sees lost Spy evs))";
 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
                                    insert_Key_singleton]) 1);
 by (Fast_tac 1);
 qed "analz_insert_Key_newK";
 
 
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway ==>                                                 \
+ "!!evs. evs : otway ==>                                                      \
 \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
 \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));

 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
 by analz_Fake_tac;
 by (ALLGOALS
-    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
-				       analz_insert_Key_newK] @ pushes)
+    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
+				      analz_insert_Key_newK]
 		            setloop split_tac [expand_if])));
 (*OR3*)
 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
                       addss (!simpset addsimps [parts_insert2])) 3);
 (*OR4, OR2, Fake*)