src/HOL/Auth/OtwayRees.ML
changeset 2160 ad4382e546fc
parent 2135 80477862ab33
child 2166 d276a806cc10
--- a/src/HOL/Auth/OtwayRees.ML	Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Nov 05 11:20:52 1996 +0100
@@ -131,30 +131,19 @@
 
 (*** Future keys can't be seen or used! ***)
 
-(*Nobody can have SEEN keys that will be generated in the future.
-  This has to be proved anew for each protocol description,
-  but should go by similar reasoning every time.  Hardest case is the
-  standard Fake rule.  
-      The Union over C is essential for the induction! *)
+(*Nobody can have SEEN keys that will be generated in the future. *)
 goal thy "!!evs. evs : otway lost ==> \
 \                length evs <= length evs' --> \
-\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+\                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy 
- "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
-\        ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
 Addsimps [new_keys_not_seen];
 
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
 goal thy 
  "!!evs. [| Says A B X : set_of_list evs;  \
 \           Key (newK evt) : parts {X};    \
@@ -167,15 +156,12 @@
 qed "Says_imp_old_keys";
 
 
-(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
+(*** Future nonces can't be seen or used! ***)
 
 goal thy "!!evs. evs : otway lost ==> \
 \                length evs <= length evt --> \
-\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
-                                     addcongs [disj_cong])));
+\                Nonce (newN evt) ~: 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]
@@ -183,22 +169,14 @@
                                       impOfSubs parts_insert_subset_Un,
                                       Suc_leD]
                               addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy 
- "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
-\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+qed_spec_mp "new_nonces_not_seen";
 Addsimps [new_nonces_not_seen];
 
-(*Another 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 lost                 \
-\        |] ==> length evt < length evs";
+(*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 lost                 \
+\                |] ==> length evt < length evs";
 by (rtac ccontr 1);
 by (dtac leI 1);
 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
@@ -208,9 +186,9 @@
 
 (*Nobody can have USED keys that will be generated in the future.
   ...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway lost ==> \
+goal thy "!!evs. evs : otway lost ==>          \
 \                length evs <= length evs' --> \
-\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\                newK evs' ~: 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]));
@@ -222,13 +200,7 @@
                       Suc_leD]
                addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
                addss (!simpset)) 1));
-val lemma = result();
-
-goal thy 
- "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
-\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+qed_spec_mp "new_keys_not_used";
 
 bind_thm ("new_keys_not_analzd",
           [analz_subset_parts RS keysFor_mono,
@@ -283,12 +255,11 @@
 by (etac otway.induct 1);
 by analz_Fake_tac;
 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 22 secs*)
+by (ALLGOALS (*Takes 14 secs*)
     (asm_simp_tac 
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
                          @ pushes)
                setloop split_tac [expand_if])));
-(** LEVEL 5 **)
 (*OR4, OR2, Fake*) 
 by (EVERY (map spy_analz_tac [5,3,2]));
 (*Oops, OR3, Base*)