Renaming and simplification
authorpaulson
Tue Sep 03 18:24:42 1996 +0200 (1996-09-03)
changeset 194320574dca5a3e
parent 1942 6c9c1a42a869
child 1944 ea0f573b222b
Renaming and simplification
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 03 17:54:39 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Sep 03 18:24:42 1996 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4  
     1.5  open NS_Shared;
     1.6  
     1.7 +proof_timing:=true;
     1.8 +
     1.9  (**** Inductive proofs about ns_shared ****)
    1.10  
    1.11  (*The Enemy can see more than anybody else, except for their initial state*)
    1.12 @@ -40,7 +42,7 @@
    1.13  AddSEs   [not_Notes RSN (2, rev_notE)];
    1.14  
    1.15  
    1.16 -(*For reasoning about message NS3*)
    1.17 +(*For reasoning about the encrypted portion of message NS3*)
    1.18  goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
    1.19  \                X : parts (sees Enemy evs)";
    1.20  by (fast_tac (!claset addSEs partsEs
    1.21 @@ -48,68 +50,68 @@
    1.22  qed "NS3_msg_in_parts_sees_Enemy";
    1.23  			      
    1.24  
    1.25 -(*** Server keys are not betrayed ***)
    1.26 +(*** Shared keys are not betrayed ***)
    1.27  
    1.28 -(*Enemy never sees another agent's server key!*)
    1.29 +(*Enemy never sees another agent's shared key!*)
    1.30  goal thy 
    1.31   "!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \
    1.32 -\        Key (serverKey A) ~: parts (sees Enemy evs)";
    1.33 +\        Key (shrK A) ~: parts (sees Enemy evs)";
    1.34  be ns_shared.induct 1;
    1.35  bd NS3_msg_in_parts_sees_Enemy 5;
    1.36  by (Auto_tac());
    1.37  (*Deals with Fake message*)
    1.38  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.39 -			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
    1.40 -qed "Enemy_not_see_serverKey";
    1.41 +			     impOfSubs Fake_parts_insert]) 1);
    1.42 +qed "Enemy_not_see_shrK";
    1.43  
    1.44 -bind_thm ("Enemy_not_analz_serverKey",
    1.45 -	  [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
    1.46 +bind_thm ("Enemy_not_analz_shrK",
    1.47 +	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    1.48  
    1.49 -Addsimps [Enemy_not_see_serverKey, 
    1.50 -	  not_sym RSN (2, Enemy_not_see_serverKey), 
    1.51 -	  Enemy_not_analz_serverKey, 
    1.52 -	  not_sym RSN (2, Enemy_not_analz_serverKey)];
    1.53 +Addsimps [Enemy_not_see_shrK, 
    1.54 +	  not_sym RSN (2, Enemy_not_see_shrK), 
    1.55 +	  Enemy_not_analz_shrK, 
    1.56 +	  not_sym RSN (2, Enemy_not_analz_shrK)];
    1.57  
    1.58  (*We go to some trouble to preserve R in the 3rd subgoal*)
    1.59  val major::prems = 
    1.60 -goal thy  "[| Key (serverKey A) : parts (sees Enemy evs);    \
    1.61 +goal thy  "[| Key (shrK A) : parts (sees Enemy evs);    \
    1.62  \             evs : ns_shared;                                  \
    1.63  \             A=Enemy ==> R                                  \
    1.64  \           |] ==> R";
    1.65  br ccontr 1;
    1.66 -br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1;
    1.67 +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
    1.68  by (swap_res_tac prems 2);
    1.69  by (ALLGOALS (fast_tac (!claset addIs prems)));
    1.70 -qed "Enemy_see_serverKey_E";
    1.71 +qed "Enemy_see_shrK_E";
    1.72  
    1.73 -bind_thm ("Enemy_analz_serverKey_E", 
    1.74 -	  analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
    1.75 +bind_thm ("Enemy_analz_shrK_E", 
    1.76 +	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
    1.77  
    1.78  (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
    1.79 -AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
    1.80 +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
    1.81  
    1.82  
    1.83 -(*No Friend will ever see another agent's server key 
    1.84 +(*No Friend will ever see another agent's shared key 
    1.85    (excluding the Enemy, who might transmit his).
    1.86 -  The Server, of course, knows all server keys.*)
    1.87 +  The Server, of course, knows all shared keys.*)
    1.88  goal thy 
    1.89   "!!evs. [| evs : ns_shared; A ~= Enemy;  A ~= Friend j |] ==> \
    1.90 -\        Key (serverKey A) ~: parts (sees (Friend j) evs)";
    1.91 +\        Key (shrK A) ~: parts (sees (Friend j) evs)";
    1.92  br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
    1.93  by (ALLGOALS Asm_simp_tac);
    1.94 -qed "Friend_not_see_serverKey";
    1.95 +qed "Friend_not_see_shrK";
    1.96  
    1.97  
    1.98  (*Not for Addsimps -- it can cause goals to blow up!*)
    1.99  goal thy  
   1.100   "!!evs. evs : ns_shared ==>                                  \
   1.101 -\        (Key (serverKey A) \
   1.102 -\           : analz (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   1.103 +\        (Key (shrK A) \
   1.104 +\           : analz (insert (Key (shrK B)) (sees Enemy evs))) =  \
   1.105  \        (A=B | A=Enemy)";
   1.106  by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.107  		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.108  	              addss (!simpset)) 1);
   1.109 -qed "serverKey_mem_analz";
   1.110 +qed "shrK_mem_analz";
   1.111  
   1.112  
   1.113  (*** Future keys can't be seen or used! ***)
   1.114 @@ -200,8 +202,8 @@
   1.115  \           evs : ns_shared    \
   1.116  \        |] ==> (EX evt:ns_shared. \
   1.117  \                         K = Key(newK evt) & \
   1.118 -\                         X = (Crypt {|K, Agent A|} (serverKey B)) & \
   1.119 -\                         K' = serverKey A & \
   1.120 +\                         X = (Crypt {|K, Agent A|} (shrK B)) & \
   1.121 +\                         K' = shrK A & \
   1.122  \                         length evt < length evs)";
   1.123  be rev_mp 1;
   1.124  be ns_shared.induct 1;
   1.125 @@ -209,14 +211,15 @@
   1.126  qed "Says_Server_message_form";
   1.127  
   1.128  
   1.129 -(*Describes the form of X when the following message is sent*)
   1.130 +(*Describes the form of X when the following message is sent.  The use of
   1.131 +  "parts" strengthens the induction hyp for proving the Fake case*)
   1.132  goal thy
   1.133   "!!evs. evs : ns_shared ==>                             \
   1.134  \        ALL A NA B K X.                            \
   1.135 -\            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.136 +\            (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.137  \            : parts (sees Enemy evs) & A ~= Enemy  -->   \
   1.138  \          (EX evt:ns_shared. K = newK evt & \
   1.139 -\                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.140 +\                             X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.141  be ns_shared.induct 1;
   1.142  bd NS3_msg_in_parts_sees_Enemy 5;
   1.143  by (Step_tac 1);
   1.144 @@ -225,7 +228,7 @@
   1.145  by (fast_tac (!claset addSDs [spec]) 2);
   1.146  (*Now for the Fake case*)
   1.147  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.148 -			     impOfSubs synth_analz_parts_insert_subset_Un]
   1.149 +			     impOfSubs Fake_parts_insert]
   1.150  	              addss (!simpset)) 1);
   1.151  qed_spec_mp "encrypted_form";
   1.152  
   1.153 @@ -234,7 +237,7 @@
   1.154  goal thy 
   1.155   "!!evs. evs : ns_shared ==>                             \
   1.156  \        ALL S A NA B K X.                            \
   1.157 -\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.158 +\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.159  \            : set_of_list evs  -->   \
   1.160  \        S = Server | S = Enemy";
   1.161  be ns_shared.induct 1;
   1.162 @@ -247,7 +250,7 @@
   1.163  bd Says_Server_message_form 1;
   1.164  by (ALLGOALS Full_simp_tac);
   1.165  (*Final case.  Clear out needless quantifiers to speed the following step*)
   1.166 -by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   1.167 +by (thin_tac "ALL x. ?P(x)" 1);
   1.168  bd encrypted_form 1;
   1.169  br (parts.Inj RS conjI) 1;
   1.170  auto();
   1.171 @@ -257,11 +260,11 @@
   1.172  (*Describes the form of X when the following message is sent;
   1.173    use Says_Server_message_form if applicable*)
   1.174  goal thy 
   1.175 - "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.176 -\            : set_of_list evs;                              \
   1.177 -\           evs : ns_shared               \
   1.178 -\        |] ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
   1.179 -\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.180 + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))    \
   1.181 +\            : set_of_list evs;                                          \
   1.182 +\           evs : ns_shared |]                                           \
   1.183 +\        ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
   1.184 +\                               X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.185  by (forward_tac [Server_or_Enemy] 1);
   1.186  ba 1;
   1.187  by (Step_tac 1);
   1.188 @@ -277,8 +280,8 @@
   1.189   The following is to prove theorems of the form
   1.190  
   1.191            Key K : analz (insert (Key (newK evt)) 
   1.192 -	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
   1.193 -          Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
   1.194 +	                   (insert (Key (shrK C)) (sees Enemy evs))) ==>
   1.195 +          Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
   1.196  
   1.197   A more general formula must be proved inductively.
   1.198  
   1.199 @@ -323,52 +326,56 @@
   1.200  
   1.201  (** Session keys are not used to encrypt other session keys **)
   1.202  
   1.203 +(*Lemma for the trivial direction of the if-and-only-if*)
   1.204 +goal thy  
   1.205 + "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \
   1.206 +\          (K : nE | Key K : analz (insert KsC sEe))  ==>     \
   1.207 +\        (Key K : analz (insert KsC (Key``nE Un sEe))) = \
   1.208 +\          (K : nE | Key K : analz (insert KsC sEe))";
   1.209 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   1.210 +val lemma = result();
   1.211 +
   1.212  goal thy  
   1.213   "!!evs. evs : ns_shared ==> \
   1.214 -\  ALL K E. (Key K : analz (insert (Key (serverKey C)) \
   1.215 +\  ALL K E. (Key K : analz (insert (Key (shrK C)) \
   1.216  \                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   1.217  \           (K : newK``E |  \
   1.218 -\            Key K : analz (insert (Key (serverKey C)) \
   1.219 +\            Key K : analz (insert (Key (shrK C)) \
   1.220  \                             (sees Enemy evs)))";
   1.221  be ns_shared.induct 1;
   1.222  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.223  by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
   1.224 +by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   1.225  by (ALLGOALS 
   1.226      (asm_simp_tac 
   1.227       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.228  			 @ pushes)
   1.229                 setloop split_tac [expand_if])));
   1.230 +(** LEVEL 5 **)
   1.231  (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   1.232  by (REPEAT (Fast_tac 3));
   1.233 +(*Fake case*) (** LEVEL 6 **)
   1.234 +by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   1.235 +    (insert_commute RS ssubst) 2);
   1.236 +(*This is enemy_analz_tac from OtwayRees.ML*)
   1.237 +by (EVERY [rtac impI 2,
   1.238 +	   dtac (impOfSubs Fake_analz_insert) 2,
   1.239 +	   eresolve_tac [asm_rl, synth.Inj] 2,
   1.240 +	   Fast_tac 2,
   1.241 +	   Asm_full_simp_tac 2,
   1.242 +	   deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 2]);
   1.243  (*Base case*)
   1.244  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.245 -(** LEVEL 7 **)
   1.246 -(*Fake case*)
   1.247 -by (REPEAT (Safe_step_tac 1));
   1.248 -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2);
   1.249 -by (subgoal_tac 
   1.250 -    "Key K : analz \
   1.251 -\             (synth \
   1.252 -\              (analz (insert (Key (serverKey C)) \
   1.253 -\                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.254 -(*First, justify this subgoal*)
   1.255 -(*Discard formulae for better speed*)
   1.256 -by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.257 -by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
   1.258 -by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.259 -                      addSEs [impOfSubs analz_mono]) 2);
   1.260 -by (Asm_full_simp_tac 1);
   1.261 -by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
   1.262  qed_spec_mp "analz_image_newK";
   1.263  
   1.264  
   1.265  goal thy
   1.266   "!!evs. evs : ns_shared ==>                               \
   1.267  \        Key K : analz (insert (Key (newK evt))            \
   1.268 -\                         (insert (Key (serverKey C))      \
   1.269 +\                         (insert (Key (shrK C))      \
   1.270  \                          (sees Enemy evs))) =            \
   1.271  \             (K = newK evt |                              \
   1.272 -\              Key K : analz (insert (Key (serverKey C))   \
   1.273 +\              Key K : analz (insert (Key (shrK C))   \
   1.274  \                               (sees Enemy evs)))";
   1.275  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.276  				   insert_Key_singleton]) 1);
   1.277 @@ -384,8 +391,7 @@
   1.278  \      EX X'. ALL C S A Y N B X.               \
   1.279  \         C ~= Enemy -->                       \
   1.280  \         Says S A Y : set_of_list evs -->     \
   1.281 -\         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
   1.282 -\       (X = X'))";
   1.283 +\         ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> X=X')";
   1.284  be ns_shared.induct 1;
   1.285  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.286  by (ALLGOALS 
   1.287 @@ -407,13 +413,13 @@
   1.288  ba 2;
   1.289  by (Step_tac 1);
   1.290  (** LEVEL 12 **)
   1.291 -by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
   1.292 +by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \
   1.293  \                  : parts (sees Enemy evsa)" 1);
   1.294 -by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.295 +by (thin_tac "ALL S.?P(S)" 2);
   1.296  by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.297  	              addDs [impOfSubs parts_insert_subset_Un]
   1.298                        addss (!simpset)) 2);
   1.299 -by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
   1.300 +by (thin_tac "?aa : parts {X}" 1);
   1.301  bd parts_singleton 1;
   1.302  by (Step_tac 1);
   1.303  bd seesD 1;
   1.304 @@ -426,10 +432,10 @@
   1.305  (*In messages of this form, the session key uniquely identifies the rest*)
   1.306  goal thy 
   1.307   "!!evs. [| Says S A          \
   1.308 -\             (Crypt {|N, Agent B, Key K, X|} (serverKey C))     \
   1.309 +\             (Crypt {|N, Agent B, Key K, X|} (shrK C))     \
   1.310  \                  : set_of_list evs; \
   1.311   \          Says S' A'                                         \
   1.312 -\             (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
   1.313 +\             (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
   1.314  \                  : set_of_list evs;                         \
   1.315  \           evs : ns_shared;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.316  bd lemma 1;
   1.317 @@ -447,9 +453,10 @@
   1.318  \            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
   1.319  \           evs : ns_shared;  Friend i ~= C;  Friend j ~= C              \
   1.320  \        |] ==>                                                       \
   1.321 -\     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
   1.322 +\     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
   1.323  be rev_mp 1;
   1.324  be ns_shared.induct 1;
   1.325 +(*TRY CHANGING NEXT CMD TO by (ALLGOALS Asm_simp_tac);*)
   1.326  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.327  (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.328  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.329 @@ -467,7 +474,7 @@
   1.330  br notI 1;
   1.331  by (subgoal_tac 
   1.332      "Key (newK evt) : \
   1.333 -\    analz (synth (analz (insert (Key (serverKey C)) \
   1.334 +\    analz (synth (analz (insert (Key (shrK C)) \
   1.335  \                                  (sees Enemy evsa))))" 1);
   1.336  be (impOfSubs analz_mono) 2;
   1.337  by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
   1.338 @@ -489,7 +496,7 @@
   1.339  by (REPEAT_FIRST assume_tac);
   1.340  by (ALLGOALS Full_simp_tac);
   1.341  by (Step_tac 1);
   1.342 -by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
   1.343 +by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1);
   1.344  qed "Enemy_not_see_encrypted_key";
   1.345  
   1.346  
     2.1 --- a/src/HOL/Auth/NS_Shared.thy	Tue Sep 03 17:54:39 1996 +0200
     2.2 +++ b/src/HOL/Auth/NS_Shared.thy	Tue Sep 03 18:24:42 1996 +0200
     2.3 @@ -22,46 +22,49 @@
     2.4             invent new nonces here, but he can also use NS1.  Common to
     2.5             all similar protocols.*)
     2.6      Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
     2.7 -          |] ==> (Says Enemy B X) # evs : ns_shared"
     2.8 +          |] ==> Says Enemy B X # evs : ns_shared"
     2.9  
    2.10           (*Alice initiates a protocol run*)
    2.11      NS1  "[| evs: ns_shared;  A ~= Server
    2.12 -          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    2.13 -                 # evs : ns_shared"
    2.14 +          |] ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
    2.15 +                 : ns_shared"
    2.16  
    2.17           (*Server's response to Alice's message.
    2.18             !! It may respond more than once to A's request !!
    2.19  	   Server doesn't know who the true sender is, hence the A' in
    2.20                 the sender field.*)
    2.21      NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;
    2.22 -             (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.23 -          |] ==> (Says Server A 
    2.24 +             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
    2.25 +          |] ==> Says Server A 
    2.26                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    2.27 -                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    2.28 -                   (serverKey A))) # evs : ns_shared"
    2.29 +                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    2.30 +                   (shrK A)) # evs : ns_shared"
    2.31  
    2.32            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    2.33              May assume WLOG that she is NOT the Enemy: the Fake rule
    2.34              covers this case.  Can inductively show A ~= Server*)
    2.35      NS3  "[| evs: ns_shared;  A ~= B;
    2.36 -             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.37 +             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    2.38                 : set_of_list evs;
    2.39               A = Friend i;
    2.40 -             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.41 -          |] ==> (Says A B X) # evs : ns_shared"
    2.42 +             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
    2.43 +          |] ==> Says A B X # evs : ns_shared"
    2.44  
    2.45           (*Bob's nonce exchange.  He does not know who the message came
    2.46             from, but responds to A because she is mentioned inside.*)
    2.47      NS4  "[| evs: ns_shared;  A ~= B;  
    2.48 -             (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
    2.49 -               : set_of_list evs
    2.50 -          |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : ns_shared"
    2.51 +             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs
    2.52 +          |] ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
    2.53  
    2.54 -         (*Alice responds with (Suc N), if she has seen the key before.*)
    2.55 +         (*Alice responds with the Nonce, if she has seen the key before.
    2.56 +           We do NOT use N-1 or similar as the Enemy cannot spoof such things.
    2.57 +           Allowing the Enemy to add or subtract 1 allows him to send ALL
    2.58 +               nonces.  Instead we distinguish the messages by sending the
    2.59 +               nonce twice.*)
    2.60      NS5  "[| evs: ns_shared;  A ~= B;  
    2.61 -             (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
    2.62 -             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.63 +             Says B' A (Crypt (Nonce N) K) : set_of_list evs;
    2.64 +             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    2.65                 : set_of_list evs
    2.66 -          |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : ns_shared"
    2.67 +          |] ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
    2.68  
    2.69  end
     3.1 --- a/src/HOL/Auth/Shared.ML	Tue Sep 03 17:54:39 1996 +0200
     3.2 +++ b/src/HOL/Auth/Shared.ML	Tue Sep 03 18:24:42 1996 +0200
     3.3 @@ -12,13 +12,6 @@
     3.4  
     3.5  Addsimps [parts_cut_eq];
     3.6  
     3.7 -proof_timing:=true;
     3.8 -
     3.9 -(*IN SET.ML*)
    3.10 -goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    3.11 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    3.12 -qed "mem_if";
    3.13 -
    3.14  (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    3.15  goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    3.16  by (fast_tac (!claset addEs [equalityE]) 1);
    3.17 @@ -34,37 +27,37 @@
    3.18    will not!*)
    3.19  Addsimps [o_def];
    3.20  
    3.21 -(*** Basic properties of serverKey and newK ***)
    3.22 +(*** Basic properties of shrK and newK ***)
    3.23  
    3.24 -(* invKey (serverKey A) = serverKey A *)
    3.25 -bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
    3.26 +(* invKey (shrK A) = shrK A *)
    3.27 +bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
    3.28  
    3.29  (* invKey (newK evs) = newK evs *)
    3.30  bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    3.31 -Addsimps [invKey_serverKey, invKey_newK];
    3.32 +Addsimps [invKey_shrK, invKey_newK];
    3.33  
    3.34  
    3.35  (*New keys and nonces are fresh*)
    3.36 -val serverKey_inject = inj_serverKey RS injD;
    3.37 +val shrK_inject = inj_shrK RS injD;
    3.38  val newN_inject = inj_newN RS injD
    3.39  and newK_inject = inj_newK RS injD;
    3.40 -AddSEs [serverKey_inject, newN_inject, newK_inject,
    3.41 +AddSEs [shrK_inject, newN_inject, newK_inject,
    3.42  	fresh_newK RS notE, fresh_newN RS notE];
    3.43 -Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    3.44 +Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    3.45  Addsimps [fresh_newN, fresh_newK];
    3.46  
    3.47  (** Rewrites should not refer to  initState(Friend i) 
    3.48      -- not in normal form! **)
    3.49  
    3.50 -goal thy "newK evs ~= serverKey B";
    3.51 -by (subgoal_tac "newK evs = serverKey B --> \
    3.52 +goal thy "newK evs ~= shrK B";
    3.53 +by (subgoal_tac "newK evs = shrK B --> \
    3.54  \                Key (newK evs) : parts (initState B)" 1);
    3.55  by (Fast_tac 1);
    3.56  by (agent.induct_tac "B" 1);
    3.57  by (auto_tac (!claset addIs [range_eqI], !simpset));
    3.58 -qed "newK_neq_serverKey";
    3.59 +qed "newK_neq_shrK";
    3.60  
    3.61 -Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
    3.62 +Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
    3.63  
    3.64  (*Good for talking about Server's initial state*)
    3.65  goal thy "!!H. H <= Key``E ==> parts H = H";
    3.66 @@ -96,25 +89,25 @@
    3.67  qed "keysFor_image_Key";
    3.68  Addsimps [keysFor_image_Key];
    3.69  
    3.70 -goal thy "serverKey A ~: newK``E";
    3.71 +goal thy "shrK A ~: newK``E";
    3.72  by (agent.induct_tac "A" 1);
    3.73  by (Auto_tac ());
    3.74 -qed "serverKey_notin_image_newK";
    3.75 -Addsimps [serverKey_notin_image_newK];
    3.76 +qed "shrK_notin_image_newK";
    3.77 +Addsimps [shrK_notin_image_newK];
    3.78  
    3.79  
    3.80 -(*Agents see their own serverKeys!*)
    3.81 -goal thy "Key (serverKey A) : analz (sees A evs)";
    3.82 +(*Agents see their own shrKs!*)
    3.83 +goal thy "Key (shrK A) : analz (sees A evs)";
    3.84  by (list.induct_tac "evs" 1);
    3.85  by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
    3.86  by (agent.induct_tac "A" 1);
    3.87  by (auto_tac (!claset addIs [range_eqI], !simpset));
    3.88 -qed "analz_own_serverKey";
    3.89 +qed "analz_own_shrK";
    3.90  
    3.91 -bind_thm ("parts_own_serverKey",
    3.92 -	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
    3.93 +bind_thm ("parts_own_shrK",
    3.94 +	  [analz_subset_parts, analz_own_shrK] MRS subsetD);
    3.95  
    3.96 -Addsimps [analz_own_serverKey, parts_own_serverKey];
    3.97 +Addsimps [analz_own_shrK, parts_own_shrK];
    3.98  
    3.99  
   3.100  
   3.101 @@ -143,6 +136,11 @@
   3.102  by (Fast_tac 1);
   3.103  qed "sees_Says_subset_insert";
   3.104  
   3.105 +goal thy "sees A (Notes A' X # evs) <= insert X (sees A evs)";
   3.106 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   3.107 +by (Fast_tac 1);
   3.108 +qed "sees_Notes_subset_insert";
   3.109 +
   3.110  goal thy "sees A evs <= sees A (Says A' B X # evs)";
   3.111  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   3.112  by (Fast_tac 1);
   3.113 @@ -166,7 +164,7 @@
   3.114  Addsimps [Says_imp_sees_Enemy];
   3.115  AddIs    [Says_imp_sees_Enemy];
   3.116  
   3.117 -goal thy "initState C <= Key `` range serverKey";
   3.118 +goal thy "initState C <= Key `` range shrK";
   3.119  by (agent.induct_tac "C" 1);
   3.120  by (Auto_tac ());
   3.121  qed "initState_subset";
   3.122 @@ -174,7 +172,7 @@
   3.123  goal thy "X : sees C evs --> \
   3.124  \          (EX A B. Says A B X : set_of_list evs) | \
   3.125  \          (EX A. Notes A X : set_of_list evs) | \
   3.126 -\          (EX A. X = Key (serverKey A))";
   3.127 +\          (EX A. X = Key (shrK A))";
   3.128  by (list.induct_tac "evs" 1);
   3.129  by (ALLGOALS Asm_simp_tac);
   3.130  by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
   3.131 @@ -211,6 +209,6 @@
   3.132  (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   3.133  val pushes = pushKeys@pushCrypts;
   3.134  
   3.135 -val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
   3.136 +val pushKey_newK = insComm "Key (newK ?evs)"  "Key (shrK ?C)";
   3.137  
   3.138  
     4.1 --- a/src/HOL/Auth/Shared.thy	Tue Sep 03 17:54:39 1996 +0200
     4.2 +++ b/src/HOL/Auth/Shared.thy	Tue Sep 03 18:24:42 1996 +0200
     4.3 @@ -6,24 +6,26 @@
     4.4  Theory of Shared Keys (common to all symmetric-key protocols)
     4.5  
     4.6  Server keys; initial states of agents; new nonces and keys; function "sees" 
     4.7 +
     4.8 +IS THE Notes constructor needed??
     4.9  *)
    4.10  
    4.11  Shared = Message + List + 
    4.12  
    4.13  consts
    4.14 -  serverKey    :: agent => key  (*symmetric keys*)
    4.15 +  shrK    :: agent => key  (*symmetric keys*)
    4.16  
    4.17  rules
    4.18 -  isSym_serverKey "isSymKey (serverKey A)"
    4.19 +  isSym_shrK "isSymKey (shrK A)"
    4.20  
    4.21  consts  (*Initial states of agents -- parameter of the construction*)
    4.22    initState :: agent => msg set
    4.23  
    4.24  primrec initState agent
    4.25          (*Server knows all keys; other agents know only their own*)
    4.26 -  initState_Server  "initState Server     = Key `` range serverKey"
    4.27 -  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    4.28 -  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    4.29 +  initState_Server  "initState Server     = Key `` range shrK"
    4.30 +  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    4.31 +  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
    4.32  
    4.33  datatype  (*Messages, and components of agent stores*)
    4.34    event = Says agent agent msg
    4.35 @@ -55,7 +57,7 @@
    4.36    newK :: "event list => key"
    4.37  
    4.38  rules
    4.39 -  inj_serverKey "inj serverKey"
    4.40 +  inj_shrK "inj shrK"
    4.41  
    4.42    inj_newN   "inj newN"
    4.43    fresh_newN "Nonce (newN evs) ~: parts (initState B)"