src/HOL/Auth/Yahalom.ML
changeset 3961 6a8996fb7d99
parent 3919 c036caebfc75
child 4091 771b1f6422a8
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Oct 21 10:36:23 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Oct 21 10:39:27 1997 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4   "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     1.5  by (parts_induct_tac 1);
     1.6  by (Fake_parts_insert_tac 1);
     1.7 -by (Blast_tac 1);
     1.8 +by (ALLGOALS Blast_tac);
     1.9  qed "Spy_see_shrK";
    1.10  Addsimps [Spy_see_shrK];
    1.11  
    1.12 @@ -105,16 +105,14 @@
    1.13  goal thy "!!evs. evs : yahalom ==>          \
    1.14  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    1.15  by (parts_induct_tac 1);
    1.16 -(*YM4: Key K is not fresh!*)
    1.17 -by (blast_tac (!claset addSEs spies_partsEs) 3);
    1.18 -(*YM3*)
    1.19 -by (Blast_tac 2);
    1.20  (*Fake*)
    1.21  by (best_tac
    1.22 -      (!claset addIs [impOfSubs analz_subset_parts]
    1.23 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.24 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.25 -               addss (!simpset)) 1);
    1.26 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.27 +               addIs  [impOfSubs analz_subset_parts]
    1.28 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.29 +               addss  (!simpset)) 1);
    1.30 +(*YM2-4: Because Key K is not fresh, etc.*)
    1.31 +by (REPEAT (blast_tac (!claset addSEs spies_partsEs) 1));
    1.32  qed_spec_mp "new_keys_not_used";
    1.33  
    1.34  bind_thm ("new_keys_not_analzd",
    1.35 @@ -226,8 +224,8 @@
    1.36  by analz_spies_tac;
    1.37  by (ALLGOALS
    1.38      (asm_simp_tac 
    1.39 -     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    1.40 -               addsplits [expand_if])));
    1.41 +     (!simpset addsimps (expand_ifs@pushes)
    1.42 +	       addsimps [analz_insert_eq, analz_insert_freshK])));
    1.43  (*Oops*)
    1.44  by (blast_tac (!claset addDs [unique_session_keys]) 3);
    1.45  (*YM3*)
    1.46 @@ -365,7 +363,7 @@
    1.47   "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
    1.48  \        P --> (X : analz (G Un H)) = (X : analz H)";
    1.49  by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
    1.50 -val lemma = result();
    1.51 +val Nonce_secrecy_lemma = result();
    1.52  
    1.53  goal thy 
    1.54   "!!evs. evs : yahalom ==>                                         \
    1.55 @@ -376,17 +374,18 @@
    1.56  by (etac yahalom.induct 1);
    1.57  by analz_spies_tac;
    1.58  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
    1.59 -by (REPEAT_FIRST (rtac lemma));
    1.60 +by (REPEAT_FIRST (rtac Nonce_secrecy_lemma));
    1.61  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
    1.62    we get (~ KeyWithNonce K NB evsa); then simplification can apply the
    1.63    induction hypothesis with KK = {K}.*)
    1.64 -by (ALLGOALS  (*17 seconds*)
    1.65 +by (ALLGOALS  (*12 seconds*)
    1.66      (asm_simp_tac 
    1.67 -     (analz_image_freshK_ss addsimps
    1.68 -        [all_conj_distrib, analz_image_freshK,
    1.69 -	 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    1.70 -	 imp_disj_not1,			      (*Moves NBa~=NB to the front*)
    1.71 -	 Says_Server_KeyWithNonce])));
    1.72 +     (analz_image_freshK_ss 
    1.73 +       addsimps expand_ifs
    1.74 +       addsimps [all_conj_distrib, analz_image_freshK,
    1.75 +		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    1.76 +		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
    1.77 +		 Says_Server_KeyWithNonce])));
    1.78  (*Base*)
    1.79  by (Blast_tac 1);
    1.80  (*Fake*) 
    1.81 @@ -498,8 +497,8 @@
    1.82  by analz_spies_tac;
    1.83  by (ALLGOALS
    1.84      (asm_simp_tac 
    1.85 -     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    1.86 -               addsplits [expand_if])));
    1.87 +     (!simpset addsimps (expand_ifs@pushes)
    1.88 +	       addsimps [analz_insert_eq, analz_insert_freshK])));
    1.89  (*Prove YM3 by showing that no NB can also be an NA*)
    1.90  by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
    1.91  	               addSEs [MPair_parts]