src/HOL/Auth/Yahalom.ML
changeset 2160 ad4382e546fc
parent 2156 9c361df93bd5
child 2170 c5e460f1ebb4
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Nov 04 17:23:37 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Nov 05 11:20:52 1996 +0100
     1.3 @@ -118,30 +118,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 : yahalom 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 : yahalom 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 @@ -168,31 +157,25 @@
    1.39    ...very like new_keys_not_seen*)
    1.40  goal thy "!!evs. evs : yahalom lost ==> \
    1.41  \                length evs <= length evs' --> \
    1.42 -\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    1.43 +\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    1.44  by (parts_induct_tac 1);
    1.45 -by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
    1.46  (*YM1, YM2 and YM3*)
    1.47  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    1.48 -(*Fake and YM4: these messages send unknown (X) components*)
    1.49 -by (stac insert_commute 2);
    1.50 -by (Simp_tac 2);
    1.51 -(*YM4: the only way K could have been used is if it had been seen,
    1.52 -  contradicting new_keys_not_seen*)
    1.53 -by (REPEAT
    1.54 -     (best_tac
    1.55 -      (!claset addDs [impOfSubs analz_subset_parts,
    1.56 -                      impOfSubs (analz_subset_parts RS keysFor_mono),
    1.57 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.58 -                      Suc_leD]
    1.59 +(*Fake and Oops: these messages send unknown (X) components*)
    1.60 +by (EVERY
    1.61 +    (map (fast_tac
    1.62 +	  (!claset addDs [impOfSubs analz_subset_parts,
    1.63 +			  impOfSubs (analz_subset_parts RS keysFor_mono),
    1.64 +			  impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.65 +			  Suc_leD]
    1.66 +                   addss (!simpset))) [3,1]));
    1.67 +(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
    1.68 +by (fast_tac
    1.69 +      (!claset addSEs partsEs
    1.70 +               addSDs [Says_imp_sees_Spy RS parts.Inj]
    1.71                 addEs [new_keys_not_seen RSN(2,rev_notE)]
    1.72 -               addss (!simpset)) 1));
    1.73 -val lemma = result();
    1.74 -
    1.75 -goal thy 
    1.76 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
    1.77 -\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
    1.78 -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    1.79 -qed "new_keys_not_used";
    1.80 +               addDs [Suc_leD]) 1);
    1.81 +qed_spec_mp "new_keys_not_used";
    1.82  
    1.83  bind_thm ("new_keys_not_analzd",
    1.84            [analz_subset_parts RS keysFor_mono,
    1.85 @@ -413,31 +396,22 @@
    1.86  
    1.87  goal thy "!!evs. evs : yahalom lost ==> \
    1.88  \                length evs <= length evt --> \
    1.89 -\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    1.90 -by (etac yahalom.induct 1);
    1.91 -(*auto_tac does not work here, as it performs safe_tac first*)
    1.92 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    1.93 -                                     addcongs [disj_cong])));
    1.94 -by (REPEAT_FIRST
    1.95 -    (fast_tac (!claset addSEs partsEs
    1.96 -	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.97 -		       addDs  [impOfSubs analz_subset_parts,
    1.98 -			       impOfSubs parts_insert_subset_Un, Suc_leD]
    1.99 -		       addss (!simpset))));
   1.100 -val lemma = result();
   1.101 -
   1.102 -(*Variant needed for the main theorem below*)
   1.103 -goal thy 
   1.104 - "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   1.105 -\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
   1.106 -by (fast_tac (!claset addDs [lemma]) 1);
   1.107 -qed "new_nonces_not_seen";
   1.108 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   1.109 +by (parts_induct_tac 1);
   1.110 +by (REPEAT_FIRST (fast_tac (!claset 
   1.111 +                              addSEs partsEs
   1.112 +                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   1.113 +                              addDs  [impOfSubs analz_subset_parts,
   1.114 +                                      impOfSubs parts_insert_subset_Un,
   1.115 +                                      Suc_leD]
   1.116 +                              addss (!simpset))));
   1.117 +qed_spec_mp "new_nonces_not_seen";
   1.118  Addsimps [new_nonces_not_seen];
   1.119  
   1.120 -(*Another variant: old messages must contain old nonces!*)
   1.121 +(*Variant: old messages must contain old nonces!*)
   1.122  goal thy 
   1.123 - "!!evs. [| Says A B X : set_of_list evs;  \
   1.124 -\           Nonce (newN evt) : parts {X};    \
   1.125 + "!!evs. [| Says A B X : set_of_list evs;      \
   1.126 +\           Nonce (newN evt) : parts {X};      \
   1.127  \           evs : yahalom lost                 \
   1.128  \        |] ==> length evt < length evs";
   1.129  by (rtac ccontr 1);