Extensive tidying and simplification, largely stemming from
authorpaulson
Thu Dec 19 11:58:39 1996 +0100 (1996-12-19)
changeset 2451ce85a2aafc7a
parent 2450 3ad2493fa0e0
child 2452 045d00d777fb
Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Public.ML
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Thu Dec 19 11:54:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Thu Dec 19 11:58:39 1996 +0100
     1.3 @@ -84,9 +84,9 @@
     1.4  
     1.5  (*** Future nonces can't be seen or used! ***)
     1.6  
     1.7 -goal thy "!!evs. evs : ns_public ==> \
     1.8 -\                length evs <= length evt --> \
     1.9 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    1.10 +goal thy "!!evs. evs : ns_public ==>          \
    1.11 +\                length evs <= i --> \
    1.12 +\                Nonce (newN i) ~: parts (sees lost Spy evs)";
    1.13  by (parts_induct_tac 1);
    1.14  by (REPEAT_FIRST (fast_tac (!claset 
    1.15                                addSEs partsEs
    1.16 @@ -104,8 +104,8 @@
    1.17  fun analz_induct_tac i = 
    1.18      etac ns_public.induct i	THEN
    1.19      ALLGOALS (asm_simp_tac 
    1.20 -	      (!simpset addsimps ([not_parts_not_analz] @ pushes)
    1.21 -               setloop split_tac [expand_if]));
    1.22 +	      (!simpset addsimps [not_parts_not_analz]
    1.23 +                        setloop split_tac [expand_if]));
    1.24  
    1.25  (**** Authenticity properties obtained from NS2 ****)
    1.26  
     2.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Dec 19 11:54:19 1996 +0100
     2.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Dec 19 11:58:39 1996 +0100
     2.3 @@ -25,15 +25,16 @@
     2.4  
     2.5           (*Alice initiates a protocol run, sending a nonce to Bob*)
     2.6      NS1  "[| evs: ns_public;  A ~= B |]
     2.7 -          ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
     2.8 -                : ns_public"
     2.9 +          ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
    2.10 +                 # evs  :  ns_public"
    2.11  
    2.12           (*Bob responds to Alice's message with a further nonce*)
    2.13      NS2  "[| evs: ns_public;  A ~= B;
    2.14               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.15                 : set_of_list evs |]
    2.16 -          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs), Agent B|})
    2.17 -                # evs  : ns_public"
    2.18 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)), 
    2.19 +                                         Agent B|})
    2.20 +                # evs  :  ns_public"
    2.21  
    2.22           (*Alice proves her existence by sending NB back to Bob.*)
    2.23      NS3  "[| evs: ns_public;  A ~= B;
     3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Dec 19 11:54:19 1996 +0100
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Dec 19 11:58:39 1996 +0100
     3.3 @@ -89,9 +89,8 @@
     3.4  
     3.5  (*** Future nonces can't be seen or used! ***)
     3.6  
     3.7 -goal thy "!!evs. evs : ns_public ==> \
     3.8 -\                length evs <= length evt --> \
     3.9 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    3.10 +goal thy "!!i. evs : ns_public ==>        \
    3.11 +\             length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
    3.12  by (parts_induct_tac 1);
    3.13  by (REPEAT_FIRST (fast_tac (!claset 
    3.14                                addSEs partsEs
    3.15 @@ -109,7 +108,7 @@
    3.16  fun analz_induct_tac i = 
    3.17      etac ns_public.induct i	THEN
    3.18      ALLGOALS (asm_simp_tac 
    3.19 -	      (!simpset addsimps ([not_parts_not_analz] @ pushes)
    3.20 +	      (!simpset addsimps [not_parts_not_analz]
    3.21                 setloop split_tac [expand_if]));
    3.22  
    3.23  
     4.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Dec 19 11:54:19 1996 +0100
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Dec 19 11:58:39 1996 +0100
     4.3 @@ -29,15 +29,15 @@
     4.4  
     4.5           (*Alice initiates a protocol run, sending a nonce to Bob*)
     4.6      NS1  "[| evs: ns_public;  A ~= B |]
     4.7 -          ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
     4.8 -                : ns_public"
     4.9 +          ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
    4.10 +                # evs  :  ns_public"
    4.11  
    4.12           (*Bob responds to Alice's message with a further nonce*)
    4.13      NS2  "[| evs: ns_public;  A ~= B;
    4.14               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.15                 : set_of_list evs |]
    4.16 -          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs
    4.17 -                : ns_public"
    4.18 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs))|})
    4.19 +                # evs  :  ns_public"
    4.20  
    4.21           (*Alice proves her existence by sending NB back to Bob.*)
    4.22      NS3  "[| evs: ns_public;  A ~= B;
     5.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Dec 19 11:54:19 1996 +0100
     5.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Dec 19 11:58:39 1996 +0100
     5.3 @@ -111,8 +111,7 @@
     5.4  
     5.5  (*Nobody can have SEEN keys that will be generated in the future. *)
     5.6  goal thy "!!evs. evs : ns_shared lost ==>      \
     5.7 -\                length evs <= length evs' --> \
     5.8 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
     5.9 +\               length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
    5.10  by (parts_induct_tac 1);
    5.11  by (ALLGOALS (fast_tac (!claset addEs [leD RS notE]
    5.12  				addDs [impOfSubs analz_subset_parts,
    5.13 @@ -124,10 +123,10 @@
    5.14  
    5.15  (*Variant: old messages must contain old keys!*)
    5.16  goal thy 
    5.17 - "!!evs. [| Says A B X : set_of_list evs;  \
    5.18 -\           Key (newK evt) : parts {X};    \
    5.19 -\           evs : ns_shared lost           \
    5.20 -\        |] ==> length evt < length evs";
    5.21 + "!!evs. [| Says A B X : set_of_list evs;          \
    5.22 +\           Key (newK i) : parts {X};              \
    5.23 +\           evs : ns_shared lost                   \
    5.24 +\        |] ==> i < length evs";
    5.25  by (rtac ccontr 1);
    5.26  by (dtac leI 1);
    5.27  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    5.28 @@ -139,8 +138,7 @@
    5.29  (*** Future nonces can't be seen or used! ***)
    5.30  
    5.31  goal thy "!!evs. evs : ns_shared lost ==>     \
    5.32 -\                length evs <= length evt --> \
    5.33 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    5.34 +\             length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
    5.35  by (parts_induct_tac 1);
    5.36  by (REPEAT_FIRST
    5.37      (fast_tac (!claset addSEs partsEs
    5.38 @@ -156,8 +154,8 @@
    5.39  (*Nobody can have USED keys that will be generated in the future.
    5.40    ...very like new_keys_not_seen*)
    5.41  goal thy "!!evs. evs : ns_shared lost ==>      \
    5.42 -\                length evs <= length evs' --> \
    5.43 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    5.44 +\                length evs <= i -->           \
    5.45 +\                newK i ~: keysFor (parts (sees lost Spy evs))";
    5.46  by (parts_induct_tac 1);
    5.47  (*NS1 and NS2*)
    5.48  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]));
    5.49 @@ -189,11 +187,10 @@
    5.50  (*Describes the form of K, X and K' when the Server sends this message.*)
    5.51  goal thy 
    5.52   "!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \
    5.53 -\           evs : ns_shared lost |]    \
    5.54 -\        ==> (EX evt: ns_shared lost. \
    5.55 -\                  K = Key(newK evt) & \
    5.56 -\                  X = (Crypt (shrK B) {|K, Agent A|}) & \
    5.57 -\                  K' = shrK A)";
    5.58 +\           evs : ns_shared lost |]                       \
    5.59 +\        ==> (EX i. K = Key(newK i) &                     \
    5.60 +\                   X = (Crypt (shrK B) {|K, Agent A|}) & \
    5.61 +\                   K' = shrK A)";
    5.62  by (etac rev_mp 1);
    5.63  by (etac ns_shared.induct 1);
    5.64  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    5.65 @@ -222,9 +219,8 @@
    5.66  goal thy 
    5.67   "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
    5.68  \            : set_of_list evs;  evs : ns_shared lost |]                   \
    5.69 -\        ==> (EX evt: ns_shared lost. K = newK evt &                       \
    5.70 -\                               length evt < length evs &                  \
    5.71 -\                               X = (Crypt (shrK B) {|Key K, Agent A|}))   \
    5.72 +\        ==> (EX i. K = newK i & i < length evs &                  \
    5.73 +\                   X = (Crypt (shrK B) {|Key K, Agent A|}))       \
    5.74  \          | X : analz (sees lost Spy evs)";
    5.75  by (case_tac "A : lost" 1);
    5.76  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    5.77 @@ -242,14 +238,14 @@
    5.78      forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
    5.79      forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
    5.80      Full_simp_tac 7 THEN
    5.81 -    REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac);
    5.82 +    REPEAT_FIRST (eresolve_tac [asm_rl, exE, disjE] ORELSE' hyp_subst_tac);
    5.83  
    5.84  
    5.85  (****
    5.86   The following is to prove theorems of the form
    5.87  
    5.88 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
    5.89 -          Key K : analz (sees lost Spy evs)
    5.90 +  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
    5.91 +  Key K : analz (sees lost Spy evs)
    5.92  
    5.93   A more general formula must be proved inductively.
    5.94  
    5.95 @@ -261,7 +257,7 @@
    5.96    We require that agents should behave like this subsequently also.*)
    5.97  goal thy 
    5.98   "!!evs. evs : ns_shared lost ==> \
    5.99 -\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
   5.100 +\        (Crypt (newK i) X) : parts (sees lost Spy evs) & \
   5.101  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   5.102  by (etac ns_shared.induct 1);
   5.103  by parts_Fake_tac;
   5.104 @@ -285,23 +281,22 @@
   5.105  by (etac ns_shared.induct 1);
   5.106  by analz_Fake_tac;
   5.107  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   5.108 -by (ALLGOALS 
   5.109 +by (ALLGOALS (*Takes 18 secs*)
   5.110      (asm_simp_tac 
   5.111 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   5.112 -                         @ pushes)
   5.113 +     (!simpset addsimps [Un_assoc RS sym, 
   5.114 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   5.115                 setloop split_tac [expand_if])));
   5.116 -(*NS3, Fake*) 
   5.117 +(*NS4, Fake*) 
   5.118  by (EVERY (map spy_analz_tac [5,2]));
   5.119 +(*NS3, NS2, Base*)
   5.120  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   5.121 -(*NS3, NS2, Base*)
   5.122 -by (REPEAT (Fast_tac 3));
   5.123  qed_spec_mp "analz_image_newK";
   5.124  
   5.125  
   5.126  goal thy
   5.127   "!!evs. evs : ns_shared lost ==>                               \
   5.128 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   5.129 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   5.130 +\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   5.131 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
   5.132  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   5.133                                     insert_Key_singleton]) 1);
   5.134  by (Fast_tac 1);
   5.135 @@ -312,8 +307,8 @@
   5.136      with a secure key **)
   5.137  
   5.138  goal thy 
   5.139 - "!!evs. evs : ns_shared lost ==>                                            \
   5.140 -\      EX A' NA' B' X'. ALL A NA B X.                                        \
   5.141 + "!!evs. evs : ns_shared lost ==>                                        \
   5.142 +\      EX A' NA' B' X'. ALL A NA B X.                                    \
   5.143  \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
   5.144  \       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
   5.145  by (etac ns_shared.induct 1);
   5.146 @@ -339,12 +334,7 @@
   5.147  \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
   5.148  \                  : set_of_list evs;                        \
   5.149  \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
   5.150 -by (dtac lemma 1);
   5.151 -by (REPEAT (etac exE 1));
   5.152 -(*Duplicate the assumption*)
   5.153 -by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1);
   5.154 -by (fast_tac (!claset addSDs [ spec] 
   5.155 -                      delrules [conjI] addss (!simpset)) 1);
   5.156 +by (prove_unique_tac lemma 1);
   5.157  qed "unique_session_keys";
   5.158  
   5.159  
   5.160 @@ -369,14 +359,14 @@
   5.161  by (fast_tac (!claset addIs [parts_insertI]
   5.162                        addEs [Says_imp_old_keys RS less_irrefl]
   5.163                        addss (!simpset)) 2);
   5.164 -(*OR4, OR2, Fake*) 
   5.165 -by (REPEAT_FIRST spy_analz_tac);
   5.166 -(*NS3 and Oops subcases*) (**LEVEL 7 **)
   5.167 +(*NS4, Fake*) 
   5.168 +by (EVERY (map spy_analz_tac [3,1]));
   5.169 +(*NS3 and Oops subcases*) (**LEVEL 5 **)
   5.170  by (step_tac (!claset delrules [impCE]) 1);
   5.171  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   5.172  by (etac conjE 2);
   5.173  by (mp_tac 2);
   5.174 -(**LEVEL 11 **)
   5.175 +(**LEVEL 9 **)
   5.176  by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 2);
   5.177  by (assume_tac 3);
   5.178  by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2);
   5.179 @@ -460,7 +450,7 @@
   5.180  by (Fast_tac 2);
   5.181  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   5.182  (*Contradiction from the assumption   
   5.183 -   Crypt (newK evsa) (Nonce NB) : parts (sees lost Spy evsa) *)
   5.184 +   Crypt (newK(length evsa)) (Nonce NB) : parts (sees lost Spy evsa) *)
   5.185  by (dtac Crypt_imp_invKey_keysFor 1);
   5.186  (**LEVEL 10**)
   5.187  by (Asm_full_simp_tac 1);
     6.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Dec 19 11:54:19 1996 +0100
     6.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Dec 19 11:58:39 1996 +0100
     6.3 @@ -27,8 +27,8 @@
     6.4  
     6.5           (*Alice initiates a protocol run, requesting to talk to any B*)
     6.6      NS1  "[| evs: ns_shared lost;  A ~= Server |]
     6.7 -          ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
     6.8 -                 : ns_shared lost"
     6.9 +          ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|}
    6.10 +                  # evs  :  ns_shared lost"
    6.11  
    6.12           (*Server's response to Alice's message.
    6.13             !! It may respond more than once to A's request !!
    6.14 @@ -36,9 +36,10 @@
    6.15                 the sender field.*)
    6.16      NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
    6.17               Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    6.18 -          ==> Says Server A (Crypt (shrK A)
    6.19 -                             {|Nonce NA, Agent B, Key (newK evs),   
    6.20 -                               (Crypt (shrK B) {|Key (newK evs), Agent A|})|}) 
    6.21 +          ==> Says Server A 
    6.22 +                (Crypt (shrK A)
    6.23 +                   {|Nonce NA, Agent B, Key (newK(length evs)),   
    6.24 +                    (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) 
    6.25                  # evs : ns_shared lost"
    6.26  
    6.27            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    6.28 @@ -53,7 +54,8 @@
    6.29             from, but responds to A because she is mentioned inside.*)
    6.30      NS4  "[| evs: ns_shared lost;  A ~= B;  
    6.31               Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
    6.32 -          ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost"
    6.33 +          ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs
    6.34 +                : ns_shared lost"
    6.35  
    6.36           (*Alice responds with Nonce NB if she has seen the key before.
    6.37             Maybe should somehow check Nonce NA again.
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Dec 19 11:54:19 1996 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Dec 19 11:58:39 1996 +0100
     7.3 @@ -16,7 +16,6 @@
     7.4  
     7.5  proof_timing:=true;
     7.6  HOL_quantifiers := false;
     7.7 -Pretty.setdepth 15;
     7.8  
     7.9  
    7.10  (*A "possibility property": there are traces that reach the end*)
    7.11 @@ -132,9 +131,8 @@
    7.12  (*** Future keys can't be seen or used! ***)
    7.13  
    7.14  (*Nobody can have SEEN keys that will be generated in the future. *)
    7.15 -goal thy "!!evs. evs : otway lost ==> \
    7.16 -\                length evs <= length evs' --> \
    7.17 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
    7.18 +goal thy "!!i. evs : otway lost ==>          \
    7.19 +\              length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
    7.20  by (parts_induct_tac 1);
    7.21  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    7.22                                      addDs [impOfSubs analz_subset_parts,
    7.23 @@ -146,10 +144,10 @@
    7.24  
    7.25  (*Variant: old messages must contain old keys!*)
    7.26  goal thy 
    7.27 - "!!evs. [| Says A B X : set_of_list evs;  \
    7.28 -\           Key (newK evt) : parts {X};    \
    7.29 -\           evs : otway lost                 \
    7.30 -\        |] ==> length evt < length evs";
    7.31 + "!!evs. [| Says A B X : set_of_list evs;          \
    7.32 +\           Key (newK i) : parts {X};    \
    7.33 +\           evs : otway lost                       \
    7.34 +\        |] ==> i < length evs";
    7.35  by (rtac ccontr 1);
    7.36  by (dtac leI 1);
    7.37  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    7.38 @@ -159,9 +157,9 @@
    7.39  
    7.40  (*** Future nonces can't be seen or used! ***)
    7.41  
    7.42 -goal thy "!!evs. evs : otway lost ==> \
    7.43 -\                length evs <= length evt --> \
    7.44 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    7.45 +goal thy "!!evs. evs : otway lost ==>         \
    7.46 +\                length evs <= i --> \
    7.47 +\                Nonce (newN i) ~: parts (sees lost Spy evs)";
    7.48  by (parts_induct_tac 1);
    7.49  by (REPEAT_FIRST (fast_tac (!claset 
    7.50                                addSEs partsEs
    7.51 @@ -175,10 +173,10 @@
    7.52  Addsimps [new_nonces_not_seen];
    7.53  
    7.54  (*Variant: old messages must contain old nonces!*)
    7.55 -goal thy "!!evs. [| Says A B X : set_of_list evs;    \
    7.56 -\                   Nonce (newN evt) : parts {X};    \
    7.57 -\                   evs : otway lost                 \
    7.58 -\                |] ==> length evt < length evs";
    7.59 +goal thy "!!evs. [| Says A B X : set_of_list evs;            \
    7.60 +\                   Nonce (newN i) : parts {X};    \
    7.61 +\                   evs : otway lost                         \
    7.62 +\                |] ==> i < length evs";
    7.63  by (rtac ccontr 1);
    7.64  by (dtac leI 1);
    7.65  by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
    7.66 @@ -188,9 +186,8 @@
    7.67  
    7.68  (*Nobody can have USED keys that will be generated in the future.
    7.69    ...very like new_keys_not_seen*)
    7.70 -goal thy "!!evs. evs : otway lost ==>          \
    7.71 -\                length evs <= length evs' --> \
    7.72 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    7.73 +goal thy "!!i. evs : otway lost ==>          \
    7.74 +\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
    7.75  by (parts_induct_tac 1);
    7.76  (*OR1 and OR3*)
    7.77  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    7.78 @@ -218,9 +215,9 @@
    7.79    for Oops case.*)
    7.80  goal thy 
    7.81   "!!evs. [| Says Server B \
    7.82 -\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
    7.83 -\           evs : otway lost |]                                   \
    7.84 -\        ==> (EX evt: otway lost. K = Key(newK evt)) &            \
    7.85 +\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;       \
    7.86 +\           evs : otway lost |]                                           \
    7.87 +\        ==> (EX n. K = Key(newK n)) &                                    \
    7.88  \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    7.89  by (etac rev_mp 1);
    7.90  by (etac otway.induct 1);
    7.91 @@ -234,14 +231,14 @@
    7.92      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
    7.93      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    7.94      assume_tac 7 THEN Full_simp_tac 7 THEN
    7.95 -    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
    7.96 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    7.97  
    7.98  
    7.99  (****
   7.100   The following is to prove theorems of the form
   7.101  
   7.102 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   7.103 -          Key K : analz (sees lost Spy evs)
   7.104 +  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   7.105 +  Key K : analz (sees lost Spy evs)
   7.106  
   7.107   A more general formula must be proved inductively.
   7.108  ****)
   7.109 @@ -257,10 +254,10 @@
   7.110  by (etac otway.induct 1);
   7.111  by analz_Fake_tac;
   7.112  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   7.113 -by (ALLGOALS (*Takes 12 secs*)
   7.114 +by (ALLGOALS (*Takes 11 secs*)
   7.115      (asm_simp_tac 
   7.116 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   7.117 -                         @ pushes)
   7.118 +     (!simpset addsimps [Un_assoc RS sym, 
   7.119 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   7.120                 setloop split_tac [expand_if])));
   7.121  (*OR4, OR2, Fake*) 
   7.122  by (EVERY (map spy_analz_tac [5,3,2]));
   7.123 @@ -271,8 +268,8 @@
   7.124  
   7.125  goal thy
   7.126   "!!evs. evs : otway lost ==>                               \
   7.127 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   7.128 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   7.129 +\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
   7.130 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
   7.131  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   7.132                                     insert_Key_singleton]) 1);
   7.133  by (Fast_tac 1);
   7.134 @@ -442,8 +439,8 @@
   7.135  by (etac otway.induct 1);
   7.136  by analz_Fake_tac;
   7.137  by (ALLGOALS
   7.138 -    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
   7.139 -				       analz_insert_Key_newK] @ pushes)
   7.140 +    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
   7.141 +				      analz_insert_Key_newK] 
   7.142  		            setloop split_tac [expand_if])));
   7.143  (*OR3*)
   7.144  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
     8.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Dec 19 11:54:19 1996 +0100
     8.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Dec 19 11:58:39 1996 +0100
     8.3 @@ -29,9 +29,9 @@
     8.4  
     8.5           (*Alice initiates a protocol run*)
     8.6      OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
     8.7 -          ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
     8.8 +          ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, 
     8.9                           Crypt (shrK A)
    8.10 -                               {|Nonce (newN evs), Agent A, Agent B|} |} 
    8.11 +                           {|Nonce (newN(length evs)), Agent A, Agent B|} |} 
    8.12                   # evs : otway lost"
    8.13  
    8.14           (*Bob's response to Alice's message.  Bob doesn't know who 
    8.15 @@ -41,8 +41,8 @@
    8.16               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    8.17            ==> Says B Server 
    8.18                    {|Nonce NA, Agent A, Agent B, X, 
    8.19 -                    Crypt 
    8.20 -                          (shrK B){|Nonce NA, Nonce (newN evs), Agent A, Agent B|}|}
    8.21 +                    Crypt (shrK B)
    8.22 +                      {|Nonce NA, Nonce(newN(length evs)), Agent A, Agent B|}|}
    8.23                   # evs : otway lost"
    8.24  
    8.25           (*The Server receives Bob's message and checks that the three NAs
    8.26 @@ -56,8 +56,8 @@
    8.27                 : set_of_list evs |]
    8.28            ==> Says Server B 
    8.29                    {|Nonce NA, 
    8.30 -                    Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
    8.31 -                    Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
    8.32 +                    Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
    8.33 +                    Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
    8.34                   # evs : otway lost"
    8.35  
    8.36           (*Bob receives the Server's (?) message and compares the Nonces with
     9.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Dec 19 11:54:19 1996 +0100
     9.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Dec 19 11:58:39 1996 +0100
     9.3 @@ -120,9 +120,8 @@
     9.4  (*** Future keys can't be seen or used! ***)
     9.5  
     9.6  (*Nobody can have SEEN keys that will be generated in the future. *)
     9.7 -goal thy "!!evs. evs : otway lost ==>             \
     9.8 -\                length evs <= length evs' -->    \
     9.9 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
    9.10 +goal thy "!!i. evs : otway lost ==>             \
    9.11 +\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
    9.12  by (parts_induct_tac 1);
    9.13  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    9.14  				    addDs [impOfSubs analz_subset_parts,
    9.15 @@ -134,10 +133,10 @@
    9.16  
    9.17  (*Variant: old messages must contain old keys!*)
    9.18  goal thy 
    9.19 - "!!evs. [| Says A B X : set_of_list evs;  \
    9.20 -\           Key (newK evt) : parts {X};    \
    9.21 -\           evs : otway lost               \
    9.22 -\        |] ==> length evt < length evs";
    9.23 + "!!evs. [| Says A B X : set_of_list evs;          \
    9.24 +\           Key (newK i) : parts {X};              \
    9.25 +\           evs : otway lost                       \
    9.26 +\        |] ==> i < length evs";
    9.27  by (rtac ccontr 1);
    9.28  by (dtac leI 1);
    9.29  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
    9.30 @@ -147,9 +146,8 @@
    9.31  
    9.32  (*Nobody can have USED keys that will be generated in the future.
    9.33    ...very like new_keys_not_seen*)
    9.34 -goal thy "!!evs. evs : otway lost ==>          \
    9.35 -\                length evs <= length evs' --> \
    9.36 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    9.37 +goal thy "!!i. evs : otway lost ==>          \
    9.38 +\           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
    9.39  by (parts_induct_tac 1);
    9.40  (*Fake, OR4: these messages send unknown (X) components*)
    9.41  by (EVERY
    9.42 @@ -180,9 +178,8 @@
    9.43  \           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    9.44  \             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
    9.45  \           evs : otway lost |]                                               \
    9.46 -\        ==> (EX evt: otway lost. K = Key(newK evt)) & \
    9.47 -\            (EX i. NA = Nonce i) &                    \
    9.48 -\            (EX j. NB = Nonce j)";
    9.49 +\        ==> (EX n. K = Key(newK n)) &                                        \
    9.50 +\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    9.51  by (etac rev_mp 1);
    9.52  by (etac otway.induct 1);
    9.53  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    9.54 @@ -194,14 +191,14 @@
    9.55      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
    9.56      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    9.57      assume_tac 7 THEN Full_simp_tac 7 THEN
    9.58 -    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
    9.59 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    9.60  
    9.61  
    9.62  (****
    9.63   The following is to prove theorems of the form
    9.64  
    9.65 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
    9.66 -          Key K : analz (sees lost Spy evs)
    9.67 +  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
    9.68 +  Key K : analz (sees lost Spy evs)
    9.69  
    9.70   A more general formula must be proved inductively.
    9.71  
    9.72 @@ -218,12 +215,11 @@
    9.73  by (etac otway.induct 1);
    9.74  by analz_Fake_tac;
    9.75  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
    9.76 -by (ALLGOALS (*Takes 28 secs*)
    9.77 +by (ALLGOALS (*Takes 18 secs*)
    9.78      (asm_simp_tac 
    9.79 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    9.80 -                         @ pushes)
    9.81 +     (!simpset addsimps [Un_assoc RS sym, 
    9.82 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
    9.83                 setloop split_tac [expand_if])));
    9.84 -(** LEVEL 5 **)
    9.85  (*OR4, Fake*) 
    9.86  by (EVERY (map spy_analz_tac [4,2]));
    9.87  (*Oops, OR3, Base*)
    9.88 @@ -233,8 +229,8 @@
    9.89  
    9.90  goal thy
    9.91   "!!evs. evs : otway lost ==>                                          \
    9.92 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
    9.93 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
    9.94 +\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
    9.95 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
    9.96  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
    9.97                                     insert_Key_singleton]) 1);
    9.98  by (Fast_tac 1);
    9.99 @@ -333,8 +329,8 @@
   9.100  by (etac otway.induct 1);
   9.101  by analz_Fake_tac;
   9.102  by (ALLGOALS
   9.103 -    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
   9.104 -				       analz_insert_Key_newK] @ pushes)
   9.105 +    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
   9.106 +				      analz_insert_Key_newK]
   9.107  		            setloop split_tac [expand_if])));
   9.108  (*OR3*)
   9.109  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    10.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Dec 19 11:54:19 1996 +0100
    10.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Dec 19 11:58:39 1996 +0100
    10.3 @@ -29,14 +29,15 @@
    10.4  
    10.5           (*Alice initiates a protocol run*)
    10.6      OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
    10.7 -          ==> Says A B {|Agent A, Agent B, Nonce (newN evs)|}
    10.8 +          ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|}
    10.9                   # evs : otway lost"
   10.10  
   10.11           (*Bob's response to Alice's message.  Bob doesn't know who 
   10.12  	   the sender is, hence the A' in the sender field.*)
   10.13      OR2  "[| evs: otway lost;  B ~= Server;
   10.14               Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
   10.15 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
   10.16 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, 
   10.17 +                              Nonce (newN(length evs))|}
   10.18                   # evs : otway lost"
   10.19  
   10.20           (*The Server receives Bob's message.  Then he sends a new
   10.21 @@ -45,8 +46,10 @@
   10.22               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   10.23                 : set_of_list evs |]
   10.24            ==> Says Server B 
   10.25 -               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
   10.26 -                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
   10.27 +               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, 
   10.28 +                                  Key(newK(length evs))|},
   10.29 +                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 
   10.30 +                                  Key(newK(length evs))|}|}
   10.31                # evs : otway lost"
   10.32  
   10.33           (*Bob receives the Server's (?) message and compares the Nonces with
    11.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Dec 19 11:54:19 1996 +0100
    11.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Dec 19 11:58:39 1996 +0100
    11.3 @@ -132,9 +132,8 @@
    11.4  (*** Future keys can't be seen or used! ***)
    11.5  
    11.6  (*Nobody can have SEEN keys that will be generated in the future. *)
    11.7 -goal thy "!!evs. evs : otway ==>               \
    11.8 -\                length evs <= length evs' --> \
    11.9 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
   11.10 +goal thy "!!i. evs : otway ==>               \
   11.11 +\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   11.12  by (parts_induct_tac 1);
   11.13  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   11.14  				    addDs [impOfSubs analz_subset_parts,
   11.15 @@ -146,10 +145,10 @@
   11.16  
   11.17  (*Variant: old messages must contain old keys!*)
   11.18  goal thy 
   11.19 - "!!evs. [| Says A B X : set_of_list evs;  \
   11.20 -\           Key (newK evt) : parts {X};    \
   11.21 -\           evs : otway                 \
   11.22 -\        |] ==> length evt < length evs";
   11.23 + "!!evs. [| Says A B X : set_of_list evs;          \
   11.24 +\           Key (newK i) : parts {X};    \
   11.25 +\           evs : otway                            \
   11.26 +\        |] ==> i < length evs";
   11.27  by (rtac ccontr 1);
   11.28  by (dtac leI 1);
   11.29  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   11.30 @@ -159,9 +158,8 @@
   11.31  
   11.32  (*** Future nonces can't be seen or used! ***)
   11.33  
   11.34 -goal thy "!!evs. evs : otway ==> \
   11.35 -\                length evs <= length evs' --> \
   11.36 -\                Nonce (newN evs') ~: parts (sees lost Spy evs)";
   11.37 +goal thy "!!i. evs : otway ==>               \
   11.38 +\              length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
   11.39  by (parts_induct_tac 1);
   11.40  by (REPEAT_FIRST
   11.41      (fast_tac (!claset addSEs partsEs
   11.42 @@ -175,10 +173,10 @@
   11.43  
   11.44  (*Variant: old messages must contain old nonces!*)
   11.45  goal thy 
   11.46 - "!!evs. [| Says A B X : set_of_list evs;    \
   11.47 -\           Nonce (newN evt) : parts {X};    \
   11.48 -\           evs : otway                 \
   11.49 -\        |] ==> length evt < length evs";
   11.50 + "!!evs. [| Says A B X : set_of_list evs;            \
   11.51 +\           Nonce (newN i) : parts {X};    \
   11.52 +\           evs : otway                              \
   11.53 +\        |] ==> i < length evs";
   11.54  by (rtac ccontr 1);
   11.55  by (dtac leI 1);
   11.56  by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   11.57 @@ -188,9 +186,8 @@
   11.58  
   11.59  (*Nobody can have USED keys that will be generated in the future.
   11.60    ...very like new_keys_not_seen*)
   11.61 -goal thy "!!evs. evs : otway ==> \
   11.62 -\                length evs <= length evs' --> \
   11.63 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   11.64 +goal thy "!!i. evs : otway ==>               \
   11.65 +\           length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
   11.66  by (parts_induct_tac 1);
   11.67  (*OR1 and OR3*)
   11.68  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   11.69 @@ -219,8 +216,8 @@
   11.70  goal thy 
   11.71   "!!evs. [| Says Server B \
   11.72  \            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
   11.73 -\           evs : otway |]                                   \
   11.74 -\        ==> (EX evt: otway. K = Key(newK evt)) &            \
   11.75 +\           evs : otway |]                                           \
   11.76 +\        ==> (EX n. K = Key(newK n)) &                               \
   11.77  \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   11.78  by (etac rev_mp 1);
   11.79  by (etac otway.induct 1);
   11.80 @@ -234,14 +231,14 @@
   11.81      dtac OR4_analz_sees_Spy 6 THEN
   11.82      forward_tac [Says_Server_message_form] 7 THEN
   11.83      assume_tac 7 THEN Full_simp_tac 7 THEN
   11.84 -    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   11.85 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   11.86  
   11.87  
   11.88  (****
   11.89   The following is to prove theorems of the form
   11.90  
   11.91 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   11.92 -          Key K : analz (sees lost Spy evs)
   11.93 +  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   11.94 +  Key K : analz (sees lost Spy evs)
   11.95  
   11.96   A more general formula must be proved inductively.
   11.97  
   11.98 @@ -267,12 +264,11 @@
   11.99  by (etac otway.induct 1);
  11.100  by analz_Fake_tac;
  11.101  by (REPEAT_FIRST (ares_tac [allI, lemma]));
  11.102 -by (ALLGOALS
  11.103 +by (ALLGOALS (*Takes 18 secs*)
  11.104      (asm_simp_tac 
  11.105 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
  11.106 -                         @ pushes)
  11.107 +     (!simpset addsimps [Un_assoc RS sym, 
  11.108 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
  11.109                 setloop split_tac [expand_if])));
  11.110 -(** LEVEL 7 **)
  11.111  (*OR4, OR2, Fake*) 
  11.112  by (EVERY (map spy_analz_tac [5,3,2]));
  11.113  (*Oops, OR3, Base*)
  11.114 @@ -282,8 +278,8 @@
  11.115  
  11.116  goal thy
  11.117   "!!evs. evs : otway ==>                               \
  11.118 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
  11.119 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
  11.120 +\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
  11.121 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
  11.122  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
  11.123                                     insert_Key_singleton]) 1);
  11.124  by (Fast_tac 1);
  11.125 @@ -293,7 +289,7 @@
  11.126  (*** The Key K uniquely identifies the Server's  message. **)
  11.127  
  11.128  goal thy 
  11.129 - "!!evs. evs : otway ==>                                                 \
  11.130 + "!!evs. evs : otway ==>                                                      \
  11.131  \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
  11.132  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
  11.133  \     B=B' & NA=NA' & NB=NB' & X=X'";
  11.134 @@ -332,8 +328,8 @@
  11.135  by (etac otway.induct 1);
  11.136  by analz_Fake_tac;
  11.137  by (ALLGOALS
  11.138 -    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
  11.139 -				       analz_insert_Key_newK] @ pushes)
  11.140 +    (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
  11.141 +				      analz_insert_Key_newK]
  11.142  		            setloop split_tac [expand_if])));
  11.143  (*OR3*)
  11.144  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    12.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Dec 19 11:54:19 1996 +0100
    12.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Dec 19 11:58:39 1996 +0100
    12.3 @@ -28,9 +28,9 @@
    12.4  
    12.5           (*Alice initiates a protocol run*)
    12.6      OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    12.7 -          ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    12.8 +          ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, 
    12.9                           Crypt (shrK A) 
   12.10 -                               {|Nonce (newN evs), Agent A, Agent B|} |} 
   12.11 +                            {|Nonce (newN(length evs)), Agent A, Agent B|} |} 
   12.12                   # evs : otway"
   12.13  
   12.14           (*Bob's response to Alice's message.  Bob doesn't know who 
   12.15 @@ -39,7 +39,7 @@
   12.16      OR2  "[| evs: otway;  B ~= Server;
   12.17               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
   12.18            ==> Says B Server 
   12.19 -                  {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
   12.20 +                  {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)), 
   12.21                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   12.22                   # evs : otway"
   12.23  
   12.24 @@ -55,8 +55,8 @@
   12.25                 : set_of_list evs |]
   12.26            ==> Says Server B 
   12.27                    {|Nonce NA, 
   12.28 -                    Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
   12.29 -                    Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
   12.30 +                    Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
   12.31 +                    Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
   12.32                   # evs : otway"
   12.33  
   12.34           (*Bob receives the Server's (?) message and compares the Nonces with
    13.1 --- a/src/HOL/Auth/Public.ML	Thu Dec 19 11:54:19 1996 +0100
    13.2 +++ b/src/HOL/Auth/Public.ML	Thu Dec 19 11:58:39 1996 +0100
    13.3 @@ -27,15 +27,14 @@
    13.4  (*** Basic properties of pubK ***)
    13.5  
    13.6  (*Injectiveness and freshness of new keys and nonces*)
    13.7 -AddIffs [inj_pubK RS inj_eq];
    13.8 -AddSDs  [newN_length];
    13.9 +AddIffs [inj_pubK RS inj_eq, inj_newN RS inj_eq];
   13.10  
   13.11  (** Rewrites should not refer to  initState(Friend i) 
   13.12      -- not in normal form! **)
   13.13  
   13.14  Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
   13.15  
   13.16 -goal thy "Nonce (newN evs) ~: parts (initState lost B)";
   13.17 +goal thy "Nonce (newN i) ~: parts (initState lost B)";
   13.18  by (agent.induct_tac "B" 1);
   13.19  by (Auto_tac ());
   13.20  qed "newN_notin_initState";
    14.1 --- a/src/HOL/Auth/Public.thy	Thu Dec 19 11:54:19 1996 +0100
    14.2 +++ b/src/HOL/Auth/Public.thy	Thu Dec 19 11:58:39 1996 +0100
    14.3 @@ -50,17 +50,16 @@
    14.4    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    14.5  
    14.6  
    14.7 -(*Agents generate "random" nonces.  These are uniquely determined by
    14.8 -  the length of their argument, a trace.*)
    14.9 +(*Agents generate "random" nonces, uniquely determined by their argument.*)
   14.10  consts
   14.11 -  newN :: "event list => nat"
   14.12 +  newN  :: nat => nat
   14.13  
   14.14  rules
   14.15  
   14.16    (*Public keys are disjoint, and never clash with private keys*)
   14.17 -  inj_pubK      "inj pubK"
   14.18 -  priK_neq_pubK "priK A ~= pubK B"
   14.19 +  inj_pubK        "inj pubK"
   14.20 +  priK_neq_pubK   "priK A ~= pubK B"
   14.21  
   14.22 -  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
   14.23 +  inj_newN        "inj newN"
   14.24  
   14.25  end
    15.1 --- a/src/HOL/Auth/Recur.ML	Thu Dec 19 11:54:19 1996 +0100
    15.2 +++ b/src/HOL/Auth/Recur.ML	Thu Dec 19 11:58:39 1996 +0100
    15.3 @@ -27,8 +27,8 @@
    15.4  \                       Agent Server|}      \
    15.5  \         : set_of_list evs";
    15.6  by (REPEAT (resolve_tac [exI,bexI] 1));
    15.7 -by (rtac (recur.Nil RS recur.NA1 RS 
    15.8 -	  (respond.One RSN (4,recur.NA3))) 2);
    15.9 +by (rtac (recur.Nil RS recur.RA1 RS 
   15.10 +	  (respond.One RSN (4,recur.RA3))) 2);
   15.11  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
   15.12  by (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]));
   15.13  result();
   15.14 @@ -42,9 +42,9 @@
   15.15  \                       Agent Server|}                          \
   15.16  \         : set_of_list evs";
   15.17  by (REPEAT (resolve_tac [exI,bexI] 1));
   15.18 -by (rtac (recur.Nil RS recur.NA1 RS recur.NA2 RS 
   15.19 -	  (respond.One RS respond.Cons RSN (4,recur.NA3)) RS
   15.20 -	  recur.NA4) 2);
   15.21 +by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
   15.22 +	  (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
   15.23 +	  recur.RA4) 2);
   15.24  by (REPEAT
   15.25      (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
   15.26       THEN
   15.27 @@ -60,9 +60,9 @@
   15.28  \                       Agent Server|}                          \
   15.29  \         : set_of_list evs";
   15.30  by (REPEAT (resolve_tac [exI,bexI] 1));
   15.31 -by (rtac (recur.Nil RS recur.NA1 RS recur.NA2 RS recur.NA2 RS 
   15.32 +by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
   15.33  	  (respond.One RS respond.Cons RS respond.Cons RSN
   15.34 -	   (4,recur.NA3)) RS recur.NA4 RS recur.NA4) 2);
   15.35 +	   (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
   15.36  by (REPEAT	(*SLOW: 37 seconds*)
   15.37      (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
   15.38       THEN
   15.39 @@ -104,30 +104,30 @@
   15.40  
   15.41  (** For reasoning about the encrypted portion of messages **)
   15.42  
   15.43 -val NA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
   15.44 +val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
   15.45  
   15.46  goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
   15.47  \                ==> RA : analz (sees lost Spy evs)";
   15.48  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   15.49 -qed "NA4_analz_sees_Spy";
   15.50 +qed "RA4_analz_sees_Spy";
   15.51  
   15.52 -(*NA2_analz... and NA4_analz... let us treat those cases using the same 
   15.53 +(*RA2_analz... and RA4_analz... let us treat those cases using the same 
   15.54    argument as for the Fake case.  This is possible for most, but not all,
   15.55 -  proofs: Fake does not invent new nonces (as in NA2), and of course Fake
   15.56 +  proofs: Fake does not invent new nonces (as in RA2), and of course Fake
   15.57    messages originate from the Spy. *)
   15.58  
   15.59 -bind_thm ("NA2_parts_sees_Spy",
   15.60 -          NA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   15.61 -bind_thm ("NA4_parts_sees_Spy",
   15.62 -          NA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   15.63 +bind_thm ("RA2_parts_sees_Spy",
   15.64 +          RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   15.65 +bind_thm ("RA4_parts_sees_Spy",
   15.66 +          RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   15.67  
   15.68  (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   15.69    harder to complete, since simplification does less for us.*)
   15.70  val parts_Fake_tac = 
   15.71      let val tac = forw_inst_tac [("lost","lost")] 
   15.72 -    in  tac NA2_parts_sees_Spy 4              THEN
   15.73 +    in  tac RA2_parts_sees_Spy 4              THEN
   15.74  	forward_tac [respond_imp_responses] 5 THEN
   15.75 -	tac NA4_parts_sees_Spy 6
   15.76 +	tac RA4_parts_sees_Spy 6
   15.77      end;
   15.78  
   15.79  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   15.80 @@ -159,10 +159,10 @@
   15.81   "!!evs. evs : recur lost \
   15.82  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   15.83  by (parts_induct_tac 1);
   15.84 -(*NA2*)
   15.85 +(*RA2*)
   15.86  by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
   15.87                        addss (!simpset)) 1);
   15.88 -(*NA3*)
   15.89 +(*RA3*)
   15.90  by (fast_tac (!claset addDs [Key_in_parts_respond]
   15.91                        addss (!simpset addsimps [parts_insert_sees])) 1);
   15.92  qed "Spy_see_shrK";
   15.93 @@ -191,7 +191,7 @@
   15.94  \                length evs <= i -->   \
   15.95  \                Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
   15.96  by (parts_induct_tac 1);
   15.97 -(*NA2*)
   15.98 +(*RA2*)
   15.99  by (best_tac (!claset addSEs partsEs 
  15.100  	              addSDs [parts_cut]
  15.101                        addDs  [Suc_leD]
  15.102 @@ -201,9 +201,9 @@
  15.103  			     impOfSubs parts_insert_subset_Un,
  15.104  			     Suc_leD]
  15.105  		      addss (!simpset)) 1);
  15.106 -(*For NA3*)
  15.107 +(*For RA3*)
  15.108  by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
  15.109 -(*NA1-NA4*)
  15.110 +(*RA1-RA4*)
  15.111  by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
  15.112  		              addss (!simpset)) 1));
  15.113  qed_spec_mp "new_keys_not_seen";
  15.114 @@ -235,7 +235,7 @@
  15.115  goal thy "!!i. evs : recur lost ==> \
  15.116  \              length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
  15.117  by (parts_induct_tac 1);
  15.118 -(*For NA3*)
  15.119 +(*For RA3*)
  15.120  by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
  15.121  by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  15.122                          addDs  [Nonce_in_parts_respond, parts_cut, Suc_leD]
  15.123 @@ -245,7 +245,7 @@
  15.124  			      impOfSubs parts_insert_subset_Un,
  15.125  			      Suc_leD]
  15.126  		      addss (!simpset)) 1);
  15.127 -(*NA1, NA2, NA4*)
  15.128 +(*RA1, RA2, RA4*)
  15.129  by (REPEAT_FIRST  (fast_tac (!claset 
  15.130                                addSEs partsEs
  15.131                                addEs [leD RS notE]
  15.132 @@ -279,13 +279,13 @@
  15.133  goal thy "!!i. evs : recur lost ==>          \
  15.134  \       length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
  15.135  by (parts_induct_tac 1);
  15.136 -(*NA3*)
  15.137 +(*RA3*)
  15.138  by (fast_tac (!claset addDs  [Key_in_keysFor_parts_respond, Suc_leD]
  15.139  		      addss  (!simpset addsimps [parts_insert_sees])) 4);
  15.140 -(*NA2*)
  15.141 +(*RA2*)
  15.142  by (fast_tac (!claset addSEs partsEs 
  15.143  	              addDs  [Suc_leD] addss (!simpset)) 3);
  15.144 -(*Fake, NA1, NA4*)
  15.145 +(*Fake, RA1, RA4*)
  15.146  by (REPEAT 
  15.147      (best_tac
  15.148        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
  15.149 @@ -308,14 +308,14 @@
  15.150  
  15.151  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
  15.152  val analz_Fake_tac = 
  15.153 -    dres_inst_tac [("lost","lost")] NA2_analz_sees_Spy 4 THEN 
  15.154 +    dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
  15.155      forward_tac [respond_imp_responses] 5                THEN
  15.156 -    dres_inst_tac [("lost","lost")] NA4_analz_sees_Spy 6;
  15.157 +    dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
  15.158  
  15.159  
  15.160  (** Session keys are not used to encrypt other session keys **)
  15.161  
  15.162 -(*Version for "responses" relation.  Handles case NA3 in the theorem below.  
  15.163 +(*Version for "responses" relation.  Handles case RA3 in the theorem below.  
  15.164    Note that it holds for *any* set H (not just "sees lost Spy evs")
  15.165    satisfying the inductive hypothesis.*)
  15.166  goal thy  
  15.167 @@ -340,12 +340,12 @@
  15.168  \           (K : newK``I | Key K : analz (sees lost Spy evs))";
  15.169  by (etac recur.induct 1);
  15.170  by analz_Fake_tac;
  15.171 -be ssubst 4;	(*NA2: DELETE needless definition of PA!*)
  15.172 +be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
  15.173  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
  15.174  by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
  15.175  (*Base*)
  15.176  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  15.177 -(*NA4, NA2, Fake*) 
  15.178 +(*RA4, RA2, Fake*) 
  15.179  by (REPEAT (spy_analz_tac 1));
  15.180  val raw_analz_image_newK = result();
  15.181  qed_spec_mp "analz_image_newK";
  15.182 @@ -381,12 +381,12 @@
  15.183  \                (Nonce (newN i) : parts {X} --> \
  15.184  \                 Hash X ~: parts (sees lost Spy evs))";
  15.185  be recur.induct 1;
  15.186 -be ssubst 4;	(*NA2: DELETE needless definition of PA!*)
  15.187 +be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
  15.188  by parts_Fake_tac;
  15.189 -(*NA3 requires a further induction*)
  15.190 +(*RA3 requires a further induction*)
  15.191  be responses.induct 5;
  15.192  by (ALLGOALS Asm_simp_tac);
  15.193 -(*NA2*)
  15.194 +(*RA2*)
  15.195  by (best_tac (!claset addDs  [Suc_leD, parts_cut]
  15.196                        addEs  [leD RS notE,
  15.197  			      new_nonces_not_seen RSN(2,rev_notE)]
  15.198 @@ -405,7 +405,7 @@
  15.199  
  15.200  
  15.201  (** The Nonce NA uniquely identifies A's message. 
  15.202 -    This theorem applies to rounds NA1 and NA2!
  15.203 +    This theorem applies to rounds RA1 and RA2!
  15.204  **)
  15.205  
  15.206  goal thy 
  15.207 @@ -414,15 +414,15 @@
  15.208  \        Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
  15.209  \          : parts (sees lost Spy evs)  -->  B=B' & P=P'";
  15.210  be recur.induct 1;
  15.211 -be ssubst 4;	(*NA2: DELETE needless definition of PA!*)
  15.212 -(*For better simplification of NA2*)
  15.213 +be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
  15.214 +(*For better simplification of RA2*)
  15.215  by (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 4);
  15.216  by parts_Fake_tac;
  15.217 -(*NA3 requires a further induction*)
  15.218 +(*RA3 requires a further induction*)
  15.219  be responses.induct 5;
  15.220  by (ALLGOALS Asm_simp_tac);
  15.221  by (step_tac (!claset addSEs partsEs) 1);
  15.222 -(*NA3: inductive case*)
  15.223 +(*RA3: inductive case*)
  15.224  by (best_tac (!claset addss  (!simpset)) 5);
  15.225  (*Fake*)
  15.226  by (best_tac (!claset addSIs [exI]
  15.227 @@ -433,13 +433,13 @@
  15.228  by (fast_tac (!claset addss (!simpset)) 1);
  15.229  
  15.230  by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
  15.231 -(*NA1: creation of new Nonce.  Move assertion into global context*)
  15.232 +(*RA1: creation of new Nonce.  Move assertion into global context*)
  15.233  by (expand_case_tac "NA = ?y" 1);
  15.234  by (best_tac (!claset addSIs [exI]
  15.235                        addEs  [Hash_new_nonces_not_seen]
  15.236  		      addss (!simpset)) 1);
  15.237  by (best_tac (!claset addss  (!simpset)) 1);
  15.238 -(*NA2: creation of new Nonce*)
  15.239 +(*RA2: creation of new Nonce*)
  15.240  by (expand_case_tac "NA = ?y" 1);
  15.241  by (best_tac (!claset addSIs [exI]
  15.242                        addDs  [parts_cut]
  15.243 @@ -510,7 +510,7 @@
  15.244  
  15.245  
  15.246  (*The Server does not send such messages.  This theorem lets us avoid
  15.247 -  assuming B~=Server in NA4.*)
  15.248 +  assuming B~=Server in RA4.*)
  15.249  goal thy 
  15.250   "!!evs. evs : recur lost       \
  15.251  \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
  15.252 @@ -557,7 +557,7 @@
  15.253  qed "unique_session_keys";
  15.254  
  15.255  
  15.256 -(** Crucial secrecy property: Spy does not see the keys sent in msg NA3
  15.257 +(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
  15.258      Does not in itself guarantee security: an attack could violate 
  15.259      the premises, e.g. by having A=Spy **)
  15.260  
  15.261 @@ -614,24 +614,24 @@
  15.262  \            Key K ~: analz (sees lost Spy evs)";
  15.263  by (etac recur.induct 1);
  15.264  by analz_Fake_tac;
  15.265 -be ssubst 4;	(*NA2: DELETE needless definition of PA!*)
  15.266 +be ssubst 4;	(*RA2: DELETE needless definition of PA!*)
  15.267  by (ALLGOALS
  15.268      (asm_simp_tac
  15.269       (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] 
  15.270                 setloop split_tac [expand_if])));
  15.271 -(*NA4*)
  15.272 +(*RA4*)
  15.273  by (spy_analz_tac 4);
  15.274  (*Fake*)
  15.275  by (spy_analz_tac 1);
  15.276  by (step_tac (!claset delrules [impCE]) 1);
  15.277 -(*NA2*)
  15.278 +(*RA2*)
  15.279  by (spy_analz_tac 1);
  15.280 -(*NA3, case 2: K is an old key*)
  15.281 +(*RA3, case 2: K is an old key*)
  15.282  by (fast_tac (!claset addSDs [resp_analz_insert]
  15.283  		      addSEs partsEs
  15.284                        addDs [Key_in_parts_respond]
  15.285  	              addEs [Says_imp_old_keys RS less_irrefl]) 2);
  15.286 -(*NA3, case 1: use lemma previously proved by induction*)
  15.287 +(*RA3, case 1: use lemma previously proved by induction*)
  15.288  by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
  15.289  			      (2,rev_notE)]) 1);
  15.290  bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
  15.291 @@ -652,7 +652,7 @@
  15.292  
  15.293  (**** Authenticity properties for Agents ****)
  15.294  
  15.295 -(*Only NA1 or NA2 can have caused such a part of a message to appear.*)
  15.296 +(*Only RA1 or RA2 can have caused such a part of a message to appear.*)
  15.297  goal thy 
  15.298   "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
  15.299  \             : parts (sees lost Spy evs);                        \
  15.300 @@ -662,9 +662,9 @@
  15.301  \             : set_of_list evs";
  15.302  be rev_mp 1;
  15.303  by (parts_induct_tac 1);
  15.304 -(*NA3*)
  15.305 +(*RA3*)
  15.306  by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2);
  15.307 -(*NA2*)
  15.308 +(*RA2*)
  15.309  by ((REPEAT o CHANGED)     (*Push in XA*)
  15.310      (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
  15.311  by (best_tac (!claset addSEs partsEs 
  15.312 @@ -692,22 +692,22 @@
  15.313    in a run, then it originated with the Server!*)
  15.314  goal thy 
  15.315   "!!evs. [| A ~: lost;  A ~= Spy;  evs : recur lost |]                 \
  15.316 -\    ==> Crypt (shrK A) {|Key K, Agent B, NA|} : parts (sees lost Spy evs) \
  15.317 +\    ==> Crypt (shrK A) {|Key K, Agent A', NA|} : parts (sees lost Spy evs) \
  15.318  \        --> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
  15.319  \                       Agent A, Agent B, NA, P|}      \
  15.320  \             : set_of_list evs                                    \
  15.321  \         --> (EX C RC. Says Server C RC : set_of_list evs &  \
  15.322 -\                       Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RC})";
  15.323 +\                       Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC})";
  15.324  by (parts_induct_tac 1);
  15.325 -(*NA4*)
  15.326 +(*RA4*)
  15.327  by (best_tac (!claset addSEs [MPair_parts]
  15.328  	              addSDs [Hash_auth_sender]
  15.329  		      addSIs [disjI2]) 4);
  15.330 -(*NA1: it cannot be a new Nonce, contradiction.*)
  15.331 +(*RA1: it cannot be a new Nonce, contradiction.*)
  15.332  by (fast_tac (!claset delrules [impCE]
  15.333  	              addSEs [nonce_not_seen_now, MPair_parts]
  15.334                        addDs  [parts.Body]) 1);
  15.335 -(*NA2: it cannot be a new Nonce, contradiction.*)
  15.336 +(*RA2: it cannot be a new Nonce, contradiction.*)
  15.337  by ((REPEAT o CHANGED)     (*Push in XA*)
  15.338      (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
  15.339  by (deepen_tac (!claset delrules [impCE]
  15.340 @@ -715,7 +715,7 @@
  15.341  	              addSEs [MPair_parts]
  15.342                        addDs  [parts_cut, parts.Body]
  15.343                        addss  (!simpset)) 0 1);
  15.344 -(*NA3*)  (** LEVEL 5 **)
  15.345 +(*RA3*)  (** LEVEL 5 **)
  15.346  by (REPEAT (safe_step_tac (!claset addSEs [responses_no_Hash_Server]
  15.347  	                           delrules [impCE]) 1));
  15.348  by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
  15.349 @@ -727,13 +727,13 @@
  15.350    then the key really did come from the Server!*)
  15.351  goal thy 
  15.352   "!!evs. [| Says B' A RA : set_of_list evs;                        \
  15.353 -\           Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RA};    \
  15.354 +\           Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA};    \
  15.355  \           Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
  15.356  \                       Agent A, Agent B, NA, P|}   \
  15.357  \            : set_of_list evs;                                    \
  15.358  \           A ~: lost;  A ~= Spy;  evs : recur lost |]             \
  15.359  \        ==> EX C RC. Says Server C RC : set_of_list evs &  \
  15.360 -\                       Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RC}";
  15.361 +\                       Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC}";
  15.362  by (best_tac (!claset addSIs [Crypt_imp_Server_msg]
  15.363                        addDs  [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)]
  15.364                        addss  (!simpset)) 1);
  15.365 @@ -744,12 +744,12 @@
  15.366    then the only other agent who knows the key is B.*)
  15.367  goal thy 
  15.368   "!!evs. [| Says B' A RA : set_of_list evs;                           \
  15.369 -\           Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RA};       \
  15.370 +\           Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA};      \
  15.371  \           Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
  15.372  \                      Agent A, Agent B, NA, P|}                      \
  15.373  \            : set_of_list evs;                                       \
  15.374 -\           C ~: {A,B,Server};                                        \
  15.375 -\           A ~: lost;  B ~: lost;  A ~= Spy;  evs : recur lost |]   \
  15.376 +\           C ~: {A,A',Server};                                       \
  15.377 +\           A ~: lost;  A' ~: lost;  A ~= Spy;  evs : recur lost |]   \
  15.378  \        ==> Key K ~: analz (sees lost C evs)";
  15.379  by (dtac Agent_trust 1 THEN REPEAT_FIRST assume_tac);
  15.380  by (fast_tac (!claset addSEs [Agent_not_see_encrypted_key RSN(2,rev_notE)]) 1);
    16.1 --- a/src/HOL/Auth/Recur.thy	Thu Dec 19 11:54:19 1996 +0100
    16.2 +++ b/src/HOL/Auth/Recur.thy	Thu Dec 19 11:58:39 1996 +0100
    16.3 @@ -77,7 +77,7 @@
    16.4  
    16.5           (*Alice initiates a protocol run.
    16.6             "Agent Server" is just a placeholder, to terminate the nesting.*)
    16.7 -    NA1  "[| evs: recur lost;  A ~= B;  A ~= Server;
    16.8 +    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;
    16.9               MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|]
   16.10            ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost"
   16.11  
   16.12 @@ -85,7 +85,7 @@
   16.13             XA should be the Hash of the remaining components with KA, but
   16.14  		Bob cannot check that.
   16.15             P is the previous recur message from Alice's caller.*)
   16.16 -    NA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
   16.17 +    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
   16.18               Says A' B PA : set_of_list evs;  
   16.19               PA = {|XA, Agent A, Agent B, Nonce NA, P|};
   16.20               MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |]
   16.21 @@ -93,14 +93,14 @@
   16.22  
   16.23           (*The Server receives and decodes Bob's message.  Then he generates
   16.24             a new session key and a response.*)
   16.25 -    NA3  "[| evs: recur lost;  B ~= Server;
   16.26 +    RA3  "[| evs: recur lost;  B ~= Server;
   16.27               Says B' Server PB : set_of_list evs;
   16.28               (0,PB,RB) : respond (length evs) |]
   16.29            ==> Says Server B RB # evs : recur lost"
   16.30  
   16.31           (*Bob receives the returned message and compares the Nonces with
   16.32  	   those in the message he previously sent the Server.*)
   16.33 -    NA4  "[| evs: recur lost;  A ~= B;  
   16.34 +    RA4  "[| evs: recur lost;  A ~= B;  
   16.35               Says C' B {|Agent B, 
   16.36                           Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
   16.37                           Agent B, 
    17.1 --- a/src/HOL/Auth/Shared.ML	Thu Dec 19 11:54:19 1996 +0100
    17.2 +++ b/src/HOL/Auth/Shared.ML	Thu Dec 19 11:58:39 1996 +0100
    17.3 @@ -26,62 +26,35 @@
    17.4  
    17.5  (*** Basic properties of shrK and newK ***)
    17.6  
    17.7 -goalw thy [newN_def] "!!evs. newN evs = newN evt ==> length evs = length evt";
    17.8 -by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
    17.9 -qed "newN_length";
   17.10 -
   17.11 -goalw thy [newK_def] "!!evs. newK evs = newK evt ==> length evs = length evt";
   17.12 -by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
   17.13 -qed "newK_length";
   17.14 -
   17.15 -goalw thy [newK_def] "newK evs ~= shrK A";
   17.16 -by (rtac random_neq_shrK 1);
   17.17 -qed "newK_neq_shrK";
   17.18 -
   17.19 -goalw thy [newK_def] "isSymKey (newK evs)";
   17.20 -by (rtac isSym_random 1);
   17.21 -qed "isSym_newK";
   17.22 +(*Injectiveness and freshness of new keys and nonces*)
   17.23 +AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, 
   17.24 +	 inj_newK RS inj_eq, inj_nPair RS inj_eq];
   17.25  
   17.26  (* invKey (shrK A) = shrK A *)
   17.27  bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
   17.28  
   17.29 -(* invKey (random x) = random x *)
   17.30 -bind_thm ("invKey_random", rewrite_rule [isSymKey_def] isSym_random);
   17.31 -
   17.32 -(* invKey (newK evs) = newK evs *)
   17.33 +(* invKey (newK i) = newK i *)
   17.34  bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
   17.35 -Addsimps [invKey_shrK, invKey_random, invKey_newK];
   17.36 +Addsimps [invKey_shrK, invKey_newK];
   17.37  
   17.38 -goal thy "!!K. random x = invKey K ==> random x = K";
   17.39 -by (rtac (invKey_eq RS iffD1) 1);
   17.40 -by (Simp_tac 1);
   17.41 -val random_invKey = result();
   17.42 -
   17.43 -AddSDs [random_invKey, sym RS random_invKey];
   17.44 -
   17.45 -goal thy "!!K. newK evs = invKey K ==> newK evs = K";
   17.46 +goal thy "!!K. newK i = invKey K ==> newK i = K";
   17.47  by (rtac (invKey_eq RS iffD1) 1);
   17.48  by (Simp_tac 1);
   17.49  val newK_invKey = result();
   17.50  
   17.51  AddSDs [newK_invKey, sym RS newK_invKey];
   17.52  
   17.53 -(*Injectiveness and freshness of new keys and nonces*)
   17.54 -AddIffs [inj_shrK RS inj_eq, inj_random RS inj_eq];
   17.55 -AddSDs  [newN_length, newK_length];
   17.56 -
   17.57 -Addsimps [random_neq_shrK, random_neq_shrK RS not_sym,
   17.58 -	  newK_neq_shrK, newK_neq_shrK RS not_sym];
   17.59 +Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
   17.60  
   17.61  (** Rewrites should not refer to  initState(Friend i) 
   17.62      -- not in normal form! **)
   17.63  
   17.64 -goal thy "Key (newK evs) ~: parts (initState lost B)";
   17.65 +goal thy "Key (newK i) ~: parts (initState lost B)";
   17.66  by (agent.induct_tac "B" 1);
   17.67  by (Auto_tac ());
   17.68  qed "newK_notin_initState";
   17.69  
   17.70 -goal thy "Nonce (newN evs) ~: parts (initState lost B)";
   17.71 +goal thy "Nonce (newN i) ~: parts (initState lost B)";
   17.72  by (agent.induct_tac "B" 1);
   17.73  by (Auto_tac ());
   17.74  qed "newN_notin_initState";
   17.75 @@ -105,12 +78,6 @@
   17.76  qed "shrK_notin_image_newK";
   17.77  Addsimps [shrK_notin_image_newK];
   17.78  
   17.79 -goal thy "shrK A ~: random``E";
   17.80 -by (agent.induct_tac "A" 1);
   17.81 -by (Auto_tac ());
   17.82 -qed "shrK_notin_image_random";
   17.83 -Addsimps [shrK_notin_image_random];
   17.84 -
   17.85  
   17.86  (*** Function "sees" ***)
   17.87  
    18.1 --- a/src/HOL/Auth/Shared.thy	Thu Dec 19 11:54:19 1996 +0100
    18.2 +++ b/src/HOL/Auth/Shared.thy	Thu Dec 19 11:58:39 1996 +0100
    18.3 @@ -44,24 +44,25 @@
    18.4    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    18.5  
    18.6  
    18.7 -(*Agents generate "random" numbers for use as symmetric keys, as well as
    18.8 -  nonces.*)
    18.9 +(*Agents generate random (symmetric) keys and nonces.
   18.10 +  The numeric argument is typically the length of the current trace.
   18.11 +  An injective pairing function allows multiple keys/nonces to be generated
   18.12 +	in one protocol round.  A typical candidate for npair(i,j) is
   18.13 +	2^j(2i+1)
   18.14 +*)
   18.15  
   18.16  consts
   18.17 -  random :: "nat*nat => nat"
   18.18 -
   18.19 -constdefs
   18.20 -  newN   :: event list => nat
   18.21 -  "newN evs == random (length evs, 0)"
   18.22 -
   18.23 -  newK   :: event list => nat
   18.24 -  "newK evs == random (length evs, 1)"
   18.25 +  nPair :: "nat*nat => nat"
   18.26 +  newN  :: "nat => nat"
   18.27 +  newK  :: "nat => key"
   18.28  
   18.29  rules
   18.30    inj_shrK        "inj shrK"
   18.31 -  inj_random      "inj random"
   18.32 +  inj_nPair       "inj nPair"
   18.33 +  inj_newN        "inj newN"
   18.34 +  inj_newK        "inj newK"
   18.35  
   18.36 -  random_neq_shrK "random ij ~= shrK A" 
   18.37 -  isSym_random    "isSymKey (random ij)"
   18.38 +  newK_neq_shrK   "newK i ~= shrK A" 
   18.39 +  isSym_newK      "isSymKey (newK i)"
   18.40  
   18.41  end
    19.1 --- a/src/HOL/Auth/WooLam.ML	Thu Dec 19 11:54:19 1996 +0100
    19.2 +++ b/src/HOL/Auth/WooLam.ML	Thu Dec 19 11:58:39 1996 +0100
    19.3 @@ -96,9 +96,8 @@
    19.4  
    19.5  (*** Future nonces can't be seen or used! ***)
    19.6  
    19.7 -goal thy "!!evs. evs : woolam ==> \
    19.8 -\                length evs <= length evt --> \
    19.9 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   19.10 +goal thy "!!i. evs : woolam ==>             \
   19.11 +\             length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)";
   19.12  by (parts_induct_tac 1);
   19.13  by (REPEAT_FIRST (fast_tac (!claset 
   19.14                                addSEs partsEs
    20.1 --- a/src/HOL/Auth/WooLam.thy	Thu Dec 19 11:54:19 1996 +0100
    20.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Dec 19 11:58:39 1996 +0100
    20.3 @@ -37,7 +37,7 @@
    20.4           (*Bob responds to Alice's message with a challenge.*)
    20.5      WL2  "[| evs: woolam;  A ~= B;
    20.6               Says A' B (Agent A) : set_of_list evs |]
    20.7 -          ==> Says B A (Nonce (newN evs)) # evs : woolam"
    20.8 +          ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
    20.9  
   20.10           (*Alice responds to Bob's challenge by encrypting NB with her key.
   20.11             B is *not* properly determined -- Alice essentially broadcasts
    21.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Dec 19 11:54:19 1996 +0100
    21.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Dec 19 11:58:39 1996 +0100
    21.3 @@ -118,9 +118,8 @@
    21.4  (*** Future keys can't be seen or used! ***)
    21.5  
    21.6  (*Nobody can have SEEN keys that will be generated in the future. *)
    21.7 -goal thy "!!evs. evs : yahalom lost ==> \
    21.8 -\                length evs <= length evs' --> \
    21.9 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
   21.10 +goal thy "!!i. evs : yahalom lost ==>        \
   21.11 +\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   21.12  by (parts_induct_tac 1);
   21.13  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   21.14  				    addDs [impOfSubs analz_subset_parts,
   21.15 @@ -132,10 +131,10 @@
   21.16  
   21.17  (*Variant: old messages must contain old keys!*)
   21.18  goal thy 
   21.19 - "!!evs. [| Says A B X : set_of_list evs;  \
   21.20 -\           Key (newK evt) : parts {X};    \
   21.21 -\           evs : yahalom lost                 \
   21.22 -\        |] ==> length evt < length evs";
   21.23 + "!!evs. [| Says A B X : set_of_list evs;          \
   21.24 +\           Key (newK i) : parts {X};    \
   21.25 +\           evs : yahalom lost                     \
   21.26 +\        |] ==> i < length evs";
   21.27  by (rtac ccontr 1);
   21.28  by (dtac leI 1);
   21.29  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   21.30 @@ -144,7 +143,7 @@
   21.31  
   21.32  
   21.33  (*Ready-made for the classical reasoner*)
   21.34 -goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|}  \
   21.35 +goal thy "!!evs. [| Says A B {|Crypt K {|b,Key(newK(length evs)),na,nb|}, X|}\
   21.36  \                   : set_of_list evs;  evs : yahalom lost |]              \
   21.37  \                ==> R";
   21.38  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   21.39 @@ -155,9 +154,8 @@
   21.40  
   21.41  (*Nobody can have USED keys that will be generated in the future.
   21.42    ...very like new_keys_not_seen*)
   21.43 -goal thy "!!evs. evs : yahalom lost ==> \
   21.44 -\                length evs <= length evs' --> \
   21.45 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   21.46 +goal thy "!!i. evs : yahalom lost ==>        \
   21.47 +\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
   21.48  by (parts_induct_tac 1);
   21.49  (*YM1, YM2 and YM3*)
   21.50  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   21.51 @@ -187,10 +185,10 @@
   21.52  (*Describes the form of K when the Server sends this message.  Useful for
   21.53    Oops as well as main secrecy property.*)
   21.54  goal thy 
   21.55 - "!!evs. [| Says Server A                                           \
   21.56 + "!!evs. [| Says Server A                                                    \
   21.57  \            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
   21.58 -\           evs : yahalom lost |]                                   \
   21.59 -\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   21.60 +\           evs : yahalom lost |]                                            \
   21.61 +\        ==> EX i. K = Key(newK i)";
   21.62  by (etac rev_mp 1);
   21.63  by (etac yahalom.induct 1);
   21.64  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   21.65 @@ -202,14 +200,14 @@
   21.66      forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   21.67      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   21.68      assume_tac 7 THEN Full_simp_tac 7 THEN
   21.69 -    REPEAT ((etac bexE ORELSE' hyp_subst_tac) 7);
   21.70 +    REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   21.71  
   21.72  
   21.73  (****
   21.74   The following is to prove theorems of the form
   21.75  
   21.76 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   21.77 -          Key K : analz (sees lost Spy evs)
   21.78 +  Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   21.79 +  Key K : analz (sees lost Spy evs)
   21.80  
   21.81   A more general formula must be proved inductively.
   21.82  
   21.83 @@ -221,7 +219,7 @@
   21.84    We require that agents should behave like this subsequently also.*)
   21.85  goal thy 
   21.86   "!!evs. evs : yahalom lost ==> \
   21.87 -\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
   21.88 +\        (Crypt (newK i) X) : parts (sees lost Spy evs) & \
   21.89  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   21.90  by (etac yahalom.induct 1);
   21.91  by parts_Fake_tac;
   21.92 @@ -244,12 +242,11 @@
   21.93  by (etac yahalom.induct 1);
   21.94  by analz_Fake_tac;
   21.95  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   21.96 -by (ALLGOALS
   21.97 +by (ALLGOALS (*Takes 11 secs*)
   21.98      (asm_simp_tac 
   21.99 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
  21.100 -                         @ pushes)
  21.101 +     (!simpset addsimps [Un_assoc RS sym, 
  21.102 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
  21.103                 setloop split_tac [expand_if])));
  21.104 -(** LEVEL 5 **)
  21.105  (*YM4, Fake*) 
  21.106  by (EVERY (map spy_analz_tac [4, 2]));
  21.107  (*Oops, YM3, Base*)
  21.108 @@ -258,8 +255,8 @@
  21.109  
  21.110  goal thy
  21.111   "!!evs. evs : yahalom lost ==>                               \
  21.112 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
  21.113 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
  21.114 +\        Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
  21.115 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
  21.116  by (asm_simp_tac (HOL_ss addsimps [analz_image_newK, 
  21.117                                     insert_Key_singleton]) 1);
  21.118  by (Fast_tac 1);
  21.119 @@ -295,11 +292,7 @@
  21.120  \           : set_of_list evs;                                      \
  21.121  \          evs : yahalom lost |]                                    \
  21.122  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
  21.123 -by (dtac lemma 1);
  21.124 -by (REPEAT (etac exE 1));
  21.125 -(*Duplicate the assumption*)
  21.126 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
  21.127 -by (fast_tac (!claset addSDs [spec]) 1);
  21.128 +by (prove_unique_tac lemma 1);
  21.129  qed "unique_session_keys";
  21.130  
  21.131  
  21.132 @@ -331,14 +324,13 @@
  21.133  by analz_Fake_tac;
  21.134  by (ALLGOALS
  21.135      (asm_simp_tac 
  21.136 -     (!simpset addsimps ([not_parts_not_analz,
  21.137 -                          analz_insert_Key_newK] @ pushes)
  21.138 +     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
  21.139                 setloop split_tac [expand_if])));
  21.140  (*YM3*)
  21.141  by (Fast_tac 2);  (*uses Says_too_new_key*)
  21.142  (*OR4, Fake*) 
  21.143  by (REPEAT_FIRST spy_analz_tac);
  21.144 -(*Oops*) (** LEVEL 6 **)
  21.145 +(*Oops*)
  21.146  by (fast_tac (!claset delrules [disjE] 
  21.147                        addDs [unique_session_keys]
  21.148                        addss (!simpset)) 1);
  21.149 @@ -381,8 +373,8 @@
  21.150   "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
  21.151  \           B ~: lost;  evs : yahalom lost |]                           \
  21.152  \        ==> EX NA NB. Says Server A                                    \
  21.153 -\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
  21.154 -\                                  Nonce NA, Nonce NB|},       \
  21.155 +\                        {|Crypt (shrK A) {|Agent B, Key K,             \
  21.156 +\                                  Nonce NA, Nonce NB|},                \
  21.157  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  21.158  \                       : set_of_list evs";
  21.159  by (etac rev_mp 1);
  21.160 @@ -394,9 +386,9 @@
  21.161  
  21.162  (*** General properties of nonces ***)
  21.163  
  21.164 -goal thy "!!evs. evs : yahalom lost ==> \
  21.165 -\                length evs <= length evt --> \
  21.166 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
  21.167 +goal thy "!!evs. evs : yahalom lost ==>       \
  21.168 +\                length evs <= i --> \
  21.169 +\                Nonce (newN i) ~: parts (sees lost Spy evs)";
  21.170  by (parts_induct_tac 1);
  21.171  by (REPEAT_FIRST (fast_tac (!claset 
  21.172                                addSEs partsEs
  21.173 @@ -411,10 +403,10 @@
  21.174  
  21.175  (*Variant: old messages must contain old nonces!*)
  21.176  goal thy 
  21.177 - "!!evs. [| Says A B X : set_of_list evs;      \
  21.178 -\           Nonce (newN evt) : parts {X};      \
  21.179 -\           evs : yahalom lost                 \
  21.180 -\        |] ==> length evt < length evs";
  21.181 + "!!evs. [| Says A B X : set_of_list evs;              \
  21.182 +\           Nonce (newN i) : parts {X};      \
  21.183 +\           evs : yahalom lost                         \
  21.184 +\        |] ==> i < length evs";
  21.185  by (rtac ccontr 1);
  21.186  by (dtac leI 1);
  21.187  by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
  21.188 @@ -427,11 +419,19 @@
  21.189  val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
  21.190  
  21.191  goal thy 
  21.192 - "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
  21.193 + "!!evs. evs : yahalom lost ==> \
  21.194 +\   EX NA' A' B'. ALL NA A B. \
  21.195  \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
  21.196  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
  21.197 -by (parts_induct_tac 1);  (*100 seconds??*)
  21.198 -by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
  21.199 +by (etac yahalom.induct 1 THEN parts_Fake_tac);
  21.200 +(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
  21.201 +by (REPEAT (etac exE 2) THEN 
  21.202 +    best_tac (!claset addSIs [exI]
  21.203 +		      addDs [impOfSubs Fake_parts_insert]
  21.204 +      	              addss (!simpset)) 2);
  21.205 +(*Base case*)
  21.206 +by (fast_tac (!claset addss (!simpset)) 1);
  21.207 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
  21.208  (*YM2: creation of new Nonce.  Move assertion into global context*)
  21.209  by (expand_case_tac "NB = ?y" 1);
  21.210  by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
  21.211 @@ -444,11 +444,7 @@
  21.212  \                  : parts (sees lost Spy evs);         \
  21.213  \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
  21.214  \        ==> NA' = NA & A' = A & B' = B";
  21.215 -by (dtac lemma 1);
  21.216 -by (REPEAT (etac exE 1));
  21.217 -(*Duplicate the assumption*)
  21.218 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
  21.219 -by (fast_tac (!claset addSDs [spec]) 1);
  21.220 +by (prove_unique_tac lemma 1);
  21.221  qed "unique_NB";
  21.222  
  21.223  (*OLD VERSION
  21.224 @@ -627,7 +623,7 @@
  21.225  \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
  21.226  by (etac yahalom.induct 1);
  21.227  by analz_Fake_tac;
  21.228 -by (ALLGOALS  (*28 seconds*)
  21.229 +by (ALLGOALS  (*22 seconds*)
  21.230      (asm_simp_tac 
  21.231       (!simpset addsimps ([not_parts_not_analz,
  21.232                            analz_image_newK,
  21.233 @@ -638,11 +634,10 @@
  21.234  by (fast_tac (!claset addss (!simpset)) 1);
  21.235  (*Fake*) (** LEVEL 4 **)
  21.236  by (spy_analz_tac 1);
  21.237 -(*YM1-YM3*) (*29 seconds*)
  21.238 +(*YM1-YM3*) (*24 seconds*)
  21.239  by (EVERY (map grind_tac [3,2,1]));
  21.240  (*Oops*)
  21.241  by (Full_simp_tac 2);
  21.242 -by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2));
  21.243  by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
  21.244  by (grind_tac 2);
  21.245  by (fast_tac (!claset delrules [bexI] 
  21.246 @@ -672,11 +667,11 @@
  21.247    was distributed with that key.  The more general form above is required
  21.248    for the induction to carry through.*)
  21.249  goal thy 
  21.250 - "!!evs. [| Says Server A                                                     \
  21.251 -\            {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
  21.252 -\           : set_of_list evs;                                                \
  21.253 -\           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
  21.254 -\           evs : yahalom lost |]                                             \
  21.255 + "!!evs. [| Says Server A                                                   \
  21.256 +\            {|Crypt (shrK A) {|Agent B, Key (newK i), na, Nonce NB'|}, X|} \
  21.257 +\           : set_of_list evs;                                              \
  21.258 +\           Nonce NB : analz (insert (Key (newK i)) (sees lost Spy evs));   \
  21.259 +\           evs : yahalom lost |]                                           \
  21.260  \ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
  21.261  by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
  21.262  by (dtac Nonce_secrecy 1 THEN assume_tac 1);
    22.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Dec 19 11:54:19 1996 +0100
    22.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Dec 19 11:58:39 1996 +0100
    22.3 @@ -27,7 +27,8 @@
    22.4  
    22.5           (*Alice initiates a protocol run*)
    22.6      YM1  "[| evs: yahalom lost;  A ~= B |]
    22.7 -          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
    22.8 +          ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs
    22.9 +                : yahalom lost"
   22.10  
   22.11           (*Bob's response to Alice's message.  Bob doesn't know who 
   22.12  	   the sender is, hence the A' in the sender field.*)
   22.13 @@ -35,7 +36,8 @@
   22.14               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
   22.15            ==> Says B Server 
   22.16                    {|Agent B, 
   22.17 -                    Crypt (shrK B) {|Agent A, Nonce NA, Nonce (newN evs)|}|}
   22.18 +                    Crypt (shrK B)
   22.19 +                      {|Agent A, Nonce NA, Nonce (newN(length evs))|}|}
   22.20                   # evs : yahalom lost"
   22.21  
   22.22           (*The Server receives Bob's message.  He responds by sending a
   22.23 @@ -45,9 +47,9 @@
   22.24                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   22.25                 : set_of_list evs |]
   22.26            ==> Says Server A
   22.27 -                  {|Crypt (shrK A) {|Agent B, Key (newK evs), 
   22.28 +                  {|Crypt (shrK A) {|Agent B, Key (newK(length evs)), 
   22.29                              Nonce NA, Nonce NB|},
   22.30 -                    Crypt (shrK B) {|Agent A, Key (newK evs)|}|}
   22.31 +                    Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|}
   22.32                   # evs : yahalom lost"
   22.33  
   22.34           (*Alice receives the Server's (?) message, checks her Nonce, and
    23.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Dec 19 11:54:19 1996 +0100
    23.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Dec 19 11:58:39 1996 +0100
    23.3 @@ -126,9 +126,8 @@
    23.4  (*** Future keys can't be seen or used! ***)
    23.5  
    23.6  (*Nobody can have SEEN keys that will be generated in the future. *)
    23.7 -goal thy "!!evs. evs : yahalom lost ==> \
    23.8 -\                length evs <= length evs' --> \
    23.9 -\                Key (newK evs') ~: parts (sees lost Spy evs)";
   23.10 +goal thy "!!i. evs : yahalom lost ==> \
   23.11 +\              length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
   23.12  by (parts_induct_tac 1);
   23.13  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   23.14  				    addDs [impOfSubs analz_subset_parts,
   23.15 @@ -141,9 +140,9 @@
   23.16  (*Variant: old messages must contain old keys!*)
   23.17  goal thy 
   23.18   "!!evs. [| Says A B X : set_of_list evs;  \
   23.19 -\           Key (newK evt) : parts {X};    \
   23.20 +\           Key (newK i) : parts {X};    \
   23.21  \           evs : yahalom lost                 \
   23.22 -\        |] ==> length evt < length evs";
   23.23 +\        |] ==> i < length evs";
   23.24  by (rtac ccontr 1);
   23.25  by (dtac leI 1);
   23.26  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   23.27 @@ -153,9 +152,8 @@
   23.28  
   23.29  (*Nobody can have USED keys that will be generated in the future.
   23.30    ...very like new_keys_not_seen*)
   23.31 -goal thy "!!evs. evs : yahalom lost ==> \
   23.32 -\                length evs <= length evs' --> \
   23.33 -\                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   23.34 +goal thy "!!i. evs : yahalom lost ==> \
   23.35 +\             length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
   23.36  by (parts_induct_tac 1);
   23.37  by (dtac YM4_Key_parts_sees_Spy 5);
   23.38  (*YM1, YM2 and YM3*)
   23.39 @@ -189,7 +187,7 @@
   23.40   "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
   23.41  \            : set_of_list evs;                                         \
   23.42  \           evs : yahalom lost |]                                       \
   23.43 -\        ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
   23.44 +\        ==> (EX i. K = Key(newK i)) & A ~= B";
   23.45  by (etac rev_mp 1);
   23.46  by (etac yahalom.induct 1);
   23.47  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   23.48 @@ -201,13 +199,13 @@
   23.49      dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   23.50      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   23.51      assume_tac 7 THEN Full_simp_tac 7 THEN
   23.52 -    REPEAT ((eresolve_tac [bexE,conjE] ORELSE' hyp_subst_tac) 7);
   23.53 +    REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7);
   23.54  
   23.55  
   23.56  (****
   23.57   The following is to prove theorems of the form
   23.58  
   23.59 -          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   23.60 +          Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
   23.61            Key K : analz (sees lost Spy evs)
   23.62  
   23.63   A more general formula must be proved inductively.
   23.64 @@ -223,10 +221,10 @@
   23.65  by (etac yahalom.induct 1);
   23.66  by analz_Fake_tac;
   23.67  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   23.68 -by (ALLGOALS  (*Takes 26 secs*)
   23.69 +by (ALLGOALS (*Takes 11 secs*)
   23.70      (asm_simp_tac 
   23.71 -     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   23.72 -                         @ pushes)
   23.73 +     (!simpset addsimps [Un_assoc RS sym, 
   23.74 +			 insert_Key_singleton, insert_Key_image, pushKey_newK]
   23.75                 setloop split_tac [expand_if])));
   23.76  (*YM4, Fake*) 
   23.77  by (EVERY (map spy_analz_tac [4, 2]));
   23.78 @@ -236,8 +234,8 @@
   23.79  
   23.80  goal thy
   23.81   "!!evs. evs : yahalom lost ==>                               \
   23.82 -\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   23.83 -\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   23.84 +\        Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \
   23.85 +\        (K = newK i | Key K : analz (sees lost Spy evs))";
   23.86  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   23.87                                     insert_Key_singleton]) 1);
   23.88  by (Fast_tac 1);
   23.89 @@ -273,11 +271,7 @@
   23.90  \           : set_of_list evs;                                      \
   23.91  \          evs : yahalom lost |]                                    \
   23.92  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   23.93 -by (dtac lemma 1);
   23.94 -by (REPEAT (etac exE 1));
   23.95 -(*Duplicate the assumption*)
   23.96 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   23.97 -by (fast_tac (!claset addSDs [spec]) 1);
   23.98 +by (prove_unique_tac lemma 1);
   23.99  qed "unique_session_keys";
  23.100  
  23.101  
  23.102 @@ -296,8 +290,7 @@
  23.103  by analz_Fake_tac;
  23.104  by (ALLGOALS
  23.105      (asm_simp_tac 
  23.106 -     (!simpset addsimps ([not_parts_not_analz,
  23.107 -                          analz_insert_Key_newK] @ pushes)
  23.108 +     (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
  23.109                 setloop split_tac [expand_if])));
  23.110  (*YM3*)
  23.111  by (fast_tac (!claset addIs [parts_insertI]
    24.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Dec 19 11:54:19 1996 +0100
    24.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Dec 19 11:58:39 1996 +0100
    24.3 @@ -31,13 +31,13 @@
    24.4  
    24.5           (*Alice initiates a protocol run*)
    24.6      YM1  "[| evs: yahalom lost;  A ~= B |]
    24.7 -          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
    24.8 +          ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost"
    24.9  
   24.10           (*Bob's response to Alice's message.  Bob doesn't know who 
   24.11  	   the sender is, hence the A' in the sender field.*)
   24.12      YM2  "[| evs: yahalom lost;  B ~= Server;
   24.13               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
   24.14 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
   24.15 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|}
   24.16                   # evs : yahalom lost"
   24.17  
   24.18           (*The Server receives Bob's message.  He responds by sending a
   24.19 @@ -48,8 +48,8 @@
   24.20                 : set_of_list evs |]
   24.21            ==> Says Server A
   24.22                 {|Nonce NB, 
   24.23 -                 Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|},
   24.24 -                 Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|}
   24.25 +                 Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|},
   24.26 +                 Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|}
   24.27                   # evs : yahalom lost"
   24.28  
   24.29           (*Alice receives the Server's (?) message, checks her Nonce, and