Proving safety properties of authentication protocols
authorpaulson
Fri Jun 28 15:26:39 1996 +0200 (1996-06-28)
changeset 1839199243afac2b
parent 1838 91e0395adc72
child 1840 149b2e69633e
Proving safety properties of authentication protocols
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Event.ML	Fri Jun 28 15:26:39 1996 +0200
     1.3 @@ -0,0 +1,491 @@
     1.4 +(*  Title:      HOL/Auth/Message
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Datatype of events;
    1.10 +inductive relation "traces" for Needham-Schroeder (shared keys)
    1.11 +*)
    1.12 +
    1.13 +
    1.14 +open Event;
    1.15 +
    1.16 +(* invKey (serverKey A) = serverKey A *)
    1.17 +bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
    1.18 +
    1.19 +(* invKey (newK(A,evs)) = newK(A,evs) *)
    1.20 +bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    1.21 +Addsimps [invKey_serverKey, invKey_newK];
    1.22 +
    1.23 +
    1.24 +(*New keys and nonces are fresh*)
    1.25 +val serverKey_inject = inj_serverKey RS injD;
    1.26 +val newN_inject = inj_newN RS injD RS Pair_inject
    1.27 +and newK_inject = inj_newK RS injD RS Pair_inject;
    1.28 +AddSEs [serverKey_inject, newN_inject, newK_inject,
    1.29 +	fresh_newK RS notE, fresh_newN RS notE];
    1.30 +Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    1.31 +Addsimps [fresh_newN, fresh_newK];
    1.32 +
    1.33 +goal thy "newK (A,evs) ~= serverKey B";
    1.34 +by (subgoal_tac "newK (A,evs) = serverKey B --> \
    1.35 +\                Key (newK(A,evs)) : parts (initState B)" 1);
    1.36 +by (Fast_tac 1);
    1.37 +by (agent.induct_tac "B" 1);
    1.38 +by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.39 +qed "newK_neq_serverKey";
    1.40 +
    1.41 +Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
    1.42 +
    1.43 +(*Good for talking about Server's initial state*)
    1.44 +goal thy "parts (range (Key o f)) = range (Key o f)";
    1.45 +by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.46 +be parts.induct 1;
    1.47 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.48 +qed "parts_range_Key";
    1.49 +
    1.50 +goal thy "analyze (range (Key o f)) = range (Key o f)";
    1.51 +by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.52 +be analyze.induct 1;
    1.53 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.54 +qed "analyze_range_Key";
    1.55 +
    1.56 +Addsimps [parts_range_Key, analyze_range_Key];
    1.57 +
    1.58 +goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    1.59 +by (agent.induct_tac "C" 1);
    1.60 +by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.61 +qed "keysFor_parts_initState";
    1.62 +Addsimps [keysFor_parts_initState];
    1.63 +
    1.64 +
    1.65 +(**** Inductive relation "traces" -- basic properties ****)
    1.66 +
    1.67 +val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps);
    1.68 +
    1.69 +val Says_tracesE        = mk_cases "Says A B X # evs: traces";
    1.70 +val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
    1.71 +val Says_Enemy_tracesE  = mk_cases "Says Enemy B X # evs: traces";
    1.72 +val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
    1.73 +val Notes_tracesE       = mk_cases "Notes A X # evs: traces";
    1.74 +
    1.75 +
    1.76 +(*The tail of a trace is a trace*)
    1.77 +goal thy "!!ev evs. ev#evs : traces ==> evs : traces";
    1.78 +by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
    1.79 +qed "traces_ConsE";
    1.80 +
    1.81 +(** Specialized rewrite rules for (sees A (Says...#evs)) **)
    1.82 +
    1.83 +goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
    1.84 +by (Simp_tac 1);
    1.85 +by (Fast_tac 1);
    1.86 +qed "sees_own";
    1.87 +
    1.88 +goal thy "!!A. Server ~= A ==> \
    1.89 +\              sees Server (Says A B X # evs) = sees Server evs";
    1.90 +by (Asm_simp_tac 1);
    1.91 +qed "sees_Server";
    1.92 +
    1.93 +goal thy "!!A. Friend i ~= A ==> \
    1.94 +\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
    1.95 +by (Asm_simp_tac 1);
    1.96 +qed "sees_Friend";
    1.97 +
    1.98 +goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
    1.99 +by (Simp_tac 1);
   1.100 +by (Fast_tac 1);
   1.101 +qed "sees_Enemy";
   1.102 +
   1.103 +goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
   1.104 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.105 +by (Fast_tac 1);
   1.106 +qed "sees_subset";
   1.107 +
   1.108 +(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
   1.109 +goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
   1.110 +\         parts {Y} Un (UN A. parts (sees A evs))";
   1.111 +by (Step_tac 1);
   1.112 +be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
   1.113 +val ss = (!simpset addsimps [parts_Un, sees_Cons] 
   1.114 +	           setloop split_tac [expand_if]);
   1.115 +by (ALLGOALS (fast_tac (!claset addss ss)));
   1.116 +qed "UN_parts_sees_Says";
   1.117 +
   1.118 +
   1.119 +Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
   1.120 +Delsimps [sees_Cons];
   1.121 +
   1.122 +
   1.123 +(**** Inductive proofs about traces ****)
   1.124 +
   1.125 +(*The Enemy can see more than anybody else, except for their initial state*)
   1.126 +goal thy 
   1.127 + "!!evs. evs : traces ==> \
   1.128 +\     sees A evs <= initState A Un sees Enemy evs";
   1.129 +be traces.induct 1;
   1.130 +be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
   1.131 +by (ALLGOALS (fast_tac (!claset addDs [sees_subset RS subsetD] 
   1.132 +			        addss (!simpset))));
   1.133 +qed "sees_agent_subset_sees_Enemy";
   1.134 +
   1.135 +
   1.136 +(*** Server keys are not betrayed ***)
   1.137 +
   1.138 +(*No Enemy will ever see a Friend's server key
   1.139 +   -- even if another friend's key is compromised.
   1.140 +  The UN is essential to handle the Fake rule in the induction.*)
   1.141 +goal thy 
   1.142 + "!!evs. [| evs : traces;  i~=j |] ==> \
   1.143 +\        Key (serverKey (Friend i)) ~: \
   1.144 +\        parts (initState (Friend j) Un sees Enemy evs)";
   1.145 +be traces.induct 1;
   1.146 +be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.147 +by (Auto_tac());
   1.148 +(*Deals with Faked messages*)
   1.149 +by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
   1.150 +			     imp_of_subset parts_insert_subset_Un]
   1.151 +	              addss (!simpset)) 1);
   1.152 +qed "Enemy_not_see_serverKey";
   1.153 +
   1.154 +(*No Friend will ever see another Friend's server key.*)
   1.155 +goal thy 
   1.156 + "!!evs. [| evs : traces;  i~=j |] ==> \
   1.157 +\        Key (serverKey (Friend i)) ~: parts (sees (Friend j) evs)";
   1.158 +br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   1.159 +by (REPEAT (ares_tac [Enemy_not_see_serverKey] 1));
   1.160 +qed "Friend_not_see_serverKey";
   1.161 +
   1.162 +(*Variant needed for the theorem below*)
   1.163 +goal thy 
   1.164 + "!!evs. evs : traces ==> \
   1.165 +\        Key (serverKey (Friend i)) ~: analyze (sees Enemy evs)";
   1.166 +bd Enemy_not_see_serverKey 1;
   1.167 +br n_not_Suc_n 1;
   1.168 +by (Full_simp_tac 1);
   1.169 +by (fast_tac (!claset addDs [imp_of_subset analyze_subset_parts]) 1);
   1.170 +qed "serverKeys_not_analyzed";
   1.171 +
   1.172 +
   1.173 +(*** Future keys can't be seen or used! ***)
   1.174 +
   1.175 +(*Nobody can have SEEN keys that will be generated in the future.
   1.176 +  This has to be proved anew for each protocol description,
   1.177 +  but should go by similar reasoning every time.  Hardest case is the
   1.178 +  standard Fake rule.  
   1.179 +      The length comparison, and Union over C, are essential for the 
   1.180 +  induction! *)
   1.181 +goal thy "!!evs. evs : traces ==> \
   1.182 +\                length evs <= length evs' --> \
   1.183 +\                          Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
   1.184 +be traces.induct 1;
   1.185 +be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.186 +by (ALLGOALS (asm_full_simp_tac
   1.187 +	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
   1.188 +(*Initial state?  New keys cannot clash*)
   1.189 +by (Fast_tac 1);
   1.190 +(*Rule NS1 in protocol*)
   1.191 +by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.192 +(*Rule NS2 in protocol*)
   1.193 +by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
   1.194 +(*Rule Fake: where an Enemy agent can say practically anything*)
   1.195 +by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
   1.196 +			     imp_of_subset parts_insert_subset_Un,
   1.197 +			     less_imp_le]
   1.198 +	              addss (!simpset)) 1);
   1.199 +val lemma = result();
   1.200 +
   1.201 +(*Variant needed for the main theorem below*)
   1.202 +goal thy 
   1.203 + "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
   1.204 +\        Key (newK (A,evs')) ~: parts (sees C evs)";
   1.205 +by (fast_tac (!claset addDs [lemma]) 1);
   1.206 +qed "new_keys_not_seen";
   1.207 +
   1.208 +goal thy "!!K. newK(A,evs) = invKey K ==> newK(A,evs) = K";
   1.209 +br (invKey_eq RS iffD1) 1;
   1.210 +by (Simp_tac 1);
   1.211 +val newK_invKey = result();
   1.212 +
   1.213 +(*Nobody can have USED keys that will be generated in the future.
   1.214 +  ...very like new_keys_not_seen*)
   1.215 +goal thy "!!evs. evs : traces ==> \
   1.216 +\                length evs <= length evs' --> \
   1.217 +\                newK (A,evs') ~: keysFor (UN C. parts (sees C evs))";
   1.218 +be traces.induct 1;
   1.219 +be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.220 +by (ALLGOALS (asm_full_simp_tac
   1.221 +	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
   1.222 +(*Rule NS1 in protocol*)
   1.223 +by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.224 +(*Rule NS2 in protocol*)
   1.225 +by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.226 +(*Rule Fake: where an Enemy agent can say practically anything*)
   1.227 +by (best_tac 
   1.228 +    (!claset addSDs [newK_invKey]
   1.229 +	     addDs [imp_of_subset (analyze_subset_parts RS keysFor_mono),
   1.230 +		    imp_of_subset (parts_insert_subset_Un RS keysFor_mono),
   1.231 +		    less_imp_le]
   1.232 +             addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
   1.233 +	     addss (!simpset)) 1);
   1.234 +val lemma = result();
   1.235 +
   1.236 +goal thy 
   1.237 + "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
   1.238 +\        newK (A,evs') ~: keysFor (parts (sees C evs))";
   1.239 +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.240 +qed "new_keys_not_used";
   1.241 +
   1.242 +bind_thm ("new_keys_not_used_analyze",
   1.243 +	  [analyze_subset_parts RS keysFor_mono,
   1.244 +	   new_keys_not_used] MRS contra_subsetD);
   1.245 +
   1.246 +
   1.247 +(*Pushes Crypt events in so that others might be pulled out*)
   1.248 +goal thy "insert (Crypt X K) (insert y evs) = \
   1.249 +\         insert y (insert (Crypt X K) evs)";
   1.250 +by (Fast_tac 1);
   1.251 +qed "insert_Crypt_delay";
   1.252 +
   1.253 +goal thy "insert (Key K) (insert y evs) = \
   1.254 +\         insert y (insert (Key K) evs)";
   1.255 +by (Fast_tac 1);
   1.256 +qed "insert_Key_delay";
   1.257 +
   1.258 +(** Lemmas concerning the form of items passed in messages **)
   1.259 +
   1.260 +(*Describes the form *and age* of K when the following message is sent*)
   1.261 +goal thy 
   1.262 + "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
   1.263 +\               : setOfList evs;  \
   1.264 +\           evs : traces          \
   1.265 +\        |] ==> (EX evs'. K = Key (newK(Server,evs')) & \
   1.266 +\                         length evs' < length evs)";
   1.267 +be rev_mp 1;
   1.268 +be traces.induct 1;
   1.269 +be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.270 +by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.271 +qed "Says_Server_imp_Key_newK";
   1.272 +
   1.273 +Addsimps [serverKeys_not_analyzed, 
   1.274 +	  new_keys_not_seen RS not_parts_not_analyze,
   1.275 +	  new_keys_not_used_analyze];
   1.276 +
   1.277 +
   1.278 +goal thy 
   1.279 + "!!evs. evs : traces ==> \
   1.280 +\     Says Server (Friend i) \
   1.281 +\          (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs  \
   1.282 +\     --> K ~: analyze (sees Enemy evs)";
   1.283 +be traces.induct 1;
   1.284 +be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
   1.285 +by (ALLGOALS Asm_full_simp_tac);
   1.286 +(*We infer that K has the form "Key (newK(Server,evs')" ... *)
   1.287 +br conjI 3;
   1.288 +by (REPEAT_FIRST (resolve_tac [impI]));
   1.289 +by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
   1.290 +(*NS1, subgoal concerns "(Says A Server
   1.291 +                          {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
   1.292 +(*... thus it cannot equal any components of A's message above.*)
   1.293 +by (fast_tac (!claset addss (!simpset)) 2);
   1.294 +(*NS2, the subcase where that message was the most recently sent;
   1.295 +  it holds because here K' = serverKey(Friend i), which Enemies can't see*)
   1.296 +by (fast_tac (!claset addss (!simpset)) 2);
   1.297 +(*NS2, other subcase!*)
   1.298 +by (fast_tac 
   1.299 +    (!claset addSEs [less_irrefl]
   1.300 +             addDs [imp_of_subset analyze_insert_Crypt_subset]
   1.301 +	     addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
   1.302 +(*Now for the Fake case*)
   1.303 +be exE 1;
   1.304 +br notI 1;
   1.305 +by (REPEAT (etac conjE 1));
   1.306 +by (REPEAT (hyp_subst_tac 1));
   1.307 +by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
   1.308 +be (imp_of_subset analyze_mono) 2;
   1.309 +by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
   1.310 +			     (2,rev_subsetD),
   1.311 +			     imp_of_subset synthesize_increasing,
   1.312 +			     imp_of_subset analyze_increasing]) 2);
   1.313 +(*Proves the Fake goal*)
   1.314 +by (Auto_tac());
   1.315 +qed "encrypted_key_not_seen";
   1.316 +
   1.317 +
   1.318 +
   1.319 +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.320 +
   1.321 +(*Nobody can have SEEN keys that will be generated in the future.
   1.322 +  This has to be proved anew for each protocol description,
   1.323 +  but should go by similar reasoning every time.  Hardest case is the
   1.324 +  standard Fake rule.  
   1.325 +      The length comparison, and Union over C, are essential for the 
   1.326 +  induction! *)
   1.327 +goal thy "!!evs. evs : traces ==> \
   1.328 +\                length evs <= length evs' --> \
   1.329 +\                          Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
   1.330 +be traces.induct 1;
   1.331 +be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
   1.332 +by (ALLGOALS (asm_full_simp_tac
   1.333 +	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
   1.334 +(*Initial state?  New keys cannot clash*)
   1.335 +by (Fast_tac 1);
   1.336 +(*Rule NS1 in protocol*)
   1.337 +by (fast_tac (!claset addDs [less_imp_le]) 2);
   1.338 +(*Rule NS2 in protocol*)
   1.339 +by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
   1.340 +(*Rule Fake: where an Enemy agent can say practically anything*)
   1.341 +by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
   1.342 +			     imp_of_subset parts_insert_subset_Un,
   1.343 +			     less_imp_le]
   1.344 +	              addss (!simpset)) 1);
   1.345 +val lemma = result();
   1.346 +
   1.347 +
   1.348 +
   1.349 +goal thy 
   1.350 + "!!evs. [| evs : traces;  i~=j |] ==> \
   1.351 +\     Says Server (Friend i) \
   1.352 +\          (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs  \
   1.353 +\     --> K ~: analyze (initState (Friend j) Un sees Enemy evs)";
   1.354 +be traces.induct 1;
   1.355 +be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
   1.356 +by (ALLGOALS Asm_full_simp_tac);
   1.357 +(*We infer that K has the form "Key (newK(Server,evs')" ... *)
   1.358 +br conjI 3;
   1.359 +by (REPEAT_FIRST (resolve_tac [impI]));
   1.360 +by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
   1.361 +(*NS1, subgoal concerns "(Says A Server
   1.362 +                          {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
   1.363 +(*... thus it cannot equal any components of A's message above.*)
   1.364 +
   1.365 +by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
   1.366 +
   1.367 +by (fast_tac (!claset addss (!simpset)) 2);
   1.368 +(*NS2, the subcase where that message was the most recently sent;
   1.369 +  it holds because here K' = serverKey(Friend i), which Enemies can't see*)
   1.370 +by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
   1.371 +by (Safe_step_tac 2);
   1.372 +
   1.373 +by (stac analyze_insert_Crypt 2);
   1.374 +
   1.375 +by (fast_tac (!claset addss (!simpset)) 2);
   1.376 +(*NS2, other subcase!*)
   1.377 +
   1.378 +by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
   1.379 +by (fast_tac 
   1.380 +    (!claset addSEs [less_irrefl]
   1.381 +             addDs [imp_of_subset analyze_insert_Crypt_subset]
   1.382 +	     addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
   1.383 +(*Now for the Fake case*)
   1.384 +be exE 1;
   1.385 +br notI 1;
   1.386 +by (REPEAT (etac conjE 1));
   1.387 +by (REPEAT (hyp_subst_tac 1));
   1.388 +by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
   1.389 +be (imp_of_subset analyze_mono) 2;
   1.390 +by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
   1.391 +			     (2,rev_subsetD),
   1.392 +			     imp_of_subset synthesize_increasing,
   1.393 +			     imp_of_subset analyze_increasing]) 2);
   1.394 +(*Proves the Fake goal*)
   1.395 +by (Auto_tac());
   1.396 +qed "encrypted_key_not_seen";
   1.397 +
   1.398 +
   1.399 +
   1.400 +
   1.401 +(*Bet this requires the premise   A = Friend i *)
   1.402 +goal thy "[| evs : traces;  \
   1.403 +\            (Says Server A (Crypt {|Agent A, Agent B, K, N|} K')) \
   1.404 +\            : setOfList evs  \
   1.405 +\         |] ==> knownBy evs K <= {A,Server}";
   1.406 +
   1.407 +
   1.408 +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.409 +
   1.410 +(*NEEDED??*)
   1.411 +
   1.412 +goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)";
   1.413 +by (asm_simp_tac (!simpset addsimps [sees_Cons] 
   1.414 +                           setloop split_tac [expand_if]) 1); 
   1.415 +qed "in_sees_Says";
   1.416 +
   1.417 +goal thy "!!A. X ~: parts {Y} ==> \
   1.418 +\              (X : parts (sees A (Says B C Y # evs))) = \
   1.419 +\              (X : parts (sees A evs))";
   1.420 +by (asm_simp_tac (!simpset addsimps [sees_Cons] 
   1.421 +                           setloop split_tac [expand_if]) 1); 
   1.422 +by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); 
   1.423 +qed "in_parts_sees_Says";
   1.424 +
   1.425 +goal thy "!!evs. length evs < length evs' ==> newK (A,evs) ~= newK (A',evs')";
   1.426 +by (fast_tac (!claset addSEs [less_irrefl]) 1);
   1.427 +qed "length_less_newK_neq";
   1.428 +
   1.429 +
   1.430 +(*Initially
   1.431 +goal thy "knownBy [] X = \
   1.432 +\         {A. X = Key (invKey (serverKey A)) | (? i. X = Key (serverKey i))}";
   1.433 +by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
   1.434 +qed "knownBy_Nil";
   1.435 +
   1.436 +goal thy "!!X. knownBy (x#l) X = ?F(knownBy l X)";
   1.437 +by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
   1.438 +********************)
   1.439 +
   1.440 +goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
   1.441 +\         insert {|X,Y|} (insert (Crypt x) evs)";
   1.442 +by (Fast_tac 1);
   1.443 +qed "insert_Crypt_MPair_delay";
   1.444 +
   1.445 +
   1.446 +
   1.447 +WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
   1.448 +
   1.449 +goal thy 
   1.450 + "!!evs. evs : traces ==> \
   1.451 +\     Says Server A       \
   1.452 +\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
   1.453 +\     --> (EX evs'. K = Key (newK(Server,evs')))";
   1.454 +be traces.induct 1;
   1.455 +by (ALLGOALS Asm_simp_tac);
   1.456 +by (Fast_tac 1);
   1.457 +val Says_Server_lemma = result();
   1.458 +
   1.459 +goal thy 
   1.460 + "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
   1.461 +\               : setOfList evs;  \
   1.462 +\           evs : traces          \
   1.463 +\        |] ==> (EX evs'. K = Key (newK(Server,evs')))";
   1.464 +bd Says_Server_lemma 1;
   1.465 +by (Fast_tac 1);
   1.466 +qed "Says_Server_imp_Key_newK";
   1.467 +
   1.468 +
   1.469 +goal thy 
   1.470 + "!!evs. evs : traces ==> \
   1.471 +\     Says Server A \
   1.472 +\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
   1.473 +\     --> (EX evs'. N = Nonce (newN(A,evs')))";
   1.474 +be traces.induct 1;
   1.475 +by (ALLGOALS Asm_simp_tac);
   1.476 +by (Fast_tac 1);
   1.477 +val Says_Server_lemma = result();
   1.478 +
   1.479 +
   1.480 +YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   1.481 +
   1.482 +goalw thy [keysFor_def]
   1.483 +    "!!X. Crypt X K: H ==> invKey K : keysFor H";
   1.484 +by (Fast_tac 1);
   1.485 +qed "keysFor_I";
   1.486 +AddSIs [keysFor_I];
   1.487 +
   1.488 +goalw thy [keysFor_def]
   1.489 +    "!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H";
   1.490 +by (Fast_tac 1);
   1.491 +qed "keysFor_D";
   1.492 +AddSDs [keysFor_D];
   1.493 +
   1.494 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/Event.thy	Fri Jun 28 15:26:39 1996 +0200
     2.3 @@ -0,0 +1,104 @@
     2.4 +(*  Title:      HOL/Auth/Message
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Datatype of events;
    2.10 +inductive relation "traces" for Needham-Schroeder (shared keys)
    2.11 +
    2.12 +WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
    2.13 +  PUBLIC KEY...
    2.14 +*)
    2.15 +
    2.16 +Event = Message + List + 
    2.17 +
    2.18 +consts
    2.19 +  publicKey    :: agent => key
    2.20 +  serverKey    :: agent => key	(*symmetric keys*)
    2.21 +
    2.22 +rules
    2.23 +  isSym_serverKey "isSymKey (serverKey A)"
    2.24 +
    2.25 +consts	(*Initial states of agents -- parameter of the construction*)
    2.26 +  initState :: agent => msg set
    2.27 +
    2.28 +primrec initState agent
    2.29 +	(*Server knows all keys; other agents know only their own*)
    2.30 +  initState_Server  "initState Server     = range (Key o serverKey)"
    2.31 +  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    2.32 +  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    2.33 +
    2.34 +(**
    2.35 +For asymmetric keys: server knows all public and private keys,
    2.36 +  others know their private key and perhaps all public keys  
    2.37 +**)
    2.38 +
    2.39 +datatype  (*Messages, and components of agent stores*)
    2.40 +  event = Says agent agent msg
    2.41 +        | Notes agent msg
    2.42 +
    2.43 +consts  
    2.44 +  sees1 :: [agent, event] => msg set
    2.45 +
    2.46 +primrec sees1 event
    2.47 +           (*First agent recalls all that it says, but NOT everything
    2.48 +             that is sent to it; it must note such things if/when received*)
    2.49 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    2.50 +          (*part of A's internal state*)
    2.51 +  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    2.52 +
    2.53 +consts  
    2.54 +  sees :: [agent, event list] => msg set
    2.55 +
    2.56 +primrec sees list
    2.57 +	(*Initial knowledge includes all public keys and own private key*)
    2.58 +  sees_Nil  "sees A []       = initState A"
    2.59 +  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    2.60 +
    2.61 +
    2.62 +constdefs
    2.63 +  knownBy :: [event list, msg] => agent set
    2.64 +  "knownBy evs X == {A. X: analyze (sees A evs)}"
    2.65 +
    2.66 +
    2.67 +(*Agents generate "random" nonces.  Different agents always generate
    2.68 +  different nonces.  Different traces also yield different nonces.  Same
    2.69 +  applies for keys.*)
    2.70 +(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.  REMOVE AGENT ARGUMENT?
    2.71 +  NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
    2.72 +consts
    2.73 +  newN :: "agent * event list => nat"
    2.74 +  newK :: "agent * event list => key"
    2.75 +
    2.76 +rules
    2.77 +  inj_serverKey "inj serverKey"
    2.78 +
    2.79 +  inj_newN   "inj(newN)"
    2.80 +  fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" 
    2.81 +
    2.82 +  inj_newK   "inj(newK)"
    2.83 +  fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" 
    2.84 +  isSym_newK "isSymKey (newK(A,evs))"
    2.85 +
    2.86 +
    2.87 +consts  traces   :: "event list set"
    2.88 +inductive traces
    2.89 +  intrs 
    2.90 +    Nil  "[]: traces"
    2.91 +
    2.92 +    (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.93 +      invent new nonces here, but he can also use NS1.*)
    2.94 +    Fake "[| evs: traces;  X: synthesize(analyze(sees Enemy evs))
    2.95 +          |] ==> (Says Enemy B X) # evs : traces"
    2.96 +
    2.97 +    NS1  "[| evs: traces;  A ~= Server
    2.98 +          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) 
    2.99 +                 # evs : traces"
   2.100 +
   2.101 +    NS2  "[| evs: traces;  
   2.102 +             evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
   2.103 +          |] ==> (Says Server A 
   2.104 +                       (Crypt {|Agent A, Agent B, 
   2.105 +                                Key (newK(Server,evs)), Nonce NA|}
   2.106 +                              (serverKey A))) # evs : traces"
   2.107 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/Message.ML	Fri Jun 28 15:26:39 1996 +0200
     3.3 @@ -0,0 +1,606 @@
     3.4 +(*  Title:      HOL/Auth/Message
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1996  University of Cambridge
     3.8 +
     3.9 +Datatypes of agents and messages;
    3.10 +Inductive relations "parts", "analyze" and "synthesize"
    3.11 +*)
    3.12 +
    3.13 +open Message;
    3.14 +
    3.15 +
    3.16 +(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
    3.17 +
    3.18 +(*Maybe swap the safe_tac and simp_tac lines?**)
    3.19 +fun auto_tac (cs,ss) = 
    3.20 +    TRY (safe_tac cs) THEN 
    3.21 +    ALLGOALS (asm_full_simp_tac ss) THEN
    3.22 +    REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
    3.23 +
    3.24 +fun Auto_tac() = auto_tac (!claset, !simpset);
    3.25 +
    3.26 +fun auto() = by (Auto_tac());
    3.27 +
    3.28 +fun imp_of_subset th = th RSN (2, rev_subsetD);
    3.29 +
    3.30 +(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
    3.31 +
    3.32 +
    3.33 +
    3.34 +(** Inverse of keys **)
    3.35 +
    3.36 +goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
    3.37 +by (Step_tac 1);
    3.38 +br box_equals 1;
    3.39 +by (REPEAT (rtac invKey 2));
    3.40 +by (Asm_simp_tac 1);
    3.41 +qed "invKey_eq";
    3.42 +
    3.43 +Addsimps [invKey, invKey_eq];
    3.44 +
    3.45 +
    3.46 +(**** keysFor operator ****)
    3.47 +
    3.48 +goalw thy [keysFor_def] "keysFor {} = {}";
    3.49 +by (Fast_tac 1);
    3.50 +qed "keysFor_empty";
    3.51 +
    3.52 +goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
    3.53 +by (Fast_tac 1);
    3.54 +qed "keysFor_Un";
    3.55 +
    3.56 +goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
    3.57 +by (Fast_tac 1);
    3.58 +qed "keysFor_UN";
    3.59 +
    3.60 +(*Monotonicity*)
    3.61 +goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
    3.62 +by (Fast_tac 1);
    3.63 +qed "keysFor_mono";
    3.64 +
    3.65 +goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    3.66 +by (fast_tac (!claset addss (!simpset)) 1);
    3.67 +qed "keysFor_insert_Agent";
    3.68 +
    3.69 +goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    3.70 +by (fast_tac (!claset addss (!simpset)) 1);
    3.71 +qed "keysFor_insert_Nonce";
    3.72 +
    3.73 +goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    3.74 +by (fast_tac (!claset addss (!simpset)) 1);
    3.75 +qed "keysFor_insert_Key";
    3.76 +
    3.77 +goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    3.78 +by (fast_tac (!claset addss (!simpset)) 1);
    3.79 +qed "keysFor_insert_MPair";
    3.80 +
    3.81 +goalw thy [keysFor_def]
    3.82 +    "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";
    3.83 +by (Auto_tac());
    3.84 +by (fast_tac (!claset addIs [image_eqI]) 1);
    3.85 +qed "keysFor_insert_Crypt";
    3.86 +
    3.87 +Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    3.88 +	  keysFor_insert_Agent, keysFor_insert_Nonce,
    3.89 +	  keysFor_insert_Key, keysFor_insert_MPair,
    3.90 +	  keysFor_insert_Crypt];
    3.91 +
    3.92 +
    3.93 +(**** Inductive relation "parts" ****)
    3.94 +
    3.95 +val major::prems = 
    3.96 +goal thy "[| {|X,Y|} : parts H;       \
    3.97 +\            [| X : parts H; Y : parts H |] ==> P  \
    3.98 +\         |] ==> P";
    3.99 +by (cut_facts_tac [major] 1);
   3.100 +brs prems 1;
   3.101 +by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
   3.102 +qed "MPair_parts";
   3.103 +
   3.104 +AddIs  [parts.Inj];
   3.105 +AddSEs [MPair_parts];
   3.106 +AddDs  [parts.Body];
   3.107 +
   3.108 +goal thy "H <= parts(H)";
   3.109 +by (Fast_tac 1);
   3.110 +qed "parts_increasing";
   3.111 +
   3.112 +(*Monotonicity*)
   3.113 +goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
   3.114 +by (rtac lfp_mono 1);
   3.115 +by (REPEAT (ares_tac basic_monos 1));
   3.116 +qed "parts_mono";
   3.117 +
   3.118 +goal thy "parts{} = {}";
   3.119 +by (Step_tac 1);
   3.120 +be parts.induct 1;
   3.121 +by (ALLGOALS Fast_tac);
   3.122 +qed "parts_empty";
   3.123 +Addsimps [parts_empty];
   3.124 +
   3.125 +goal thy "!!X. X: parts{} ==> P";
   3.126 +by (Asm_full_simp_tac 1);
   3.127 +qed "parts_emptyE";
   3.128 +AddSEs [parts_emptyE];
   3.129 +
   3.130 +
   3.131 +(** Unions **)
   3.132 +
   3.133 +goal thy "parts(G) Un parts(H) <= parts(G Un H)";
   3.134 +by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
   3.135 +val parts_Un_subset1 = result();
   3.136 +
   3.137 +goal thy "parts(G Un H) <= parts(G) Un parts(H)";
   3.138 +br subsetI 1;
   3.139 +be parts.induct 1;
   3.140 +by (ALLGOALS Fast_tac);
   3.141 +val parts_Un_subset2 = result();
   3.142 +
   3.143 +goal thy "parts(G Un H) = parts(G) Un parts(H)";
   3.144 +by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
   3.145 +qed "parts_Un";
   3.146 +
   3.147 +goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
   3.148 +by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
   3.149 +val parts_UN_subset1 = result();
   3.150 +
   3.151 +goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
   3.152 +br subsetI 1;
   3.153 +be parts.induct 1;
   3.154 +by (ALLGOALS Fast_tac);
   3.155 +val parts_UN_subset2 = result();
   3.156 +
   3.157 +goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
   3.158 +by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
   3.159 +qed "parts_UN";
   3.160 +
   3.161 +goal thy "parts(UN x. H x) = (UN x. parts(H x))";
   3.162 +by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
   3.163 +qed "parts_UN1";
   3.164 +
   3.165 +(*Added to simplify arguments to parts, analyze and synthesize*)
   3.166 +Addsimps [parts_Un, parts_UN, parts_UN1];
   3.167 +
   3.168 +goal thy "insert X (parts H) <= parts(insert X H)";
   3.169 +by (fast_tac (!claset addEs [imp_of_subset parts_mono]) 1);
   3.170 +qed "parts_insert_subset";
   3.171 +
   3.172 +(*Especially for reasoning about the Fake rule in traces*)
   3.173 +goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
   3.174 +br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;
   3.175 +by (Fast_tac 1);
   3.176 +qed "parts_insert_subset_Un";
   3.177 +
   3.178 +(** Idempotence and transitivity **)
   3.179 +
   3.180 +goal thy "!!H. X: parts (parts H) ==> X: parts H";
   3.181 +be parts.induct 1;
   3.182 +by (ALLGOALS Fast_tac);
   3.183 +qed "parts_partsE";
   3.184 +AddSEs [parts_partsE];
   3.185 +
   3.186 +goal thy "parts (parts H) = parts H";
   3.187 +by (Fast_tac 1);
   3.188 +qed "parts_idem";
   3.189 +Addsimps [parts_idem];
   3.190 +
   3.191 +goal thy "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
   3.192 +by (dtac parts_mono 1);
   3.193 +by (Fast_tac 1);
   3.194 +qed "parts_trans";
   3.195 +
   3.196 +(*Cut*)
   3.197 +goal thy "!!H. [| X: parts H;  Y: parts (insert X H) |] ==> Y: parts H";
   3.198 +be parts_trans 1;
   3.199 +by (Fast_tac 1);
   3.200 +qed "parts_cut";
   3.201 +
   3.202 +
   3.203 +(** Rewrite rules for pulling out atomic messages **)
   3.204 +
   3.205 +goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   3.206 +by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
   3.207 +br subsetI 1;
   3.208 +be parts.induct 1;
   3.209 +(*Simplification breaks up equalities between messages;
   3.210 +  how to make it work for fast_tac??*)
   3.211 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.212 +qed "parts_insert_Agent";
   3.213 +
   3.214 +goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
   3.215 +by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
   3.216 +br subsetI 1;
   3.217 +be parts.induct 1;
   3.218 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.219 +qed "parts_insert_Nonce";
   3.220 +
   3.221 +goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
   3.222 +by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
   3.223 +br subsetI 1;
   3.224 +be parts.induct 1;
   3.225 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.226 +qed "parts_insert_Key";
   3.227 +
   3.228 +goal thy "parts (insert (Crypt X K) H) = \
   3.229 +\         insert (Crypt X K) (parts (insert X H))";
   3.230 +br equalityI 1;
   3.231 +br subsetI 1;
   3.232 +be parts.induct 1;
   3.233 +by (Auto_tac());
   3.234 +be parts.induct 1;
   3.235 +by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
   3.236 +qed "parts_insert_Crypt";
   3.237 +
   3.238 +goal thy "parts (insert {|X,Y|} H) = \
   3.239 +\         insert {|X,Y|} (parts (insert X (insert Y H)))";
   3.240 +br equalityI 1;
   3.241 +br subsetI 1;
   3.242 +be parts.induct 1;
   3.243 +by (Auto_tac());
   3.244 +be parts.induct 1;
   3.245 +by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
   3.246 +qed "parts_insert_MPair";
   3.247 +
   3.248 +Addsimps [parts_insert_Agent, parts_insert_Nonce, 
   3.249 +	  parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
   3.250 +
   3.251 +
   3.252 +(**** Inductive relation "analyze" ****)
   3.253 +
   3.254 +val major::prems = 
   3.255 +goal thy "[| {|X,Y|} : analyze H;       \
   3.256 +\            [| X : analyze H; Y : analyze H |] ==> P  \
   3.257 +\         |] ==> P";
   3.258 +by (cut_facts_tac [major] 1);
   3.259 +brs prems 1;
   3.260 +by (REPEAT (eresolve_tac [asm_rl, analyze.Fst, analyze.Snd] 1));
   3.261 +qed "MPair_analyze";
   3.262 +
   3.263 +AddIs  [analyze.Inj];
   3.264 +AddSEs [MPair_analyze];
   3.265 +AddDs  [analyze.Decrypt];
   3.266 +
   3.267 +goal thy "H <= analyze(H)";
   3.268 +by (Fast_tac 1);
   3.269 +qed "analyze_increasing";
   3.270 +
   3.271 +goal thy "analyze H <= parts H";
   3.272 +by (rtac subsetI 1);
   3.273 +be analyze.induct 1;
   3.274 +by (ALLGOALS Fast_tac);
   3.275 +qed "analyze_subset_parts";
   3.276 +
   3.277 +bind_thm ("not_parts_not_analyze", analyze_subset_parts RS contra_subsetD);
   3.278 +
   3.279 +
   3.280 +goal thy "parts (analyze H) = parts H";
   3.281 +br equalityI 1;
   3.282 +br (analyze_subset_parts RS parts_mono RS subset_trans) 1;
   3.283 +by (Simp_tac 1);
   3.284 +by (fast_tac (!claset addDs [analyze_increasing RS parts_mono RS subsetD]) 1);
   3.285 +qed "parts_analyze";
   3.286 +Addsimps [parts_analyze];
   3.287 +
   3.288 +(*Monotonicity; Lemma 1 of Lowe*)
   3.289 +goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";
   3.290 +by (rtac lfp_mono 1);
   3.291 +by (REPEAT (ares_tac basic_monos 1));
   3.292 +qed "analyze_mono";
   3.293 +
   3.294 +(** General equational properties **)
   3.295 +
   3.296 +goal thy "analyze{} = {}";
   3.297 +by (Step_tac 1);
   3.298 +be analyze.induct 1;
   3.299 +by (ALLGOALS Fast_tac);
   3.300 +qed "analyze_empty";
   3.301 +Addsimps [analyze_empty];
   3.302 +
   3.303 +(*Converse fails: we can analyze more from the union than from the 
   3.304 +  separate parts, as a key in one might decrypt a message in the other*)
   3.305 +goal thy "analyze(G) Un analyze(H) <= analyze(G Un H)";
   3.306 +by (REPEAT (ares_tac [Un_least, analyze_mono, Un_upper1, Un_upper2] 1));
   3.307 +qed "analyze_Un";
   3.308 +
   3.309 +goal thy "insert X (analyze H) <= analyze(insert X H)";
   3.310 +by (fast_tac (!claset addEs [imp_of_subset analyze_mono]) 1);
   3.311 +qed "analyze_insert";
   3.312 +
   3.313 +(** Rewrite rules for pulling out atomic messages **)
   3.314 +
   3.315 +goal thy "analyze (insert (Agent agt) H) = insert (Agent agt) (analyze H)";
   3.316 +by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.317 +br subsetI 1;
   3.318 +be analyze.induct 1;
   3.319 +(*Simplification breaks up equalities between messages;
   3.320 +  how to make it work for fast_tac??*)
   3.321 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.322 +qed "analyze_insert_Agent";
   3.323 +
   3.324 +goal thy "analyze (insert (Nonce N) H) = insert (Nonce N) (analyze H)";
   3.325 +by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.326 +br subsetI 1;
   3.327 +be analyze.induct 1;
   3.328 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.329 +qed "analyze_insert_Nonce";
   3.330 +
   3.331 +(*Can only pull out Keys if they are not needed to decrypt the rest*)
   3.332 +goalw thy [keysFor_def]
   3.333 +    "!!K. K ~: keysFor (analyze H) ==>  \
   3.334 +\         analyze (insert (Key K) H) = insert (Key K) (analyze H)";
   3.335 +by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.336 +br subsetI 1;
   3.337 +be analyze.induct 1;
   3.338 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.339 +qed "analyze_insert_Key";
   3.340 +
   3.341 +goal thy "!!H. Key (invKey K) ~: analyze H ==>  \
   3.342 +\              analyze (insert (Crypt X K) H) = \
   3.343 +\              insert (Crypt X K) (analyze H)";
   3.344 +by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.345 +br subsetI 1;
   3.346 +be analyze.induct 1;
   3.347 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.348 +qed "analyze_insert_Crypt";
   3.349 +
   3.350 +goal thy "!!H. Key (invKey K) : analyze H ==>  \
   3.351 +\              analyze (insert (Crypt X K) H) <= \
   3.352 +\              insert (Crypt X K) (analyze (insert X H))";
   3.353 +br subsetI 1;
   3.354 +by (eres_inst_tac [("za","x")] analyze.induct 1);
   3.355 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.356 +val lemma1 = result();
   3.357 +
   3.358 +goal thy "!!H. Key (invKey K) : analyze H ==>  \
   3.359 +\              insert (Crypt X K) (analyze (insert X H)) <= \
   3.360 +\              analyze (insert (Crypt X K) H)";
   3.361 +by (Auto_tac());
   3.362 +by (eres_inst_tac [("za","x")] analyze.induct 1);
   3.363 +by (Auto_tac());
   3.364 +by (best_tac (!claset addIs [subset_insertI RS analyze_mono RS subsetD,
   3.365 +			     analyze.Decrypt]) 1);
   3.366 +val lemma2 = result();
   3.367 +
   3.368 +goal thy "!!H. Key (invKey K) : analyze H ==>  \
   3.369 +\              analyze (insert (Crypt X K) H) = \
   3.370 +\              insert (Crypt X K) (analyze (insert X H))";
   3.371 +by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
   3.372 +qed "analyze_insert_Decrypt";
   3.373 +
   3.374 +Addsimps [analyze_insert_Agent, analyze_insert_Nonce, 
   3.375 +	  analyze_insert_Key, analyze_insert_Crypt,
   3.376 +	  analyze_insert_Decrypt];
   3.377 +
   3.378 +
   3.379 +(*This rule supposes "for the sake of argument" that we have the key.*)
   3.380 +goal thy  "analyze (insert (Crypt X K) H) <=  \
   3.381 +\         insert (Crypt X K) (analyze (insert X H))";
   3.382 +br subsetI 1;
   3.383 +be analyze.induct 1;
   3.384 +by (Auto_tac());
   3.385 +qed "analyze_insert_Crypt_subset";
   3.386 +
   3.387 +
   3.388 +(** Rewrite rules for pulling out atomic parts of messages **)
   3.389 +
   3.390 +goal thy "analyze (insert X H) <= analyze (insert {|X,Y|} H)";
   3.391 +br subsetI 1;
   3.392 +be analyze.induct 1;
   3.393 +by (ALLGOALS (best_tac (!claset addIs [analyze.Fst]))); 
   3.394 +qed "analyze_insert_subset_MPair1";
   3.395 +
   3.396 +goal thy "analyze (insert Y H) <= analyze (insert {|X,Y|} H)";
   3.397 +br subsetI 1;
   3.398 +be analyze.induct 1;
   3.399 +by (ALLGOALS (best_tac (!claset addIs [analyze.Snd]))); 
   3.400 +qed "analyze_insert_subset_MPair2";
   3.401 +
   3.402 +goal thy "analyze (insert {|Agent agt,Y|} H) = \
   3.403 +\         insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))";
   3.404 +by (rtac equalityI 1);
   3.405 +by (best_tac (!claset addIs [analyze.Fst,
   3.406 +			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
   3.407 +br subsetI 1;
   3.408 +be analyze.induct 1;
   3.409 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.410 +qed "analyze_insert_Agent_MPair";
   3.411 +
   3.412 +goal thy "analyze (insert {|Nonce N,Y|} H) = \
   3.413 +\         insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))";
   3.414 +by (rtac equalityI 1);
   3.415 +by (best_tac (!claset addIs [analyze.Fst,
   3.416 +			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
   3.417 +br subsetI 1;
   3.418 +be analyze.induct 1;
   3.419 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.420 +qed "analyze_insert_Nonce_MPair";
   3.421 +
   3.422 +(*Can only pull out Keys if they are not needed to decrypt the rest*)
   3.423 +goalw thy [keysFor_def]
   3.424 +    "!!K. K ~: keysFor (analyze (insert Y H)) ==>  \
   3.425 +\         analyze (insert {|Key K, Y|} H) = \
   3.426 +\         insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))";
   3.427 +by (rtac equalityI 1);
   3.428 +by (best_tac (!claset addIs [analyze.Fst,
   3.429 +			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
   3.430 +br subsetI 1;
   3.431 +be analyze.induct 1;
   3.432 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.433 +qed "analyze_insert_Key_MPair";
   3.434 +
   3.435 +Addsimps [analyze_insert_Agent_MPair, analyze_insert_Nonce_MPair,
   3.436 +	  analyze_insert_Key_MPair];
   3.437 +
   3.438 +(** Idempotence and transitivity **)
   3.439 +
   3.440 +goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";
   3.441 +be analyze.induct 1;
   3.442 +by (ALLGOALS Fast_tac);
   3.443 +qed "analyze_analyzeE";
   3.444 +AddSEs [analyze_analyzeE];
   3.445 +
   3.446 +goal thy "analyze (analyze H) = analyze H";
   3.447 +by (Fast_tac 1);
   3.448 +qed "analyze_idem";
   3.449 +Addsimps [analyze_idem];
   3.450 +
   3.451 +goal thy "!!H. [| X: analyze G;  G <= analyze H |] ==> X: analyze H";
   3.452 +by (dtac analyze_mono 1);
   3.453 +by (Fast_tac 1);
   3.454 +qed "analyze_trans";
   3.455 +
   3.456 +(*Cut; Lemma 2 of Lowe*)
   3.457 +goal thy "!!H. [| X: analyze H;  Y: analyze (insert X H) |] ==> Y: analyze H";
   3.458 +be analyze_trans 1;
   3.459 +by (Fast_tac 1);
   3.460 +qed "analyze_cut";
   3.461 +
   3.462 +(*Cut can be proved easily by induction on
   3.463 +   "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H"
   3.464 +*)
   3.465 +
   3.466 +(*If there are no pairs or encryptions then analyze does nothing*)
   3.467 +goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
   3.468 +\         analyze H = H";
   3.469 +by (Step_tac 1);
   3.470 +be analyze.induct 1;
   3.471 +by (ALLGOALS Fast_tac);
   3.472 +qed "analyze_trivial";
   3.473 +
   3.474 +(*Helps to prove Fake cases*)
   3.475 +goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)";
   3.476 +be analyze.induct 1;
   3.477 +by (ALLGOALS (fast_tac (!claset addEs [imp_of_subset analyze_mono])));
   3.478 +val lemma = result();
   3.479 +
   3.480 +goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";
   3.481 +by (fast_tac (!claset addIs [lemma]
   3.482 +		      addEs [imp_of_subset analyze_mono]) 1);
   3.483 +qed "analyze_UN_analyze";
   3.484 +Addsimps [analyze_UN_analyze];
   3.485 +
   3.486 +
   3.487 +(**** Inductive relation "synthesize" ****)
   3.488 +
   3.489 +AddIs  synthesize.intrs;
   3.490 +
   3.491 +goal thy "H <= synthesize(H)";
   3.492 +by (Fast_tac 1);
   3.493 +qed "synthesize_increasing";
   3.494 +
   3.495 +(*Monotonicity*)
   3.496 +goalw thy synthesize.defs "!!G H. G<=H ==> synthesize(G) <= synthesize(H)";
   3.497 +by (rtac lfp_mono 1);
   3.498 +by (REPEAT (ares_tac basic_monos 1));
   3.499 +qed "synthesize_mono";
   3.500 +
   3.501 +(** Unions **)
   3.502 +
   3.503 +(*Converse fails: we can synthesize more from the union than from the 
   3.504 +  separate parts, building a compound message using elements of each.*)
   3.505 +goal thy "synthesize(G) Un synthesize(H) <= synthesize(G Un H)";
   3.506 +by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));
   3.507 +qed "synthesize_Un";
   3.508 +
   3.509 +(** Idempotence and transitivity **)
   3.510 +
   3.511 +goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";
   3.512 +be synthesize.induct 1;
   3.513 +by (ALLGOALS Fast_tac);
   3.514 +qed "synthesize_synthesizeE";
   3.515 +AddSEs [synthesize_synthesizeE];
   3.516 +
   3.517 +goal thy "synthesize (synthesize H) = synthesize H";
   3.518 +by (Fast_tac 1);
   3.519 +qed "synthesize_idem";
   3.520 +
   3.521 +goal thy "!!H. [| X: synthesize G;  G <= synthesize H |] ==> X: synthesize H";
   3.522 +by (dtac synthesize_mono 1);
   3.523 +by (Fast_tac 1);
   3.524 +qed "synthesize_trans";
   3.525 +
   3.526 +(*Cut; Lemma 2 of Lowe*)
   3.527 +goal thy "!!H. [| X: synthesize H;  Y: synthesize (insert X H) \
   3.528 +\              |] ==> Y: synthesize H";
   3.529 +be synthesize_trans 1;
   3.530 +by (Fast_tac 1);
   3.531 +qed "synthesize_cut";
   3.532 +
   3.533 +
   3.534 +(*Can only produce a nonce or key if it is already known,
   3.535 +  but can synthesize a pair or encryption from its components...*)
   3.536 +val mk_cases = synthesize.mk_cases msg.simps;
   3.537 +
   3.538 +val Nonce_synthesize = mk_cases "Nonce n : synthesize H";
   3.539 +val Key_synthesize   = mk_cases "Key K : synthesize H";
   3.540 +val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H";
   3.541 +val Crypt_synthesize = mk_cases "Crypt X K : synthesize H";
   3.542 +
   3.543 +AddSEs [Nonce_synthesize, Key_synthesize, MPair_synthesize, Crypt_synthesize];
   3.544 +
   3.545 +goal thy "(Nonce N : synthesize H) = (Nonce N : H)";
   3.546 +by (Fast_tac 1);
   3.547 +qed "Nonce_synthesize_eq";
   3.548 +
   3.549 +goal thy "(Key K : synthesize H) = (Key K : H)";
   3.550 +by (Fast_tac 1);
   3.551 +qed "Key_synthesize_eq";
   3.552 +
   3.553 +Addsimps [Nonce_synthesize_eq, Key_synthesize_eq];
   3.554 +
   3.555 +
   3.556 +goalw thy [keysFor_def]
   3.557 +    "keysFor (synthesize H) = keysFor H Un invKey``{K. Key K : H}";
   3.558 +by (Fast_tac 1);
   3.559 +qed "keysFor_synthesize";
   3.560 +Addsimps [keysFor_synthesize];
   3.561 +
   3.562 +
   3.563 +(*** Combinations of parts, analyze and synthesize ***)
   3.564 +
   3.565 +(*Not that useful, in view of the following one...*)
   3.566 +goal thy "parts (synthesize H) <= synthesize (parts H)";
   3.567 +by (Step_tac 1);
   3.568 +be parts.induct 1;
   3.569 +be (parts_increasing RS synthesize_mono RS subsetD) 1;
   3.570 +by (ALLGOALS Fast_tac);
   3.571 +qed "parts_synthesize_subset";
   3.572 +
   3.573 +goal thy "parts (synthesize H) = parts H Un synthesize H";
   3.574 +br equalityI 1;
   3.575 +br subsetI 1;
   3.576 +be parts.induct 1;
   3.577 +by (ALLGOALS
   3.578 +    (best_tac (!claset addIs ((synthesize_increasing RS parts_mono RS subsetD)
   3.579 +			     ::parts.intrs))));
   3.580 +qed "parts_synthesize";
   3.581 +Addsimps [parts_synthesize];
   3.582 +
   3.583 +goal thy "analyze (synthesize H) = analyze H Un synthesize H";
   3.584 +br equalityI 1;
   3.585 +br subsetI 1;
   3.586 +be analyze.induct 1;
   3.587 +by (best_tac
   3.588 +    (!claset addIs [synthesize_increasing RS analyze_mono RS subsetD]) 5);
   3.589 +(*Strange that best_tac just can't hack this one...*)
   3.590 +by (ALLGOALS (deepen_tac (!claset addIs analyze.intrs) 0));
   3.591 +qed "analyze_synthesize";
   3.592 +Addsimps [analyze_synthesize];
   3.593 +
   3.594 +(*Hard to prove; still needed now that there's only one Enemy?*)
   3.595 +goal thy "analyze (UN i. synthesize (H i)) = \
   3.596 +\         analyze (UN i. H i) Un (UN i. synthesize (H i))";
   3.597 +br equalityI 1;
   3.598 +br subsetI 1;
   3.599 +be analyze.induct 1;
   3.600 +by (best_tac
   3.601 +    (!claset addEs [imp_of_subset synthesize_increasing,
   3.602 +		    imp_of_subset analyze_mono]) 5);
   3.603 +by (Best_tac 1);
   3.604 +by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);
   3.605 +by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);
   3.606 +by (deepen_tac (!claset addSEs [analyze.Decrypt]
   3.607 +			addIs  [analyze.Decrypt]) 0 1);
   3.608 +qed "analyze_UN1_synthesize";
   3.609 +Addsimps [analyze_UN1_synthesize];
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/Message.thy	Fri Jun 28 15:26:39 1996 +0200
     4.3 @@ -0,0 +1,114 @@
     4.4 +(*  Title:      HOL/Auth/Message
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1996  University of Cambridge
     4.8 +
     4.9 +Datatypes of agents and messages;
    4.10 +Inductive relations "parts", "analyze" and "synthesize"
    4.11 +*)
    4.12 +
    4.13 +Message = Arith +
    4.14 +
    4.15 +(*Is there a difference between a nonce and arbitrary numerical data?
    4.16 +  Do we need a type of nonces?*)
    4.17 +
    4.18 +types 
    4.19 +  key = nat
    4.20 +
    4.21 +consts
    4.22 +  invKey :: key=>key
    4.23 +
    4.24 +rules
    4.25 +  invKey "invKey (invKey K) = K"
    4.26 +
    4.27 +  (*The inverse of a symmetric key is itself;
    4.28 +    that of a public key is the private key and vice versa*)
    4.29 +
    4.30 +constdefs
    4.31 +  isSymKey :: key=>bool
    4.32 +  "isSymKey K == (invKey K = K)"
    4.33 +
    4.34 +  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
    4.35 +    because Crypt is a constructor!  We assume that encryption is injective,
    4.36 +    which is not true in the real world.  The alternative is to take
    4.37 +    Crypt as an uninterpreted function symbol satisfying the equation
    4.38 +    above.  This seems to require moving to ZF and regarding msg as an
    4.39 +    inductive definition instead of a datatype.*) 
    4.40 +
    4.41 +datatype  (*We allow any number of friendly agents*)
    4.42 +  agent = Server | Friend nat | Enemy
    4.43 +
    4.44 +consts  
    4.45 +  isEnemy :: agent => bool
    4.46 +
    4.47 +primrec isEnemy agent
    4.48 +  isEnemy_Server  "isEnemy Server  = False"
    4.49 +  isEnemy_Friend  "isEnemy (Friend i) = False"
    4.50 +  isEnemy_Enemy   "isEnemy Enemy = True"
    4.51 +
    4.52 +datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
    4.53 +  msg = Agent agent
    4.54 +      | Nonce nat
    4.55 +      | Key   key
    4.56 +      | MPair msg msg
    4.57 +      | Crypt msg key
    4.58 +
    4.59 +(*Allows messages of the form {|A,B,NA|}, etc...*)
    4.60 +syntax
    4.61 +  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
    4.62 +
    4.63 +translations
    4.64 +  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    4.65 +  "{|x, y|}"      == "MPair x y"
    4.66 +
    4.67 +
    4.68 +constdefs  (*Keys useful to decrypt elements of a message set*)
    4.69 +  keysFor :: msg set => key set
    4.70 +  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
    4.71 +
    4.72 +(** Inductive definition of all "parts" of a message.  **)
    4.73 +
    4.74 +consts  parts   :: msg set => msg set
    4.75 +inductive "parts H"
    4.76 +  intrs 
    4.77 +    Inj     "X: H ==> X: parts H"
    4.78 +    Fst     "{|X,Y|} : parts H ==> X : parts H"
    4.79 +    Snd     "{|X,Y|} : parts H ==> Y : parts H"
    4.80 +    Body    "Crypt X K : parts H ==> X : parts H"
    4.81 +
    4.82 +
    4.83 +(** Inductive definition of "analyze" -- what can be broken down from a set of
    4.84 +    messages, including keys.  A form of downward closure.  Pairs can
    4.85 +    be taken apart; messages decrypted with known keys.  **)
    4.86 +
    4.87 +consts  analyze   :: msg set => msg set
    4.88 +inductive "analyze H"
    4.89 +  intrs 
    4.90 +    Inj     "X: H ==> X: analyze H"
    4.91 +
    4.92 +    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
    4.93 +
    4.94 +    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
    4.95 +
    4.96 +    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
    4.97 +             |] ==> X : analyze H"
    4.98 +
    4.99 +
   4.100 +(** Inductive definition of "synthesize" -- what can be built up from a set of
   4.101 +    messages.  A form of upward closure.  Pairs can be built, messages
   4.102 +    encrypted with known keys.  Agent names may be quoted.  **)
   4.103 +
   4.104 +consts  synthesize   :: msg set => msg set
   4.105 +inductive "synthesize H"
   4.106 +  intrs 
   4.107 +    Inj     "X: H ==> X: synthesize H"
   4.108 +
   4.109 +    Agent   "Agent agt : synthesize H"
   4.110 +
   4.111 +    MPair   "[| X: synthesize H;  Y: synthesize H
   4.112 +             |] ==> {|X,Y|} : synthesize H"
   4.113 +
   4.114 +    Crypt   "[| X: synthesize H; Key(K): synthesize H
   4.115 +             |] ==> Crypt X K : synthesize H"
   4.116 +
   4.117 +end