Added Msg 3; works up to Says_Server_imp_Key_newK
authorpaulson
Thu Jul 11 15:30:22 1996 +0200 (1996-07-11)
changeset 1852289ce6cb5c84
parent 1851 7b1e1c298e50
child 1853 c18ccd5631e0
Added Msg 3; works up to Says_Server_imp_Key_newK
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Event.ML	Thu Jul 11 15:28:10 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Thu Jul 11 15:30:22 1996 +0200
     1.3 @@ -5,31 +5,39 @@
     1.4  
     1.5  Datatype of events;
     1.6  inductive relation "traces" for Needham-Schroeder (shared keys)
     1.7 +
     1.8 +Rewrites should not refer to	 initState (Friend i)    -- not in normal form
     1.9  *)
    1.10  
    1.11  
    1.12  open Event;
    1.13  
    1.14 +(*Rewrite using   {a} Un A = insert a A *)
    1.15 +Addsimps [insert_is_Un RS sym];
    1.16 +
    1.17 +
    1.18 +(*** Basic properties of serverKey and newK ***)
    1.19 +
    1.20  (* invKey (serverKey A) = serverKey A *)
    1.21  bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
    1.22  
    1.23 -(* invKey (newK(A,evs)) = newK(A,evs) *)
    1.24 +(* invKey (newK evs) = newK evs *)
    1.25  bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    1.26  Addsimps [invKey_serverKey, invKey_newK];
    1.27  
    1.28  
    1.29  (*New keys and nonces are fresh*)
    1.30  val serverKey_inject = inj_serverKey RS injD;
    1.31 -val newN_inject = inj_newN RS injD RS Pair_inject
    1.32 -and newK_inject = inj_newK RS injD RS Pair_inject;
    1.33 +val newN_inject = inj_newN RS injD
    1.34 +and newK_inject = inj_newK RS injD;
    1.35  AddSEs [serverKey_inject, newN_inject, newK_inject,
    1.36  	fresh_newK RS notE, fresh_newN RS notE];
    1.37  Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    1.38  Addsimps [fresh_newN, fresh_newK];
    1.39  
    1.40 -goal thy "newK (A,evs) ~= serverKey B";
    1.41 -by (subgoal_tac "newK (A,evs) = serverKey B --> \
    1.42 -\                Key (newK(A,evs)) : parts (initState B)" 1);
    1.43 +goal thy "newK evs ~= serverKey B";
    1.44 +by (subgoal_tac "newK evs = serverKey B --> \
    1.45 +\                Key (newK evs) : parts (initState B)" 1);
    1.46  by (Fast_tac 1);
    1.47  by (agent.induct_tac "B" 1);
    1.48  by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.49 @@ -79,7 +87,6 @@
    1.50  
    1.51  goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
    1.52  by (Simp_tac 1);
    1.53 -by (Fast_tac 1);
    1.54  qed "sees_own";
    1.55  
    1.56  goal thy "!!A. Server ~= A ==> \
    1.57 @@ -94,13 +101,17 @@
    1.58  
    1.59  goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
    1.60  by (Simp_tac 1);
    1.61 -by (Fast_tac 1);
    1.62  qed "sees_Enemy";
    1.63  
    1.64  goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
    1.65  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.66  by (Fast_tac 1);
    1.67 -qed "sees_subset";
    1.68 +qed "sees_Says_subset_insert";
    1.69 +
    1.70 +goal thy "sees A evs <= sees A (Says A' B X # evs)";
    1.71 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.72 +by (Fast_tac 1);
    1.73 +qed "sees_subset_sees_Says";
    1.74  
    1.75  (*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
    1.76  goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
    1.77 @@ -114,7 +125,7 @@
    1.78  
    1.79  
    1.80  Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
    1.81 -Delsimps [sees_Cons];
    1.82 +Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
    1.83  
    1.84  
    1.85  (**** Inductive proofs about traces ****)
    1.86 @@ -124,47 +135,50 @@
    1.87   "!!evs. evs : traces ==> \
    1.88  \     sees A evs <= initState A Un sees Enemy evs";
    1.89  be traces.induct 1;
    1.90 -be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
    1.91 -by (ALLGOALS (fast_tac (!claset addDs [sees_subset RS subsetD] 
    1.92 +be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
    1.93 +be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
    1.94 +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.95  			        addss (!simpset))));
    1.96  qed "sees_agent_subset_sees_Enemy";
    1.97  
    1.98  
    1.99 +goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs";
   1.100 +be traces.induct 1;
   1.101 +by (Auto_tac());
   1.102 +qed_spec_mp "not_Says_to_self";
   1.103 +Addsimps [not_Says_to_self];
   1.104 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   1.105 +
   1.106 +
   1.107  (*** Server keys are not betrayed ***)
   1.108  
   1.109 -(*No Enemy will ever see a Friend's server key
   1.110 -   -- even if another friend's key is compromised.
   1.111 -  The UN is essential to handle the Fake rule in the induction.*)
   1.112 +(*Enemy never sees another agent's server key!*)
   1.113  goal thy 
   1.114 - "!!evs. [| evs : traces;  i~=j |] ==> \
   1.115 -\        Key (serverKey (Friend i)) ~: \
   1.116 -\        parts (initState (Friend j) Un sees Enemy evs)";
   1.117 + "!!evs. [| evs : traces; A ~= Enemy |] ==> \
   1.118 +\        Key (serverKey A) ~: parts (sees Enemy evs)";
   1.119  be traces.induct 1;
   1.120 -be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.121 -by (Auto_tac());
   1.122 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.123 +by (auto_tac(!claset, !simpset addsimps [parts_insert2]));
   1.124  (*Deals with Faked messages*)
   1.125 -by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
   1.126 -			     imp_of_subset parts_insert_subset_Un]
   1.127 +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
   1.128 +			     impOfSubs parts_insert_subset_Un]
   1.129  	              addss (!simpset)) 1);
   1.130  qed "Enemy_not_see_serverKey";
   1.131  
   1.132 -(*No Friend will ever see another Friend's server key.*)
   1.133 -goal thy 
   1.134 - "!!evs. [| evs : traces;  i~=j |] ==> \
   1.135 -\        Key (serverKey (Friend i)) ~: parts (sees (Friend j) evs)";
   1.136 -br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   1.137 -by (REPEAT (ares_tac [Enemy_not_see_serverKey] 1));
   1.138 -qed "Friend_not_see_serverKey";
   1.139 +bind_thm ("Enemy_not_analyze_serverKey",
   1.140 +	  [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
   1.141 +
   1.142 +Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey];
   1.143 +
   1.144  
   1.145 -(*Variant needed for the theorem below*)
   1.146 +(*No Friend will ever see another agent's server key 
   1.147 +  (excluding the Enemy, who might transmit his).*)
   1.148  goal thy 
   1.149 - "!!evs. evs : traces ==> \
   1.150 -\        Key (serverKey (Friend i)) ~: analyze (sees Enemy evs)";
   1.151 -bd Enemy_not_see_serverKey 1;
   1.152 -br n_not_Suc_n 1;
   1.153 -by (Full_simp_tac 1);
   1.154 -by (fast_tac (!claset addDs [imp_of_subset analyze_subset_parts]) 1);
   1.155 -qed "serverKeys_not_analyzed";
   1.156 + "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.157 +\        Key (serverKey A) ~: parts (sees (Friend j) evs)";
   1.158 +br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   1.159 +by (ALLGOALS Asm_simp_tac);
   1.160 +qed "Friend_not_see_serverKey";
   1.161  
   1.162  
   1.163  (*** Future keys can't be seen or used! ***)
   1.164 @@ -177,9 +191,9 @@
   1.165    induction! *)
   1.166  goal thy "!!evs. evs : traces ==> \
   1.167  \                length evs <= length evs' --> \
   1.168 -\                          Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
   1.169 +\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.170  be traces.induct 1;
   1.171 -be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.172 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.173  by (ALLGOALS (asm_full_simp_tac
   1.174  	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
   1.175  (*Initial state?  New keys cannot clash*)
   1.176 @@ -188,9 +202,11 @@
   1.177  by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.178  (*Rule NS2 in protocol*)
   1.179  by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
   1.180 +(*Rule NS3 in protocol*)
   1.181 +by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
   1.182  (*Rule Fake: where an Enemy agent can say practically anything*)
   1.183 -by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
   1.184 -			     imp_of_subset parts_insert_subset_Un,
   1.185 +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
   1.186 +			     impOfSubs parts_insert_subset_Un,
   1.187  			     less_imp_le]
   1.188  	              addss (!simpset)) 1);
   1.189  val lemma = result();
   1.190 @@ -198,22 +214,25 @@
   1.191  (*Variant needed for the main theorem below*)
   1.192  goal thy 
   1.193   "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
   1.194 -\        Key (newK (A,evs')) ~: parts (sees C evs)";
   1.195 +\        Key (newK evs') ~: parts (sees C evs)";
   1.196  by (fast_tac (!claset addDs [lemma]) 1);
   1.197  qed "new_keys_not_seen";
   1.198  
   1.199 -goal thy "!!K. newK(A,evs) = invKey K ==> newK(A,evs) = K";
   1.200 +goal thy "!!K. newK evs = invKey K ==> newK evs = K";
   1.201  br (invKey_eq RS iffD1) 1;
   1.202  by (Simp_tac 1);
   1.203  val newK_invKey = result();
   1.204  
   1.205 +
   1.206 +val keysFor_parts_mono = parts_mono RS keysFor_mono;
   1.207 +
   1.208  (*Nobody can have USED keys that will be generated in the future.
   1.209    ...very like new_keys_not_seen*)
   1.210  goal thy "!!evs. evs : traces ==> \
   1.211  \                length evs <= length evs' --> \
   1.212 -\                newK (A,evs') ~: keysFor (UN C. parts (sees C evs))";
   1.213 +\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.214  be traces.induct 1;
   1.215 -be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.216 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.217  by (ALLGOALS (asm_full_simp_tac
   1.218  	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
   1.219  (*Rule NS1 in protocol*)
   1.220 @@ -223,24 +242,52 @@
   1.221  (*Rule Fake: where an Enemy agent can say practically anything*)
   1.222  by (best_tac 
   1.223      (!claset addSDs [newK_invKey]
   1.224 -	     addDs [imp_of_subset (analyze_subset_parts RS keysFor_mono),
   1.225 -		    imp_of_subset (parts_insert_subset_Un RS keysFor_mono),
   1.226 +	     addDs [impOfSubs (analyze_subset_parts RS keysFor_mono),
   1.227 +		    impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.228  		    less_imp_le]
   1.229               addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
   1.230  	     addss (!simpset)) 1);
   1.231 +(*Rule NS3: quite messy...*)
   1.232 +by (hyp_subst_tac 1);
   1.233 +by (full_simp_tac (!simpset addcongs [conj_cong]) 1);
   1.234 +br impI 1;
   1.235 +bd mp 1;
   1.236 +by (fast_tac (!claset addDs [less_imp_le]) 1);
   1.237 +by (best_tac (!claset addIs 
   1.238 +	      [impOfSubs (sees_subset_sees_Says RS keysFor_parts_mono),
   1.239 +	       impOfSubs (sees_own RS equalityD2 RS keysFor_parts_mono),
   1.240 +	       impOfSubs (empty_subsetI RS insert_mono RS keysFor_parts_mono)]
   1.241 +              addss (!simpset)) 1);
   1.242  val lemma = result();
   1.243  
   1.244  goal thy 
   1.245   "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
   1.246 -\        newK (A,evs') ~: keysFor (parts (sees C evs))";
   1.247 +\        newK evs' ~: keysFor (parts (sees C evs))";
   1.248  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.249  qed "new_keys_not_used";
   1.250 +Addsimps [new_keys_not_used];
   1.251  
   1.252 -bind_thm ("new_keys_not_used_analyze",
   1.253 +bind_thm ("new_keys_not_analyzed",
   1.254  	  [analyze_subset_parts RS keysFor_mono,
   1.255  	   new_keys_not_used] MRS contra_subsetD);
   1.256  
   1.257  
   1.258 +(*Maybe too specific to be of much use...*)
   1.259 +goal thy 
   1.260 + "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \
   1.261 +\                                (serverKey A))                  \
   1.262 +\               : setOfList evs;                                 \
   1.263 +\           evs : traces    \
   1.264 +\        |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
   1.265 +be rev_mp 1;
   1.266 +be traces.induct 1;
   1.267 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.268 +be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
   1.269 +by (ALLGOALS Asm_full_simp_tac);
   1.270 +by (Fast_tac 1);	(*Proves the NS2 case*)
   1.271 +qed "Says_Server_imp_X_eq_Crypt";
   1.272 +
   1.273 +
   1.274  (*Pushes Crypt events in so that others might be pulled out*)
   1.275  goal thy "insert (Crypt X K) (insert y evs) = \
   1.276  \         insert y (insert (Crypt X K) evs)";
   1.277 @@ -252,157 +299,336 @@
   1.278  by (Fast_tac 1);
   1.279  qed "insert_Key_delay";
   1.280  
   1.281 +
   1.282  (** Lemmas concerning the form of items passed in messages **)
   1.283  
   1.284  (*Describes the form *and age* of K when the following message is sent*)
   1.285  goal thy 
   1.286 - "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
   1.287 + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \
   1.288  \               : setOfList evs;  \
   1.289  \           evs : traces          \
   1.290 -\        |] ==> (EX evs'. K = Key (newK(Server,evs')) & \
   1.291 -\                         length evs' < length evs)";
   1.292 +\        |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)";
   1.293  be rev_mp 1;
   1.294  be traces.induct 1;
   1.295 -be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.296 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.297  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.298  qed "Says_Server_imp_Key_newK";
   1.299  
   1.300 -Addsimps [serverKeys_not_analyzed, 
   1.301 -	  new_keys_not_seen RS not_parts_not_analyze,
   1.302 -	  new_keys_not_used_analyze];
   1.303 +(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
   1.304 +bind_thm ("not_parts_not_keysFor_analyze", 
   1.305 +	  analyze_subset_parts RS keysFor_mono RS contra_subsetD);
   1.306 +
   1.307 +
   1.308 +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.309  
   1.310 +ZZZZZZZZZZZZZZZZ;
   1.311 +
   1.312 +
   1.313 +(*Fake case below may need something like this...*)
   1.314 +goal thy 
   1.315 + "!!evs. evs : traces ==>                             \
   1.316 +\        ALL B X. Crypt X (serverKey B) : analyze (sees Enemy evs)  -->   \
   1.317 +\        (EX A A'. Says A A' (Crypt X (serverKey B)) : setOfList evs";
   1.318  
   1.319  goal thy 
   1.320 - "!!evs. evs : traces ==> \
   1.321 -\     Says Server (Friend i) \
   1.322 -\          (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs  \
   1.323 -\     --> K ~: analyze (sees Enemy evs)";
   1.324 + "!!evs. evs : traces ==>                             \
   1.325 +\        ALL NA B K X. Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B) :
   1.326 +                       analyze (sees Enemy evs)  -->   \
   1.327 +\        (EX A A'. Says A A' (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B)) : setOfList evs";
   1.328 +
   1.329 +
   1.330 +
   1.331 +(*Describes the form of X when the following message is sent*)
   1.332 +goal thy 
   1.333 + "!!evs. evs : traces ==>                             \
   1.334 +\        ALL S A NA B K X.                            \
   1.335 +\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.336 +\            : setOfList evs  -->   \
   1.337 +\        (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
   1.338  be traces.induct 1;
   1.339 -be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
   1.340 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.341 +by (Step_tac 1);
   1.342 +by (ALLGOALS Asm_full_simp_tac);
   1.343 +(*Remaining cases are Fake, NS2 and NS3*)
   1.344 +by (Fast_tac 2);	(*Solves the NS2 case*)
   1.345 +(*The NS3 case needs the induction hypothesis twice!
   1.346 +    One application is to the X component of the most recent message.*)
   1.347 +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.348 +be conjE 2;
   1.349 +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent (Friend i)|} (serverKey B)" 2);
   1.350 +by (eres_inst_tac [("V","?P|?Q")] thin_rl 3);	(*speeds the following step*)
   1.351 +by (Fast_tac 3);
   1.352 +(*DELETE the first quantified formula: it's now useless*)
   1.353 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.354 +by (fast_tac (!claset addss (!simpset)) 2);
   1.355 +(*Now for the Fake case*)
   1.356 +be disjE 1;
   1.357 +(*The subcase of Fake, where the message in question is NOT the most recent*)
   1.358 +by (Best_tac 2);
   1.359 +(*The subcase of Fake proved because server keys are kept secret*)
   1.360 +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.361 +be Crypt_synthesize 1;
   1.362 +be Key_synthesize 2;
   1.363 +by (Asm_full_simp_tac 2);
   1.364 +
   1.365 +
   1.366 +
   1.367 + 1. !!evs B X evsa S A NA Ba K Xa.
   1.368 +       [| evsa : traces;
   1.369 +          ! S A NA B K X.
   1.370 +             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) :
   1.371 +             setOfList evsa -->
   1.372 +             (? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B));
   1.373 +          B ~= Enemy;
   1.374 +          Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey B) :
   1.375 +          analyze (sees Enemy evsa) |] ==>
   1.376 +       ? evs'. Xa = Crypt {|Key (newK evs'), Agent B|} (serverKey Ba)
   1.377 +
   1.378 +
   1.379 +(*Split up the possibilities of that message being synthesized...*)
   1.380 +by (Step_tac 1);
   1.381 +by (Best_tac 6);
   1.382 +
   1.383 +
   1.384 +
   1.385 +
   1.386 +by (Safe_step_tac 1);
   1.387 +by (Safe_step_tac 2);
   1.388  by (ALLGOALS Asm_full_simp_tac);
   1.389 -(*We infer that K has the form "Key (newK(Server,evs')" ... *)
   1.390 +by (REPEAT_FIRST (etac disjE));
   1.391 +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.392 +
   1.393 +
   1.394 +by (hyp_subst_tac 5);
   1.395 +
   1.396 +
   1.397 +
   1.398 +
   1.399 +
   1.400 +by (REPEAT (dtac spec 3));
   1.401 +fe conjE;
   1.402 +fe mp ;
   1.403 +by (REPEAT (resolve_tac [refl, conjI] 3));
   1.404 +by (REPEAT_FIRST (etac conjE));
   1.405 +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.406 +
   1.407 +
   1.408 +by (subgoal_tac "? evs'. Xa = Crypt {|Key (newK evs'), Agent Aa|} (serverKey Ba)" 2);
   1.409 +by (Fast_tac 3);
   1.410 +
   1.411 +
   1.412 +
   1.413 +be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
   1.414 +
   1.415 +
   1.416 +auto();
   1.417 +by (ALLGOALS
   1.418 +    (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,de_Morgan_conj])));
   1.419 +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.420 +
   1.421 +by (REPEAT (Safe_step_tac 1));
   1.422 +
   1.423 +qed "Says_Crypt_Nonce_imp_msg_Crypt";
   1.424 +
   1.425 +goal thy 
   1.426 + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.427 +\               : setOfList evs;  \
   1.428 +\           evs : traces                             \
   1.429 +\        |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
   1.430 +
   1.431 +
   1.432 +YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   1.433 +
   1.434 +
   1.435 +WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
   1.436 +
   1.437 +(*If a message is sent, encrypted with a Friend's server key, then either
   1.438 +  that Friend or the Server originally sent it.*)
   1.439 +goal thy 
   1.440 + "!!evs. evs : traces ==>                             \
   1.441 +\    ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
   1.442 +\        : setOfList evs  -->   \
   1.443 +\    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \
   1.444 +\            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)";
   1.445 +be traces.induct 1;
   1.446 +be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.447 +by (Step_tac 1);
   1.448 +by (ALLGOALS Asm_full_simp_tac);
   1.449 +(*Remaining cases are Fake, NS2 and NS3*)
   1.450 +by (Fast_tac 2);	(*Proves the NS2 case*)
   1.451 +
   1.452 +by (REPEAT (dtac spec 2));
   1.453 +fe conjE;
   1.454 +bd mp 2;
   1.455 +
   1.456 +by (REPEAT (resolve_tac [refl, conjI] 2));
   1.457 +by (ALLGOALS Asm_full_simp_tac);
   1.458 +
   1.459 +
   1.460 +
   1.461 +
   1.462 +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.463 +be conjE 2;
   1.464 +by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
   1.465 +
   1.466 +(*The NS3 case needs the induction hypothesis twice!
   1.467 +    One application is to the X component of the most recent message.*)
   1.468 +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
   1.469 +by (Fast_tac 3);
   1.470 +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.471 +be conjE 2;
   1.472 +(*DELETE the first quantified formula: it's now useless*)
   1.473 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.474 +by (fast_tac (!claset addss (!simpset)) 2);
   1.475 +(*Now for the Fake case*)
   1.476 +be disjE 1;
   1.477 +(*The subcase of Fake, where the message in question is NOT the most recent*)
   1.478 +by (Best_tac 2);
   1.479 +
   1.480 +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.481 +be Crypt_synthesize 1;
   1.482 +be Key_synthesize 2;
   1.483 +
   1.484 +(*Split up the possibilities of that message being synthesized...*)
   1.485 +by (Step_tac 1);
   1.486 +by (Best_tac 6);
   1.487 +
   1.488 +
   1.489 +
   1.490 +
   1.491 +
   1.492 + (*The NS3 case needs the induction hypothesis twice!
   1.493 +    One application is to the X component of the most recent message.*)
   1.494 +
   1.495 +????????????????????????????????????????????????????????????????
   1.496 +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 1);
   1.497 +by (Fast_tac 2);
   1.498 +
   1.499 +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.500 +
   1.501 +be conjE 1;
   1.502 +(*DELETE the first quantified formula: it's now useless*)
   1.503 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 1);
   1.504 +by (fast_tac (!claset addss (!simpset)) 1);
   1.505 +
   1.506 +
   1.507 +(*Now for the Fake case*)
   1.508 +be disjE 1;
   1.509 +(*The subcase of Fake, where the message in question is NOT the most recent*)
   1.510 +by (Best_tac 2);
   1.511 +
   1.512 +WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
   1.513 +
   1.514 +
   1.515 +Addsimps [new_keys_not_seen];
   1.516 +
   1.517 +(*Crucial security property: Enemy does not see the keys sent in msg NS2
   1.518 +   -- even if another friend's key is compromised*)
   1.519 +goal thy 
   1.520 + "!!evs. [| Says Server (Friend i) \
   1.521 +\          (Crypt {|N, Agent B, K, X|} K') : setOfList evs;  \
   1.522 +\          evs : traces;  i~=j |] ==> \
   1.523 +\       \
   1.524 +\     K ~: analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
   1.525 +be rev_mp 1;
   1.526 +be traces.induct 1;
   1.527 +be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.528 +by (ALLGOALS Asm_full_simp_tac);
   1.529 +(*The two simplifications cannot be combined -- they loop!*)
   1.530 +by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
   1.531 +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.532  br conjI 3;
   1.533  by (REPEAT_FIRST (resolve_tac [impI]));
   1.534  by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
   1.535  (*NS1, subgoal concerns "(Says A Server
   1.536 -                          {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
   1.537 +                          {|Agent A, Agent B, Nonce (newN evsa)|}"*)
   1.538  (*... thus it cannot equal any components of A's message above.*)
   1.539  by (fast_tac (!claset addss (!simpset)) 2);
   1.540  (*NS2, the subcase where that message was the most recently sent;
   1.541 -  it holds because here K' = serverKey(Friend i), which Enemies can't see*)
   1.542 -by (fast_tac (!claset addss (!simpset)) 2);
   1.543 -(*NS2, other subcase!*)
   1.544 +  it holds because here K' = serverKey(Friend i), which Enemies can't see,
   1.545 +  AND because nobody can know about a brand new key*)
   1.546 +by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2);
   1.547 +(*NS2, other subcase.  K is an old key, and thus not in the latest message.*)
   1.548  by (fast_tac 
   1.549      (!claset addSEs [less_irrefl]
   1.550 -             addDs [imp_of_subset analyze_insert_Crypt_subset]
   1.551 -	     addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
   1.552 +             addDs [impOfSubs analyze_insert_Crypt_subset]
   1.553 +	     addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2);
   1.554  (*Now for the Fake case*)
   1.555  be exE 1;
   1.556  br notI 1;
   1.557  by (REPEAT (etac conjE 1));
   1.558  by (REPEAT (hyp_subst_tac 1));
   1.559 -by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
   1.560 -be (imp_of_subset analyze_mono) 2;
   1.561 +by (subgoal_tac 
   1.562 +    "Key (newK evs') : \
   1.563 +\    analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \
   1.564 +\                                  (sees Enemy evsa))))" 1);
   1.565 +be (impOfSubs analyze_mono) 2;
   1.566  by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
   1.567  			     (2,rev_subsetD),
   1.568 -			     imp_of_subset synthesize_increasing,
   1.569 -			     imp_of_subset analyze_increasing]) 2);
   1.570 +			     impOfSubs synthesize_increasing,
   1.571 +			     impOfSubs analyze_increasing]) 2);
   1.572  (*Proves the Fake goal*)
   1.573  by (Auto_tac());
   1.574 -qed "encrypted_key_not_seen";
   1.575 +qed "Enemy_not_see_encrypted_key";
   1.576 +
   1.577 +
   1.578 +goal thy 
   1.579 + "!!evs. [| Says Server (Friend i) \
   1.580 +\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
   1.581 +\           evs : traces;  i~=j    \
   1.582 +\         |] ==> K ~: analyze (sees (Friend j) evs)";
   1.583 +br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
   1.584 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
   1.585 +qed "Friend_not_see_encrypted_key";
   1.586 +
   1.587 +goal thy 
   1.588 + "!!evs. [| Says Server (Friend i) \
   1.589 +\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
   1.590 +\           A ~: {Friend i, Server};  \
   1.591 +\           evs : traces    \
   1.592 +\        |] ==>  K ~: analyze (sees A evs)";
   1.593 +by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
   1.594 +by (agent.induct_tac "A" 1);
   1.595 +by (ALLGOALS Simp_tac);
   1.596 +by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
   1.597 +				     Friend_not_see_encrypted_key]) 1);
   1.598 +br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
   1.599 +(*  hyp_subst_tac would deletes the equality assumption... *)
   1.600 +by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
   1.601 +qed "Agent_not_see_encrypted_key";
   1.602 +
   1.603 +
   1.604 +(*Neatly packaged, perhaps in a useless form*)
   1.605 +goalw thy [knownBy_def]
   1.606 + "!!evs. [| Says Server (Friend i) \
   1.607 +\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
   1.608 +\           evs : traces    \
   1.609 +\        |] ==>  knownBy evs K <= {Friend i, Server}";
   1.610 +
   1.611 +by (Step_tac 1);
   1.612 +br ccontr 1;
   1.613 +by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
   1.614 +qed "knownBy_encrypted_key";
   1.615 +
   1.616  
   1.617  
   1.618  
   1.619  XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.620  
   1.621 -(*Nobody can have SEEN keys that will be generated in the future.
   1.622 -  This has to be proved anew for each protocol description,
   1.623 -  but should go by similar reasoning every time.  Hardest case is the
   1.624 -  standard Fake rule.  
   1.625 -      The length comparison, and Union over C, are essential for the 
   1.626 -  induction! *)
   1.627 -goal thy "!!evs. evs : traces ==> \
   1.628 -\                length evs <= length evs' --> \
   1.629 -\                          Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
   1.630 -be traces.induct 1;
   1.631 -be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.632 -by (ALLGOALS (asm_full_simp_tac
   1.633 -	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
   1.634 -(*Initial state?  New keys cannot clash*)
   1.635 -by (Fast_tac 1);
   1.636 -(*Rule NS1 in protocol*)
   1.637 -by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.638 -(*Rule NS2 in protocol*)
   1.639 -by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
   1.640 -(*Rule Fake: where an Enemy agent can say practically anything*)
   1.641 -by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
   1.642 -			     imp_of_subset parts_insert_subset_Un,
   1.643 -			     less_imp_le]
   1.644 -	              addss (!simpset)) 1);
   1.645 -val lemma = result();
   1.646 +
   1.647  
   1.648  
   1.649  
   1.650  goal thy 
   1.651 - "!!evs. [| evs : traces;  i~=j |] ==> \
   1.652 -\     Says Server (Friend i) \
   1.653 -\          (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs  \
   1.654 -\     --> K ~: analyze (initState (Friend j) Un sees Enemy evs)";
   1.655 + "!!evs. evs : traces ==> \
   1.656 +\     Says Server A \
   1.657 +\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
   1.658 +\     --> (EX evs'. N = Nonce (newN evs'))";
   1.659  be traces.induct 1;
   1.660 -be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
   1.661 -by (ALLGOALS Asm_full_simp_tac);
   1.662 -(*We infer that K has the form "Key (newK(Server,evs')" ... *)
   1.663 -br conjI 3;
   1.664 -by (REPEAT_FIRST (resolve_tac [impI]));
   1.665 -by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
   1.666 -(*NS1, subgoal concerns "(Says A Server
   1.667 -                          {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
   1.668 -(*... thus it cannot equal any components of A's message above.*)
   1.669 -
   1.670 -by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
   1.671 -
   1.672 -by (fast_tac (!claset addss (!simpset)) 2);
   1.673 -(*NS2, the subcase where that message was the most recently sent;
   1.674 -  it holds because here K' = serverKey(Friend i), which Enemies can't see*)
   1.675 -by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
   1.676 -by (Safe_step_tac 2);
   1.677 -
   1.678 -by (stac analyze_insert_Crypt 2);
   1.679 -
   1.680 -by (fast_tac (!claset addss (!simpset)) 2);
   1.681 -(*NS2, other subcase!*)
   1.682 +by (ALLGOALS Asm_simp_tac);
   1.683 +by (Fast_tac 1);
   1.684 +val Says_Server_lemma = result();
   1.685  
   1.686 -by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
   1.687 -by (fast_tac 
   1.688 -    (!claset addSEs [less_irrefl]
   1.689 -             addDs [imp_of_subset analyze_insert_Crypt_subset]
   1.690 -	     addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
   1.691 -(*Now for the Fake case*)
   1.692 -be exE 1;
   1.693 -br notI 1;
   1.694 -by (REPEAT (etac conjE 1));
   1.695 -by (REPEAT (hyp_subst_tac 1));
   1.696 -by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
   1.697 -be (imp_of_subset analyze_mono) 2;
   1.698 -by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
   1.699 -			     (2,rev_subsetD),
   1.700 -			     imp_of_subset synthesize_increasing,
   1.701 -			     imp_of_subset analyze_increasing]) 2);
   1.702 -(*Proves the Fake goal*)
   1.703 -by (Auto_tac());
   1.704 -qed "encrypted_key_not_seen";
   1.705 -
   1.706 -
   1.707 -
   1.708 -
   1.709 -(*Bet this requires the premise   A = Friend i *)
   1.710 -goal thy "[| evs : traces;  \
   1.711 -\            (Says Server A (Crypt {|Agent A, Agent B, K, N|} K')) \
   1.712 -\            : setOfList evs  \
   1.713 -\         |] ==> knownBy evs K <= {A,Server}";
   1.714 -
   1.715 -
   1.716 -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.717  
   1.718  (*NEEDED??*)
   1.719  
   1.720 @@ -419,20 +645,11 @@
   1.721  by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); 
   1.722  qed "in_parts_sees_Says";
   1.723  
   1.724 -goal thy "!!evs. length evs < length evs' ==> newK (A,evs) ~= newK (A',evs')";
   1.725 +goal thy "!!evs. length evs < length evs' ==> newK  evs ~= newK (A',evs')";
   1.726  by (fast_tac (!claset addSEs [less_irrefl]) 1);
   1.727  qed "length_less_newK_neq";
   1.728  
   1.729  
   1.730 -(*Initially
   1.731 -goal thy "knownBy [] X = \
   1.732 -\         {A. X = Key (invKey (serverKey A)) | (? i. X = Key (serverKey i))}";
   1.733 -by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
   1.734 -qed "knownBy_Nil";
   1.735 -
   1.736 -goal thy "!!X. knownBy (x#l) X = ?F(knownBy l X)";
   1.737 -by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
   1.738 -********************)
   1.739  
   1.740  goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
   1.741  \         insert {|X,Y|} (insert (Crypt x) evs)";
   1.742 @@ -441,39 +658,6 @@
   1.743  
   1.744  
   1.745  
   1.746 -WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
   1.747 -
   1.748 -goal thy 
   1.749 - "!!evs. evs : traces ==> \
   1.750 -\     Says Server A       \
   1.751 -\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
   1.752 -\     --> (EX evs'. K = Key (newK(Server,evs')))";
   1.753 -be traces.induct 1;
   1.754 -by (ALLGOALS Asm_simp_tac);
   1.755 -by (Fast_tac 1);
   1.756 -val Says_Server_lemma = result();
   1.757 -
   1.758 -goal thy 
   1.759 - "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
   1.760 -\               : setOfList evs;  \
   1.761 -\           evs : traces          \
   1.762 -\        |] ==> (EX evs'. K = Key (newK(Server,evs')))";
   1.763 -bd Says_Server_lemma 1;
   1.764 -by (Fast_tac 1);
   1.765 -qed "Says_Server_imp_Key_newK";
   1.766 -
   1.767 -
   1.768 -goal thy 
   1.769 - "!!evs. evs : traces ==> \
   1.770 -\     Says Server A \
   1.771 -\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
   1.772 -\     --> (EX evs'. N = Nonce (newN(A,evs')))";
   1.773 -be traces.induct 1;
   1.774 -by (ALLGOALS Asm_simp_tac);
   1.775 -by (Fast_tac 1);
   1.776 -val Says_Server_lemma = result();
   1.777 -
   1.778 -
   1.779  YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   1.780  
   1.781  goalw thy [keysFor_def]
     2.1 --- a/src/HOL/Auth/Event.thy	Thu Jul 11 15:28:10 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Thu Jul 11 15:30:22 1996 +0200
     2.3 @@ -6,6 +6,8 @@
     2.4  Datatype of events;
     2.5  inductive relation "traces" for Needham-Schroeder (shared keys)
     2.6  
     2.7 +INTERLEAVING?  See defn of "traces"
     2.8 +
     2.9  WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
    2.10    PUBLIC KEY...
    2.11  *)
    2.12 @@ -14,16 +16,16 @@
    2.13  
    2.14  consts
    2.15    publicKey    :: agent => key
    2.16 -  serverKey    :: agent => key	(*symmetric keys*)
    2.17 +  serverKey    :: agent => key  (*symmetric keys*)
    2.18  
    2.19  rules
    2.20    isSym_serverKey "isSymKey (serverKey A)"
    2.21  
    2.22 -consts	(*Initial states of agents -- parameter of the construction*)
    2.23 +consts  (*Initial states of agents -- parameter of the construction*)
    2.24    initState :: agent => msg set
    2.25  
    2.26  primrec initState agent
    2.27 -	(*Server knows all keys; other agents know only their own*)
    2.28 +        (*Server knows all keys; other agents know only their own*)
    2.29    initState_Server  "initState Server     = range (Key o serverKey)"
    2.30    initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    2.31    initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    2.32 @@ -51,7 +53,7 @@
    2.33    sees :: [agent, event list] => msg set
    2.34  
    2.35  primrec sees list
    2.36 -	(*Initial knowledge includes all public keys and own private key*)
    2.37 +        (*Initial knowledge includes all public keys and own private key*)
    2.38    sees_Nil  "sees A []       = initState A"
    2.39    sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    2.40  
    2.41 @@ -61,25 +63,29 @@
    2.42    "knownBy evs X == {A. X: analyze (sees A evs)}"
    2.43  
    2.44  
    2.45 -(*Agents generate "random" nonces.  Different agents always generate
    2.46 -  different nonces.  Different traces also yield different nonces.  Same
    2.47 -  applies for keys.*)
    2.48 -(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.  REMOVE AGENT ARGUMENT?
    2.49 +(*Agents generate "random" nonces.  Different traces always yield
    2.50 +  different nonces.  Same applies for keys.*)
    2.51 +(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
    2.52    NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
    2.53  consts
    2.54 -  newN :: "agent * event list => nat"
    2.55 -  newK :: "agent * event list => key"
    2.56 +  newN :: "event list => nat"
    2.57 +  newK :: "event list => key"
    2.58  
    2.59  rules
    2.60    inj_serverKey "inj serverKey"
    2.61  
    2.62    inj_newN   "inj(newN)"
    2.63 -  fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" 
    2.64 +  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    2.65  
    2.66    inj_newK   "inj(newK)"
    2.67 -  fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" 
    2.68 -  isSym_newK "isSymKey (newK(A,evs))"
    2.69 +  fresh_newK "Key (newK evs) ~: parts (initState B)" 
    2.70 +  isSym_newK "isSymKey (newK evs)"
    2.71 +
    2.72  
    2.73 +(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
    2.74 +  MOST RECENT message.  Does this mean we can't model middleperson attacks?
    2.75 +  We don't need the most recent restriction in order to handle interception
    2.76 +  by the Enemy, as agents are not forced to respond anyway.*)
    2.77  
    2.78  consts  traces   :: "event list set"
    2.79  inductive traces
    2.80 @@ -88,17 +94,39 @@
    2.81  
    2.82      (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.83        invent new nonces here, but he can also use NS1.*)
    2.84 -    Fake "[| evs: traces;  X: synthesize(analyze(sees Enemy evs))
    2.85 +    Fake "[| evs: traces;  B ~= Enemy;  
    2.86 +             X: synthesize(analyze(sees Enemy evs))
    2.87            |] ==> (Says Enemy B X) # evs : traces"
    2.88  
    2.89      NS1  "[| evs: traces;  A ~= Server
    2.90 -          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) 
    2.91 +          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    2.92                   # evs : traces"
    2.93  
    2.94 -    NS2  "[| evs: traces;  
    2.95 +          (*We can't trust the sender field: change that A to A'?  *)
    2.96 +    NS2  "[| evs: traces;  A ~= B;
    2.97               evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
    2.98            |] ==> (Says Server A 
    2.99 -                       (Crypt {|Agent A, Agent B, 
   2.100 -                                Key (newK(Server,evs)), Nonce NA|}
   2.101 -                              (serverKey A))) # evs : traces"
   2.102 +                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
   2.103 +                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
   2.104 +                   (serverKey A))) # evs : traces"
   2.105 +
   2.106 +           (*We can't assume S=Server.  Agent A "remembers" her nonce.
   2.107 +             May assume WLOG that she is NOT the Enemy, as the Fake rule.
   2.108 +             covers this case.  Can inductively show A ~= Server*)
   2.109 +    NS3  "[| evs: traces;  A ~= B;
   2.110 +             evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
   2.111 +                              (serverKey A))) 
   2.112 +                   # evs';
   2.113 +             A = Friend i;
   2.114 +             (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
   2.115 +          |] ==> (Says A B X) # evs : traces"
   2.116 +
   2.117 +(*Initial version of NS2 had 
   2.118 +
   2.119 +        {|Agent A, Agent B, Key (newK evs), Nonce NA|}
   2.120 +
   2.121 +  for the encrypted part; the version above is LESS transparent, hence
   2.122 +  maybe HARDER to prove.  Also it is precisely as in the BAN paper.
   2.123 +*)
   2.124 +
   2.125  end
     3.1 --- a/src/HOL/Auth/Message.ML	Thu Jul 11 15:28:10 1996 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Thu Jul 11 15:30:22 1996 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4  
     3.5  fun auto() = by (Auto_tac());
     3.6  
     3.7 -fun imp_of_subset th = th RSN (2, rev_subsetD);
     3.8 +fun impOfSubs th = th RSN (2, rev_subsetD);
     3.9  
    3.10  (**************** INSTALL CENTRALLY SOMEWHERE? ****************)
    3.11  
    3.12 @@ -141,6 +141,13 @@
    3.13  by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
    3.14  qed "parts_Un";
    3.15  
    3.16 +(*TWO inserts to avoid looping.  This rewrite is better than nothing...*)
    3.17 +goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
    3.18 +by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
    3.19 +by (stac (read_instantiate [("A","{Y} Un H")] insert_is_Un) 1);
    3.20 +by (simp_tac (HOL_ss addsimps [parts_Un, Un_assoc]) 1);
    3.21 +qed "parts_insert2";
    3.22 +
    3.23  goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
    3.24  by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
    3.25  val parts_UN_subset1 = result();
    3.26 @@ -163,7 +170,7 @@
    3.27  Addsimps [parts_Un, parts_UN, parts_UN1];
    3.28  
    3.29  goal thy "insert X (parts H) <= parts(insert X H)";
    3.30 -by (fast_tac (!claset addEs [imp_of_subset parts_mono]) 1);
    3.31 +by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1);
    3.32  qed "parts_insert_subset";
    3.33  
    3.34  (*Especially for reasoning about the Fake rule in traces*)
    3.35 @@ -304,7 +311,7 @@
    3.36  qed "analyze_Un";
    3.37  
    3.38  goal thy "insert X (analyze H) <= analyze(insert X H)";
    3.39 -by (fast_tac (!claset addEs [imp_of_subset analyze_mono]) 1);
    3.40 +by (fast_tac (!claset addEs [impOfSubs analyze_mono]) 1);
    3.41  qed "analyze_insert";
    3.42  
    3.43  (** Rewrite rules for pulling out atomic messages **)
    3.44 @@ -400,7 +407,7 @@
    3.45  \         insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))";
    3.46  by (rtac equalityI 1);
    3.47  by (best_tac (!claset addIs [analyze.Fst,
    3.48 -			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
    3.49 +			     impOfSubs analyze_insert_subset_MPair2]) 2); 
    3.50  br subsetI 1;
    3.51  be analyze.induct 1;
    3.52  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.53 @@ -410,7 +417,7 @@
    3.54  \         insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))";
    3.55  by (rtac equalityI 1);
    3.56  by (best_tac (!claset addIs [analyze.Fst,
    3.57 -			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
    3.58 +			     impOfSubs analyze_insert_subset_MPair2]) 2); 
    3.59  br subsetI 1;
    3.60  be analyze.induct 1;
    3.61  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.62 @@ -423,7 +430,7 @@
    3.63  \         insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))";
    3.64  by (rtac equalityI 1);
    3.65  by (best_tac (!claset addIs [analyze.Fst,
    3.66 -			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
    3.67 +			     impOfSubs analyze_insert_subset_MPair2]) 2); 
    3.68  br subsetI 1;
    3.69  be analyze.induct 1;
    3.70  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.71 @@ -471,12 +478,12 @@
    3.72  (*Helps to prove Fake cases*)
    3.73  goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)";
    3.74  be analyze.induct 1;
    3.75 -by (ALLGOALS (fast_tac (!claset addEs [imp_of_subset analyze_mono])));
    3.76 +by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analyze_mono])));
    3.77  val lemma = result();
    3.78  
    3.79  goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";
    3.80  by (fast_tac (!claset addIs [lemma]
    3.81 -		      addEs [imp_of_subset analyze_mono]) 1);
    3.82 +		      addEs [impOfSubs analyze_mono]) 1);
    3.83  qed "analyze_UN_analyze";
    3.84  Addsimps [analyze_UN_analyze];
    3.85  
    3.86 @@ -595,8 +602,8 @@
    3.87  br subsetI 1;
    3.88  be analyze.induct 1;
    3.89  by (best_tac
    3.90 -    (!claset addEs [imp_of_subset synthesize_increasing,
    3.91 -		    imp_of_subset analyze_mono]) 5);
    3.92 +    (!claset addEs [impOfSubs synthesize_increasing,
    3.93 +		    impOfSubs analyze_mono]) 5);
    3.94  by (Best_tac 1);
    3.95  by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);
    3.96  by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);