src/HOL/Auth/OtwayRees.ML
changeset 2160 ad4382e546fc
parent 2135 80477862ab33
child 2166 d276a806cc10
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Nov 04 17:23:37 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Nov 05 11:20:52 1996 +0100
     1.3 @@ -131,30 +131,19 @@
     1.4  
     1.5  (*** Future keys can't be seen or used! ***)
     1.6  
     1.7 -(*Nobody can have SEEN keys that will be generated in the future.
     1.8 -  This has to be proved anew for each protocol description,
     1.9 -  but should go by similar reasoning every time.  Hardest case is the
    1.10 -  standard Fake rule.  
    1.11 -      The Union over C is essential for the induction! *)
    1.12 +(*Nobody can have SEEN keys that will be generated in the future. *)
    1.13  goal thy "!!evs. evs : otway lost ==> \
    1.14  \                length evs <= length evs' --> \
    1.15 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    1.16 +\                Key (newK evs') ~: parts (sees lost Spy evs)";
    1.17  by (parts_induct_tac 1);
    1.18  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.19                                             impOfSubs parts_insert_subset_Un,
    1.20                                             Suc_leD]
    1.21                                      addss (!simpset))));
    1.22 -val lemma = result();
    1.23 -
    1.24 -(*Variant needed for the main theorem below*)
    1.25 -goal thy 
    1.26 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    1.27 -\        ==> Key (newK evs') ~: parts (sees lost C evs)";
    1.28 -by (fast_tac (!claset addDs [lemma]) 1);
    1.29 -qed "new_keys_not_seen";
    1.30 +qed_spec_mp "new_keys_not_seen";
    1.31  Addsimps [new_keys_not_seen];
    1.32  
    1.33 -(*Another variant: old messages must contain old keys!*)
    1.34 +(*Variant: old messages must contain old keys!*)
    1.35  goal thy 
    1.36   "!!evs. [| Says A B X : set_of_list evs;  \
    1.37  \           Key (newK evt) : parts {X};    \
    1.38 @@ -167,15 +156,12 @@
    1.39  qed "Says_imp_old_keys";
    1.40  
    1.41  
    1.42 -(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
    1.43 +(*** Future nonces can't be seen or used! ***)
    1.44  
    1.45  goal thy "!!evs. evs : otway lost ==> \
    1.46  \                length evs <= length evt --> \
    1.47 -\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    1.48 -by (etac otway.induct 1);
    1.49 -(*auto_tac does not work here, as it performs safe_tac first*)
    1.50 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    1.51 -                                     addcongs [disj_cong])));
    1.52 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    1.53 +by (parts_induct_tac 1);
    1.54  by (REPEAT_FIRST (fast_tac (!claset 
    1.55                                addSEs partsEs
    1.56                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.57 @@ -183,22 +169,14 @@
    1.58                                        impOfSubs parts_insert_subset_Un,
    1.59                                        Suc_leD]
    1.60                                addss (!simpset))));
    1.61 -val lemma = result();
    1.62 -
    1.63 -(*Variant needed for the main theorem below*)
    1.64 -goal thy 
    1.65 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
    1.66 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
    1.67 -by (fast_tac (!claset addDs [lemma]) 1);
    1.68 -qed "new_nonces_not_seen";
    1.69 +qed_spec_mp "new_nonces_not_seen";
    1.70  Addsimps [new_nonces_not_seen];
    1.71  
    1.72 -(*Another variant: old messages must contain old nonces!*)
    1.73 -goal thy 
    1.74 - "!!evs. [| Says A B X : set_of_list evs;  \
    1.75 -\           Nonce (newN evt) : parts {X};    \
    1.76 -\           evs : otway lost                 \
    1.77 -\        |] ==> length evt < length evs";
    1.78 +(*Variant: old messages must contain old nonces!*)
    1.79 +goal thy "!!evs. [| Says A B X : set_of_list evs;    \
    1.80 +\                   Nonce (newN evt) : parts {X};    \
    1.81 +\                   evs : otway lost                 \
    1.82 +\                |] ==> length evt < length evs";
    1.83  by (rtac ccontr 1);
    1.84  by (dtac leI 1);
    1.85  by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
    1.86 @@ -208,9 +186,9 @@
    1.87  
    1.88  (*Nobody can have USED keys that will be generated in the future.
    1.89    ...very like new_keys_not_seen*)
    1.90 -goal thy "!!evs. evs : otway lost ==> \
    1.91 +goal thy "!!evs. evs : otway lost ==>          \
    1.92  \                length evs <= length evs' --> \
    1.93 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    1.94 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    1.95  by (parts_induct_tac 1);
    1.96  (*OR1 and OR3*)
    1.97  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    1.98 @@ -222,13 +200,7 @@
    1.99                        Suc_leD]
   1.100                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.101                 addss (!simpset)) 1));
   1.102 -val lemma = result();
   1.103 -
   1.104 -goal thy 
   1.105 - "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   1.106 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   1.107 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.108 -qed "new_keys_not_used";
   1.109 +qed_spec_mp "new_keys_not_used";
   1.110  
   1.111  bind_thm ("new_keys_not_analzd",
   1.112            [analz_subset_parts RS keysFor_mono,
   1.113 @@ -283,12 +255,11 @@
   1.114  by (etac otway.induct 1);
   1.115  by analz_Fake_tac;
   1.116  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.117 -by (ALLGOALS (*Takes 22 secs*)
   1.118 +by (ALLGOALS (*Takes 14 secs*)
   1.119      (asm_simp_tac 
   1.120       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.121                           @ pushes)
   1.122                 setloop split_tac [expand_if])));
   1.123 -(** LEVEL 5 **)
   1.124  (*OR4, OR2, Fake*) 
   1.125  by (EVERY (map spy_analz_tac [5,3,2]));
   1.126  (*Oops, OR3, Base*)