src/HOL/Auth/OtwayRees.ML
changeset 2451 ce85a2aafc7a
parent 2417 95f275c8476e
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Dec 19 11:54:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Dec 19 11:58:39 1996 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 -Pretty.setdepth 15;
     1.8  
     1.9  
    1.10  (*A "possibility property": there are traces that reach the end*)
    1.11 @@ -132,9 +131,8 @@
    1.12  (*** Future keys can't be seen or used! ***)
    1.13  
    1.14  (*Nobody can have SEEN keys that will be generated in the future. *)
    1.15 -goal thy "!!evs. evs : otway lost ==> \
    1.16 -\                length evs <= length evs' --> \
    1.17 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
    1.18 +goal thy "!!i. evs : otway lost ==>          \
    1.19 +\              length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
    1.20  by (parts_induct_tac 1);
    1.21  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    1.22                                      addDs [impOfSubs analz_subset_parts,
    1.23 @@ -146,10 +144,10 @@
    1.24  
    1.25  (*Variant: old messages must contain old keys!*)
    1.26  goal thy 
    1.27 - "!!evs. [| Says A B X : set_of_list evs;  \
    1.28 -\           Key (newK evt) : parts {X};    \
    1.29 -\           evs : otway lost                 \
    1.30 -\        |] ==> length evt < length evs";
    1.31 + "!!evs. [| Says A B X : set_of_list evs;          \
    1.32 +\           Key (newK i) : parts {X};    \
    1.33 +\           evs : otway lost                       \
    1.34 +\        |] ==> i < length evs";
    1.35  by (rtac ccontr 1);
    1.36  by (dtac leI 1);
    1.37  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    1.38 @@ -159,9 +157,9 @@
    1.39  
    1.40  (*** Future nonces can't be seen or used! ***)
    1.41  
    1.42 -goal thy "!!evs. evs : otway lost ==> \
    1.43 -\                length evs <= length evt --> \
    1.44 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    1.45 +goal thy "!!evs. evs : otway lost ==>         \
    1.46 +\                length evs <= i --> \
    1.47 +\                Nonce (newN i) ~: parts (sees lost Spy evs)";
    1.48  by (parts_induct_tac 1);
    1.49  by (REPEAT_FIRST (fast_tac (!claset 
    1.50                                addSEs partsEs
    1.51 @@ -175,10 +173,10 @@
    1.52  Addsimps [new_nonces_not_seen];
    1.53  
    1.54  (*Variant: old messages must contain old nonces!*)
    1.55 -goal thy "!!evs. [| Says A B X : set_of_list evs;    \
    1.56 -\                   Nonce (newN evt) : parts {X};    \
    1.57 -\                   evs : otway lost                 \
    1.58 -\                |] ==> length evt < length evs";
    1.59 +goal thy "!!evs. [| Says A B X : set_of_list evs;            \
    1.60 +\                   Nonce (newN i) : parts {X};    \
    1.61 +\                   evs : otway lost                         \
    1.62 +\                |] ==> i < length evs";
    1.63  by (rtac ccontr 1);
    1.64  by (dtac leI 1);
    1.65  by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
    1.66 @@ -188,9 +186,8 @@
    1.67  
    1.68  (*Nobody can have USED keys that will be generated in the future.
    1.69    ...very like new_keys_not_seen*)
    1.70 -goal thy "!!evs. evs : otway lost ==>          \
    1.71 -\                length evs <= length evs' --> \
    1.72 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    1.73 +goal thy "!!i. evs : otway lost ==>          \
    1.74 +\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
    1.75  by (parts_induct_tac 1);
    1.76  (*OR1 and OR3*)
    1.77  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    1.78 @@ -218,9 +215,9 @@
    1.79    for Oops case.*)
    1.80  goal thy 
    1.81   "!!evs. [| Says Server B \
    1.82 -\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
    1.83 -\           evs : otway lost |]                                   \
    1.84 -\        ==> (EX evt: otway lost. K = Key(newK evt)) &            \
    1.85 +\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;       \
    1.86 +\           evs : otway lost |]                                           \
    1.87 +\        ==> (EX n. K = Key(newK n)) &                                    \
    1.88  \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.89  by (etac rev_mp 1);
    1.90  by (etac otway.induct 1);
    1.91 @@ -234,14 +231,14 @@
    1.92      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
    1.93      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    1.94      assume_tac 7 THEN Full_simp_tac 7 THEN
    1.95 -    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
    1.96 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    1.97  
    1.98  
    1.99  (****
   1.100   The following is to prove theorems of the form
   1.101  
   1.102 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   1.103 -          Key K : analz (sees lost Spy evs)
   1.104 +  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   1.105 +  Key K : analz (sees lost Spy evs)
   1.106  
   1.107   A more general formula must be proved inductively.
   1.108  ****)
   1.109 @@ -257,10 +254,10 @@
   1.110  by (etac otway.induct 1);
   1.111  by analz_Fake_tac;
   1.112  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.113 -by (ALLGOALS (*Takes 12 secs*)
   1.114 +by (ALLGOALS (*Takes 11 secs*)
   1.115      (asm_simp_tac 
   1.116 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.117 -                         @ pushes)
   1.118 +     (!simpset addsimps [Un_assoc RS sym, 
   1.119 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.120                 setloop split_tac [expand_if])));
   1.121  (*OR4, OR2, Fake*) 
   1.122  by (EVERY (map spy_analz_tac [5,3,2]));
   1.123 @@ -271,8 +268,8 @@
   1.124  
   1.125  goal thy
   1.126   "!!evs. evs : otway lost ==>                               \
   1.127 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   1.128 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   1.129 +\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   1.130 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
   1.131  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.132                                     insert_Key_singleton]) 1);
   1.133  by (Fast_tac 1);
   1.134 @@ -442,8 +439,8 @@
   1.135  by (etac otway.induct 1);
   1.136  by analz_Fake_tac;
   1.137  by (ALLGOALS
   1.138 -    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
   1.139 -				       analz_insert_Key_newK] @ pushes)
   1.140 +    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
   1.141 +				      analz_insert_Key_newK] 
   1.142  		            setloop split_tac [expand_if])));
   1.143  (*OR3*)
   1.144  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]