src/HOL/Auth/Yahalom2.ML
changeset 2451 ce85a2aafc7a
parent 2377 ad9d2dedaeaa
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Dec 19 11:54:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Dec 19 11:58:39 1996 +0100
     1.3 @@ -126,9 +126,8 @@
     1.4  (*** Future keys can't be seen or used! ***)
     1.5  
     1.6  (*Nobody can have SEEN keys that will be generated in the future. *)
     1.7 -goal thy "!!evs. evs : yahalom lost ==> \
     1.8 -\                length evs <= length evs' --> \
     1.9 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
    1.10 +goal thy "!!i. evs : yahalom lost ==> \
    1.11 +\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
    1.12  by (parts_induct_tac 1);
    1.13  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    1.14  				    addDs [impOfSubs analz_subset_parts,
    1.15 @@ -141,9 +140,9 @@
    1.16  (*Variant: old messages must contain old keys!*)
    1.17  goal thy 
    1.18   "!!evs. [| Says A B X : set_of_list evs;  \
    1.19 -\           Key (newK evt) : parts {X};    \
    1.20 +\           Key (newK i) : parts {X};    \
    1.21  \           evs : yahalom lost                 \
    1.22 -\        |] ==> length evt < length evs";
    1.23 +\        |] ==> i < length evs";
    1.24  by (rtac ccontr 1);
    1.25  by (dtac leI 1);
    1.26  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    1.27 @@ -153,9 +152,8 @@
    1.28  
    1.29  (*Nobody can have USED keys that will be generated in the future.
    1.30    ...very like new_keys_not_seen*)
    1.31 -goal thy "!!evs. evs : yahalom lost ==> \
    1.32 -\                length evs <= length evs' --> \
    1.33 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    1.34 +goal thy "!!i. evs : yahalom lost ==> \
    1.35 +\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
    1.36  by (parts_induct_tac 1);
    1.37  by (dtac YM4_Key_parts_sees_Spy 5);
    1.38  (*YM1, YM2 and YM3*)
    1.39 @@ -189,7 +187,7 @@
    1.40   "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
    1.41  \            : set_of_list evs;                                         \
    1.42  \           evs : yahalom lost |]                                       \
    1.43 -\        ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
    1.44 +\        ==> (EX i. K = Key(newK i)) & A ~= B";
    1.45  by (etac rev_mp 1);
    1.46  by (etac yahalom.induct 1);
    1.47  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.48 @@ -201,13 +199,13 @@
    1.49      dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
    1.50      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    1.51      assume_tac 7 THEN Full_simp_tac 7 THEN
    1.52 -    REPEAT ((eresolve_tac [bexE,conjE] ORELSE' hyp_subst_tac) 7);
    1.53 +    REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7);
    1.54  
    1.55  
    1.56  (****
    1.57   The following is to prove theorems of the form
    1.58  
    1.59 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
    1.60 +          Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
    1.61            Key K : analz (sees lost Spy evs)
    1.62  
    1.63   A more general formula must be proved inductively.
    1.64 @@ -223,10 +221,10 @@
    1.65  by (etac yahalom.induct 1);
    1.66  by analz_Fake_tac;
    1.67  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
    1.68 -by (ALLGOALS  (*Takes 26 secs*)
    1.69 +by (ALLGOALS (*Takes 11 secs*)
    1.70      (asm_simp_tac 
    1.71 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.72 -                         @ pushes)
    1.73 +     (!simpset addsimps [Un_assoc RS sym, 
    1.74 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.75                 setloop split_tac [expand_if])));
    1.76  (*YM4, Fake*) 
    1.77  by (EVERY (map spy_analz_tac [4, 2]));
    1.78 @@ -236,8 +234,8 @@
    1.79  
    1.80  goal thy
    1.81   "!!evs. evs : yahalom lost ==>                               \
    1.82 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
    1.83 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
    1.84 +\        Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \
    1.85 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
    1.86  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
    1.87                                     insert_Key_singleton]) 1);
    1.88  by (Fast_tac 1);
    1.89 @@ -273,11 +271,7 @@
    1.90  \           : set_of_list evs;                                      \
    1.91  \          evs : yahalom lost |]                                    \
    1.92  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    1.93 -by (dtac lemma 1);
    1.94 -by (REPEAT (etac exE 1));
    1.95 -(*Duplicate the assumption*)
    1.96 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.97 -by (fast_tac (!claset addSDs [spec]) 1);
    1.98 +by (prove_unique_tac lemma 1);
    1.99  qed "unique_session_keys";
   1.100  
   1.101  
   1.102 @@ -296,8 +290,7 @@
   1.103  by analz_Fake_tac;
   1.104  by (ALLGOALS
   1.105      (asm_simp_tac 
   1.106 -     (!simpset addsimps ([not_parts_not_analz,
   1.107 -                          analz_insert_Key_newK] @ pushes)
   1.108 +     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
   1.109                 setloop split_tac [expand_if])));
   1.110  (*YM3*)
   1.111  by (fast_tac (!claset addIs [parts_insertI]