1.1 --- a/src/HOL/Auth/Event.thy Fri Mar 02 13:14:37 2001 +0100
1.2 +++ b/src/HOL/Auth/Event.thy Fri Mar 02 13:18:31 2001 +0100
1.3 @@ -14,12 +14,6 @@
1.4 theory Event = Message
1.5 files ("Event_lemmas.ML"):
1.6
1.7 -(*from Message.ML*)
1.8 -method_setup spy_analz = {*
1.9 - Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
1.10 - "for proving the Fake case when analz is involved"
1.11 -
1.12 -
1.13 consts (*Initial states of agents -- parameter of the construction*)
1.14 initState :: "agent => msg set"
1.15
2.1 --- a/src/HOL/Auth/Event_lemmas.ML Fri Mar 02 13:14:37 2001 +0100
2.2 +++ b/src/HOL/Auth/Event_lemmas.ML Fri Mar 02 13:18:31 2001 +0100
2.3 @@ -1,4 +1,4 @@
2.4 -(* Title: HOL/Auth/Event
2.5 +(* Title: HOL/Auth/Event_lemmas
2.6 ID: $Id$
2.7 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.8 Copyright 1996 University of Cambridge
2.9 @@ -20,8 +20,7 @@
2.10 = parts {X} Un parts (knows Spy evs) -- since general case loops*)
2.11
2.12 bind_thm ("parts_insert_knows_Spy",
2.13 - parts_insert |>
2.14 - read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
2.15 + inst "H" "knows Spy evs" parts_insert);
2.16
2.17
2.18 val expand_event_case = thm "event.split";
3.1 --- a/src/HOL/Auth/Message.ML Fri Mar 02 13:14:37 2001 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,912 +0,0 @@
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", "analz" and "synth"
3.11 -*)
3.12 -
3.13 -
3.14 -(*Eliminates a commonly-occurring expression*)
3.15 -goal HOL.thy "~ (ALL x. x~=y)";
3.16 -by (Blast_tac 1);
3.17 -Addsimps [result()];
3.18 -
3.19 -AddIffs msg.inject;
3.20 -
3.21 -(*Equations hold because constructors are injective; cannot prove for all f*)
3.22 -Goal "(Friend x : Friend`A) = (x:A)";
3.23 -by Auto_tac;
3.24 -qed "Friend_image_eq";
3.25 -
3.26 -Goal "(Key x : Key`A) = (x:A)";
3.27 -by Auto_tac;
3.28 -qed "Key_image_eq";
3.29 -
3.30 -Goal "(Nonce x ~: Key`A)";
3.31 -by Auto_tac;
3.32 -qed "Nonce_Key_image_eq";
3.33 -Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
3.34 -
3.35 -
3.36 -(** Inverse of keys **)
3.37 -
3.38 -Goal "(invKey K = invKey K') = (K=K')";
3.39 -by Safe_tac;
3.40 -by (rtac box_equals 1);
3.41 -by (REPEAT (rtac invKey 2));
3.42 -by (Asm_simp_tac 1);
3.43 -qed "invKey_eq";
3.44 -
3.45 -Addsimps [invKey, invKey_eq];
3.46 -
3.47 -
3.48 -(**** keysFor operator ****)
3.49 -
3.50 -Goalw [keysFor_def] "keysFor {} = {}";
3.51 -by (Blast_tac 1);
3.52 -qed "keysFor_empty";
3.53 -
3.54 -Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
3.55 -by (Blast_tac 1);
3.56 -qed "keysFor_Un";
3.57 -
3.58 -Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
3.59 -by (Blast_tac 1);
3.60 -qed "keysFor_UN";
3.61 -
3.62 -(*Monotonicity*)
3.63 -Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)";
3.64 -by (Blast_tac 1);
3.65 -qed "keysFor_mono";
3.66 -
3.67 -Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
3.68 -by Auto_tac;
3.69 -qed "keysFor_insert_Agent";
3.70 -
3.71 -Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
3.72 -by Auto_tac;
3.73 -qed "keysFor_insert_Nonce";
3.74 -
3.75 -Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
3.76 -by Auto_tac;
3.77 -qed "keysFor_insert_Number";
3.78 -
3.79 -Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
3.80 -by Auto_tac;
3.81 -qed "keysFor_insert_Key";
3.82 -
3.83 -Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
3.84 -by Auto_tac;
3.85 -qed "keysFor_insert_Hash";
3.86 -
3.87 -Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
3.88 -by Auto_tac;
3.89 -qed "keysFor_insert_MPair";
3.90 -
3.91 -Goalw [keysFor_def]
3.92 - "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
3.93 -by Auto_tac;
3.94 -qed "keysFor_insert_Crypt";
3.95 -
3.96 -Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
3.97 - keysFor_insert_Agent, keysFor_insert_Nonce,
3.98 - keysFor_insert_Number, keysFor_insert_Key,
3.99 - keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
3.100 -AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
3.101 - keysFor_UN RS equalityD1 RS subsetD RS UN_E];
3.102 -
3.103 -Goalw [keysFor_def] "keysFor (Key`E) = {}";
3.104 -by Auto_tac;
3.105 -qed "keysFor_image_Key";
3.106 -Addsimps [keysFor_image_Key];
3.107 -
3.108 -Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H";
3.109 -by (Blast_tac 1);
3.110 -qed "Crypt_imp_invKey_keysFor";
3.111 -
3.112 -
3.113 -(**** Inductive relation "parts" ****)
3.114 -
3.115 -val major::prems =
3.116 -Goal "[| {|X,Y|} : parts H; \
3.117 -\ [| X : parts H; Y : parts H |] ==> P \
3.118 -\ |] ==> P";
3.119 -by (cut_facts_tac [major] 1);
3.120 -by (resolve_tac prems 1);
3.121 -by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
3.122 -qed "MPair_parts";
3.123 -
3.124 -AddIs [parts.Inj];
3.125 -
3.126 -AddSEs [MPair_parts, make_elim parts.Body];
3.127 -(*NB These two rules are UNSAFE in the formal sense, as they discard the
3.128 - compound message. They work well on THIS FILE.
3.129 - MPair_parts is left as SAFE because it speeds up proofs.
3.130 - The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*)
3.131 -
3.132 -Goal "H <= parts(H)";
3.133 -by (Blast_tac 1);
3.134 -qed "parts_increasing";
3.135 -
3.136 -(*Monotonicity*)
3.137 -Goalw parts.defs "G<=H ==> parts(G) <= parts(H)";
3.138 -by (rtac lfp_mono 1);
3.139 -by (REPEAT (ares_tac basic_monos 1));
3.140 -qed "parts_mono";
3.141 -
3.142 -val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
3.143 -
3.144 -Goal "parts{} = {}";
3.145 -by Safe_tac;
3.146 -by (etac parts.induct 1);
3.147 -by (ALLGOALS Blast_tac);
3.148 -qed "parts_empty";
3.149 -Addsimps [parts_empty];
3.150 -
3.151 -Goal "X: parts{} ==> P";
3.152 -by (Asm_full_simp_tac 1);
3.153 -qed "parts_emptyE";
3.154 -AddSEs [parts_emptyE];
3.155 -
3.156 -(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
3.157 -Goal "X: parts H ==> EX Y:H. X: parts {Y}";
3.158 -by (etac parts.induct 1);
3.159 -by (ALLGOALS Blast_tac);
3.160 -qed "parts_singleton";
3.161 -
3.162 -
3.163 -(** Unions **)
3.164 -
3.165 -Goal "parts(G) Un parts(H) <= parts(G Un H)";
3.166 -by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
3.167 -val parts_Un_subset1 = result();
3.168 -
3.169 -Goal "parts(G Un H) <= parts(G) Un parts(H)";
3.170 -by (rtac subsetI 1);
3.171 -by (etac parts.induct 1);
3.172 -by (ALLGOALS Blast_tac);
3.173 -val parts_Un_subset2 = result();
3.174 -
3.175 -Goal "parts(G Un H) = parts(G) Un parts(H)";
3.176 -by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
3.177 -qed "parts_Un";
3.178 -
3.179 -Goal "parts (insert X H) = parts {X} Un parts H";
3.180 -by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
3.181 -by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
3.182 -qed "parts_insert";
3.183 -
3.184 -(*TWO inserts to avoid looping. This rewrite is better than nothing.
3.185 - Not suitable for Addsimps: its behaviour can be strange.*)
3.186 -Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
3.187 -by (simp_tac (simpset() addsimps [Un_assoc]) 1);
3.188 -by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
3.189 -qed "parts_insert2";
3.190 -
3.191 -Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
3.192 -by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
3.193 -val parts_UN_subset1 = result();
3.194 -
3.195 -Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
3.196 -by (rtac subsetI 1);
3.197 -by (etac parts.induct 1);
3.198 -by (ALLGOALS Blast_tac);
3.199 -val parts_UN_subset2 = result();
3.200 -
3.201 -Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))";
3.202 -by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
3.203 -qed "parts_UN";
3.204 -
3.205 -(*Added to simplify arguments to parts, analz and synth.
3.206 - NOTE: the UN versions are no longer used!*)
3.207 -Addsimps [parts_Un, parts_UN];
3.208 -AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
3.209 - parts_UN RS equalityD1 RS subsetD RS UN_E];
3.210 -
3.211 -Goal "insert X (parts H) <= parts(insert X H)";
3.212 -by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
3.213 -qed "parts_insert_subset";
3.214 -
3.215 -(** Idempotence and transitivity **)
3.216 -
3.217 -Goal "X: parts (parts H) ==> X: parts H";
3.218 -by (etac parts.induct 1);
3.219 -by (ALLGOALS Blast_tac);
3.220 -qed "parts_partsD";
3.221 -AddSDs [parts_partsD];
3.222 -
3.223 -Goal "parts (parts H) = parts H";
3.224 -by (Blast_tac 1);
3.225 -qed "parts_idem";
3.226 -Addsimps [parts_idem];
3.227 -
3.228 -Goal "[| X: parts G; G <= parts H |] ==> X: parts H";
3.229 -by (dtac parts_mono 1);
3.230 -by (Blast_tac 1);
3.231 -qed "parts_trans";
3.232 -
3.233 -(*Cut*)
3.234 -Goal "[| Y: parts (insert X G); X: parts H |] \
3.235 -\ ==> Y: parts (G Un H)";
3.236 -by (etac parts_trans 1);
3.237 -by Auto_tac;
3.238 -qed "parts_cut";
3.239 -
3.240 -Goal "X: parts H ==> parts (insert X H) = parts H";
3.241 -by (fast_tac (claset() addSDs [parts_cut]
3.242 - addIs [parts_insertI]
3.243 - addss (simpset())) 1);
3.244 -qed "parts_cut_eq";
3.245 -
3.246 -Addsimps [parts_cut_eq];
3.247 -
3.248 -
3.249 -(** Rewrite rules for pulling out atomic messages **)
3.250 -
3.251 -fun parts_tac i =
3.252 - EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
3.253 - etac parts.induct i,
3.254 - Auto_tac];
3.255 -
3.256 -Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
3.257 -by (parts_tac 1);
3.258 -qed "parts_insert_Agent";
3.259 -
3.260 -Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
3.261 -by (parts_tac 1);
3.262 -qed "parts_insert_Nonce";
3.263 -
3.264 -Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
3.265 -by (parts_tac 1);
3.266 -qed "parts_insert_Number";
3.267 -
3.268 -Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
3.269 -by (parts_tac 1);
3.270 -qed "parts_insert_Key";
3.271 -
3.272 -Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
3.273 -by (parts_tac 1);
3.274 -qed "parts_insert_Hash";
3.275 -
3.276 -Goal "parts (insert (Crypt K X) H) = \
3.277 -\ insert (Crypt K X) (parts (insert X H))";
3.278 -by (rtac equalityI 1);
3.279 -by (rtac subsetI 1);
3.280 -by (etac parts.induct 1);
3.281 -by Auto_tac;
3.282 -by (etac parts.induct 1);
3.283 -by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
3.284 -qed "parts_insert_Crypt";
3.285 -
3.286 -Goal "parts (insert {|X,Y|} H) = \
3.287 -\ insert {|X,Y|} (parts (insert X (insert Y H)))";
3.288 -by (rtac equalityI 1);
3.289 -by (rtac subsetI 1);
3.290 -by (etac parts.induct 1);
3.291 -by Auto_tac;
3.292 -by (etac parts.induct 1);
3.293 -by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
3.294 -qed "parts_insert_MPair";
3.295 -
3.296 -Addsimps [parts_insert_Agent, parts_insert_Nonce,
3.297 - parts_insert_Number, parts_insert_Key,
3.298 - parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
3.299 -
3.300 -
3.301 -Goal "parts (Key`N) = Key`N";
3.302 -by Auto_tac;
3.303 -by (etac parts.induct 1);
3.304 -by Auto_tac;
3.305 -qed "parts_image_Key";
3.306 -Addsimps [parts_image_Key];
3.307 -
3.308 -
3.309 -(*In any message, there is an upper bound N on its greatest nonce.*)
3.310 -Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
3.311 -by (induct_tac "msg" 1);
3.312 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
3.313 -(*MPair case: blast_tac works out the necessary sum itself!*)
3.314 -by (blast_tac (claset() addSEs [add_leE]) 2);
3.315 -(*Nonce case*)
3.316 -by (res_inst_tac [("x","N + Suc nat")] exI 1);
3.317 -by (auto_tac (claset() addSEs [add_leE], simpset()));
3.318 -qed "msg_Nonce_supply";
3.319 -
3.320 -
3.321 -(**** Inductive relation "analz" ****)
3.322 -
3.323 -val major::prems =
3.324 -Goal "[| {|X,Y|} : analz H; \
3.325 -\ [| X : analz H; Y : analz H |] ==> P \
3.326 -\ |] ==> P";
3.327 -by (cut_facts_tac [major] 1);
3.328 -by (resolve_tac prems 1);
3.329 -by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
3.330 -qed "MPair_analz";
3.331 -
3.332 -AddSEs [MPair_analz]; (*Making it safe speeds up proofs*)
3.333 -AddDs [analz.Decrypt]; (*Unsafe: we don't want to split up certificates!*)
3.334 -AddIs [analz.Inj];
3.335 -
3.336 -Addsimps [analz.Inj];
3.337 -
3.338 -Goal "H <= analz(H)";
3.339 -by (Blast_tac 1);
3.340 -qed "analz_increasing";
3.341 -
3.342 -Goal "analz H <= parts H";
3.343 -by (rtac subsetI 1);
3.344 -by (etac analz.induct 1);
3.345 -by (ALLGOALS Blast_tac);
3.346 -qed "analz_subset_parts";
3.347 -
3.348 -bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
3.349 -
3.350 -
3.351 -Goal "parts (analz H) = parts H";
3.352 -by (rtac equalityI 1);
3.353 -by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
3.354 -by (Simp_tac 1);
3.355 -by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1);
3.356 -qed "parts_analz";
3.357 -Addsimps [parts_analz];
3.358 -
3.359 -Goal "analz (parts H) = parts H";
3.360 -by Auto_tac;
3.361 -by (etac analz.induct 1);
3.362 -by Auto_tac;
3.363 -qed "analz_parts";
3.364 -Addsimps [analz_parts];
3.365 -
3.366 -(*Monotonicity; Lemma 1 of Lowe*)
3.367 -Goalw analz.defs "G<=H ==> analz(G) <= analz(H)";
3.368 -by (rtac lfp_mono 1);
3.369 -by (REPEAT (ares_tac basic_monos 1));
3.370 -qed "analz_mono";
3.371 -
3.372 -bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono));
3.373 -
3.374 -(** General equational properties **)
3.375 -
3.376 -Goal "analz{} = {}";
3.377 -by Safe_tac;
3.378 -by (etac analz.induct 1);
3.379 -by (ALLGOALS Blast_tac);
3.380 -qed "analz_empty";
3.381 -Addsimps [analz_empty];
3.382 -
3.383 -(*Converse fails: we can analz more from the union than from the
3.384 - separate parts, as a key in one might decrypt a message in the other*)
3.385 -Goal "analz(G) Un analz(H) <= analz(G Un H)";
3.386 -by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
3.387 -qed "analz_Un";
3.388 -
3.389 -Goal "insert X (analz H) <= analz(insert X H)";
3.390 -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
3.391 -qed "analz_insert";
3.392 -
3.393 -(** Rewrite rules for pulling out atomic messages **)
3.394 -
3.395 -fun analz_tac i =
3.396 - EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
3.397 - etac analz.induct i,
3.398 - Auto_tac];
3.399 -
3.400 -Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
3.401 -by (analz_tac 1);
3.402 -qed "analz_insert_Agent";
3.403 -
3.404 -Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
3.405 -by (analz_tac 1);
3.406 -qed "analz_insert_Nonce";
3.407 -
3.408 -Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
3.409 -by (analz_tac 1);
3.410 -qed "analz_insert_Number";
3.411 -
3.412 -Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
3.413 -by (analz_tac 1);
3.414 -qed "analz_insert_Hash";
3.415 -
3.416 -(*Can only pull out Keys if they are not needed to decrypt the rest*)
3.417 -Goalw [keysFor_def]
3.418 - "K ~: keysFor (analz H) ==> \
3.419 -\ analz (insert (Key K) H) = insert (Key K) (analz H)";
3.420 -by (analz_tac 1);
3.421 -qed "analz_insert_Key";
3.422 -
3.423 -Goal "analz (insert {|X,Y|} H) = \
3.424 -\ insert {|X,Y|} (analz (insert X (insert Y H)))";
3.425 -by (rtac equalityI 1);
3.426 -by (rtac subsetI 1);
3.427 -by (etac analz.induct 1);
3.428 -by Auto_tac;
3.429 -by (etac analz.induct 1);
3.430 -by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
3.431 -qed "analz_insert_MPair";
3.432 -
3.433 -(*Can pull out enCrypted message if the Key is not known*)
3.434 -Goal "Key (invKey K) ~: analz H ==> \
3.435 -\ analz (insert (Crypt K X) H) = \
3.436 -\ insert (Crypt K X) (analz H)";
3.437 -by (analz_tac 1);
3.438 -qed "analz_insert_Crypt";
3.439 -
3.440 -Goal "Key (invKey K) : analz H ==> \
3.441 -\ analz (insert (Crypt K X) H) <= \
3.442 -\ insert (Crypt K X) (analz (insert X H))";
3.443 -by (rtac subsetI 1);
3.444 -by (eres_inst_tac [("xa","x")] analz.induct 1);
3.445 -by Auto_tac;
3.446 -val lemma1 = result();
3.447 -
3.448 -Goal "Key (invKey K) : analz H ==> \
3.449 -\ insert (Crypt K X) (analz (insert X H)) <= \
3.450 -\ analz (insert (Crypt K X) H)";
3.451 -by Auto_tac;
3.452 -by (eres_inst_tac [("xa","x")] analz.induct 1);
3.453 -by Auto_tac;
3.454 -by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
3.455 -val lemma2 = result();
3.456 -
3.457 -Goal "Key (invKey K) : analz H ==> \
3.458 -\ analz (insert (Crypt K X) H) = \
3.459 -\ insert (Crypt K X) (analz (insert X H))";
3.460 -by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
3.461 -qed "analz_insert_Decrypt";
3.462 -
3.463 -(*Case analysis: either the message is secure, or it is not!
3.464 - Effective, but can cause subgoals to blow up!
3.465 - Use with split_if; apparently split_tac does not cope with patterns
3.466 - such as "analz (insert (Crypt K X) H)" *)
3.467 -Goal "analz (insert (Crypt K X) H) = \
3.468 -\ (if (Key (invKey K) : analz H) \
3.469 -\ then insert (Crypt K X) (analz (insert X H)) \
3.470 -\ else insert (Crypt K X) (analz H))";
3.471 -by (case_tac "Key (invKey K) : analz H " 1);
3.472 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt,
3.473 - analz_insert_Decrypt])));
3.474 -qed "analz_Crypt_if";
3.475 -
3.476 -Addsimps [analz_insert_Agent, analz_insert_Nonce,
3.477 - analz_insert_Number, analz_insert_Key,
3.478 - analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
3.479 -
3.480 -(*This rule supposes "for the sake of argument" that we have the key.*)
3.481 -Goal "analz (insert (Crypt K X) H) <= \
3.482 -\ insert (Crypt K X) (analz (insert X H))";
3.483 -by (rtac subsetI 1);
3.484 -by (etac analz.induct 1);
3.485 -by Auto_tac;
3.486 -qed "analz_insert_Crypt_subset";
3.487 -
3.488 -
3.489 -Goal "analz (Key`N) = Key`N";
3.490 -by Auto_tac;
3.491 -by (etac analz.induct 1);
3.492 -by Auto_tac;
3.493 -qed "analz_image_Key";
3.494 -
3.495 -Addsimps [analz_image_Key];
3.496 -
3.497 -
3.498 -(** Idempotence and transitivity **)
3.499 -
3.500 -Goal "X: analz (analz H) ==> X: analz H";
3.501 -by (etac analz.induct 1);
3.502 -by (ALLGOALS Blast_tac);
3.503 -qed "analz_analzD";
3.504 -AddSDs [analz_analzD];
3.505 -
3.506 -Goal "analz (analz H) = analz H";
3.507 -by (Blast_tac 1);
3.508 -qed "analz_idem";
3.509 -Addsimps [analz_idem];
3.510 -
3.511 -Goal "[| X: analz G; G <= analz H |] ==> X: analz H";
3.512 -by (dtac analz_mono 1);
3.513 -by (Blast_tac 1);
3.514 -qed "analz_trans";
3.515 -
3.516 -(*Cut; Lemma 2 of Lowe*)
3.517 -Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
3.518 -by (etac analz_trans 1);
3.519 -by (Blast_tac 1);
3.520 -qed "analz_cut";
3.521 -
3.522 -(*Cut can be proved easily by induction on
3.523 - "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
3.524 -*)
3.525 -
3.526 -(*This rewrite rule helps in the simplification of messages that involve
3.527 - the forwarding of unknown components (X). Without it, removing occurrences
3.528 - of X can be very complicated. *)
3.529 -Goal "X: analz H ==> analz (insert X H) = analz H";
3.530 -by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
3.531 -qed "analz_insert_eq";
3.532 -
3.533 -
3.534 -(** A congruence rule for "analz" **)
3.535 -
3.536 -Goal "[| analz G <= analz G'; analz H <= analz H' \
3.537 -\ |] ==> analz (G Un H) <= analz (G' Un H')";
3.538 -by (Clarify_tac 1);
3.539 -by (etac analz.induct 1);
3.540 -by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
3.541 -qed "analz_subset_cong";
3.542 -
3.543 -Goal "[| analz G = analz G'; analz H = analz H' \
3.544 -\ |] ==> analz (G Un H) = analz (G' Un H')";
3.545 -by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
3.546 - ORELSE' etac equalityE));
3.547 -qed "analz_cong";
3.548 -
3.549 -
3.550 -Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
3.551 -by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
3.552 - setloop (rtac analz_cong)) 1);
3.553 -qed "analz_insert_cong";
3.554 -
3.555 -(*If there are no pairs or encryptions then analz does nothing*)
3.556 -Goal "[| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \
3.557 -\ analz H = H";
3.558 -by Safe_tac;
3.559 -by (etac analz.induct 1);
3.560 -by (ALLGOALS Blast_tac);
3.561 -qed "analz_trivial";
3.562 -
3.563 -(*These two are obsolete (with a single Spy) but cost little to prove...*)
3.564 -Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
3.565 -by (etac analz.induct 1);
3.566 -by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
3.567 -val lemma = result();
3.568 -
3.569 -Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
3.570 -by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
3.571 -qed "analz_UN_analz";
3.572 -Addsimps [analz_UN_analz];
3.573 -
3.574 -
3.575 -(**** Inductive relation "synth" ****)
3.576 -
3.577 -AddIs synth.intrs;
3.578 -
3.579 -(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*)
3.580 -val Nonce_synth = synth.mk_cases "Nonce n : synth H";
3.581 -val Key_synth = synth.mk_cases "Key K : synth H";
3.582 -val Hash_synth = synth.mk_cases "Hash X : synth H";
3.583 -val MPair_synth = synth.mk_cases "{|X,Y|} : synth H";
3.584 -val Crypt_synth = synth.mk_cases "Crypt K X : synth H";
3.585 -
3.586 -AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
3.587 -
3.588 -Goal "H <= synth(H)";
3.589 -by (Blast_tac 1);
3.590 -qed "synth_increasing";
3.591 -
3.592 -(*Monotonicity*)
3.593 -Goalw synth.defs "G<=H ==> synth(G) <= synth(H)";
3.594 -by (rtac lfp_mono 1);
3.595 -by (REPEAT (ares_tac basic_monos 1));
3.596 -qed "synth_mono";
3.597 -
3.598 -(** Unions **)
3.599 -
3.600 -(*Converse fails: we can synth more from the union than from the
3.601 - separate parts, building a compound message using elements of each.*)
3.602 -Goal "synth(G) Un synth(H) <= synth(G Un H)";
3.603 -by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
3.604 -qed "synth_Un";
3.605 -
3.606 -Goal "insert X (synth H) <= synth(insert X H)";
3.607 -by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
3.608 -qed "synth_insert";
3.609 -
3.610 -(** Idempotence and transitivity **)
3.611 -
3.612 -Goal "X: synth (synth H) ==> X: synth H";
3.613 -by (etac synth.induct 1);
3.614 -by (ALLGOALS Blast_tac);
3.615 -qed "synth_synthD";
3.616 -AddSDs [synth_synthD];
3.617 -
3.618 -Goal "synth (synth H) = synth H";
3.619 -by (Blast_tac 1);
3.620 -qed "synth_idem";
3.621 -
3.622 -Goal "[| X: synth G; G <= synth H |] ==> X: synth H";
3.623 -by (dtac synth_mono 1);
3.624 -by (Blast_tac 1);
3.625 -qed "synth_trans";
3.626 -
3.627 -(*Cut; Lemma 2 of Lowe*)
3.628 -Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
3.629 -by (etac synth_trans 1);
3.630 -by (Blast_tac 1);
3.631 -qed "synth_cut";
3.632 -
3.633 -Goal "Agent A : synth H";
3.634 -by (Blast_tac 1);
3.635 -qed "Agent_synth";
3.636 -
3.637 -Goal "Number n : synth H";
3.638 -by (Blast_tac 1);
3.639 -qed "Number_synth";
3.640 -
3.641 -Goal "(Nonce N : synth H) = (Nonce N : H)";
3.642 -by (Blast_tac 1);
3.643 -qed "Nonce_synth_eq";
3.644 -
3.645 -Goal "(Key K : synth H) = (Key K : H)";
3.646 -by (Blast_tac 1);
3.647 -qed "Key_synth_eq";
3.648 -
3.649 -Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
3.650 -by (Blast_tac 1);
3.651 -qed "Crypt_synth_eq";
3.652 -
3.653 -Addsimps [Agent_synth, Number_synth,
3.654 - Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
3.655 -
3.656 -
3.657 -Goalw [keysFor_def]
3.658 - "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}";
3.659 -by (Blast_tac 1);
3.660 -qed "keysFor_synth";
3.661 -Addsimps [keysFor_synth];
3.662 -
3.663 -
3.664 -(*** Combinations of parts, analz and synth ***)
3.665 -
3.666 -Goal "parts (synth H) = parts H Un synth H";
3.667 -by (rtac equalityI 1);
3.668 -by (rtac subsetI 1);
3.669 -by (etac parts.induct 1);
3.670 -by (ALLGOALS
3.671 - (blast_tac (claset() addIs ((synth_increasing RS parts_mono RS subsetD)
3.672 - ::parts.intrs))));
3.673 -qed "parts_synth";
3.674 -Addsimps [parts_synth];
3.675 -
3.676 -Goal "analz (analz G Un H) = analz (G Un H)";
3.677 -by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
3.678 -by (ALLGOALS Simp_tac);
3.679 -qed "analz_analz_Un";
3.680 -
3.681 -Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
3.682 -by (rtac equalityI 1);
3.683 -by (rtac subsetI 1);
3.684 -by (etac analz.induct 1);
3.685 -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5);
3.686 -by (ALLGOALS (blast_tac (claset() addIs analz.intrs)));
3.687 -qed "analz_synth_Un";
3.688 -
3.689 -Goal "analz (synth H) = analz H Un synth H";
3.690 -by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
3.691 -by (Full_simp_tac 1);
3.692 -qed "analz_synth";
3.693 -Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
3.694 -
3.695 -
3.696 -(** For reasoning about the Fake rule in traces **)
3.697 -
3.698 -Goal "X: G ==> parts(insert X H) <= parts G Un parts H";
3.699 -by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
3.700 -by (Blast_tac 1);
3.701 -qed "parts_insert_subset_Un";
3.702 -
3.703 -(*More specifically for Fake. Very occasionally we could do with a version
3.704 - of the form parts{X} <= synth (analz H) Un parts H *)
3.705 -Goal "X: synth (analz H) ==> \
3.706 -\ parts (insert X H) <= synth (analz H) Un parts H";
3.707 -by (dtac parts_insert_subset_Un 1);
3.708 -by (Full_simp_tac 1);
3.709 -by (Blast_tac 1);
3.710 -qed "Fake_parts_insert";
3.711 -
3.712 -(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
3.713 -Goal "X: synth (analz G) ==> \
3.714 -\ analz (insert X H) <= synth (analz G) Un analz (G Un H)";
3.715 -by (rtac subsetI 1);
3.716 -by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
3.717 -by (blast_tac (claset() addIs [impOfSubs analz_mono,
3.718 - impOfSubs (analz_mono RS synth_mono)]) 2);
3.719 -by (Full_simp_tac 1);
3.720 -by (Blast_tac 1);
3.721 -qed "Fake_analz_insert";
3.722 -
3.723 -Goal "(X: analz H & X: parts H) = (X: analz H)";
3.724 -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
3.725 -val analz_conj_parts = result();
3.726 -
3.727 -Goal "(X: analz H | X: parts H) = (X: parts H)";
3.728 -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
3.729 -val analz_disj_parts = result();
3.730 -
3.731 -AddIffs [analz_conj_parts, analz_disj_parts];
3.732 -
3.733 -(*Without this equation, other rules for synth and analz would yield
3.734 - redundant cases*)
3.735 -Goal "({|X,Y|} : synth (analz H)) = \
3.736 -\ (X : synth (analz H) & Y : synth (analz H))";
3.737 -by (Blast_tac 1);
3.738 -qed "MPair_synth_analz";
3.739 -
3.740 -AddIffs [MPair_synth_analz];
3.741 -
3.742 -Goal "[| Key K : analz H; Key (invKey K) : analz H |] \
3.743 -\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
3.744 -by (Blast_tac 1);
3.745 -qed "Crypt_synth_analz";
3.746 -
3.747 -
3.748 -Goal "X ~: synth (analz H) \
3.749 -\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
3.750 -by (Blast_tac 1);
3.751 -qed "Hash_synth_analz";
3.752 -Addsimps [Hash_synth_analz];
3.753 -
3.754 -
3.755 -(**** HPair: a combination of Hash and MPair ****)
3.756 -
3.757 -(*** Freeness ***)
3.758 -
3.759 -Goalw [HPair_def] "Agent A ~= Hash[X] Y";
3.760 -by (Simp_tac 1);
3.761 -qed "Agent_neq_HPair";
3.762 -
3.763 -Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
3.764 -by (Simp_tac 1);
3.765 -qed "Nonce_neq_HPair";
3.766 -
3.767 -Goalw [HPair_def] "Number N ~= Hash[X] Y";
3.768 -by (Simp_tac 1);
3.769 -qed "Number_neq_HPair";
3.770 -
3.771 -Goalw [HPair_def] "Key K ~= Hash[X] Y";
3.772 -by (Simp_tac 1);
3.773 -qed "Key_neq_HPair";
3.774 -
3.775 -Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
3.776 -by (Simp_tac 1);
3.777 -qed "Hash_neq_HPair";
3.778 -
3.779 -Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
3.780 -by (Simp_tac 1);
3.781 -qed "Crypt_neq_HPair";
3.782 -
3.783 -val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair,
3.784 - Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
3.785 -
3.786 -AddIffs HPair_neqs;
3.787 -AddIffs (HPair_neqs RL [not_sym]);
3.788 -
3.789 -Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
3.790 -by (Simp_tac 1);
3.791 -qed "HPair_eq";
3.792 -
3.793 -Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
3.794 -by (Simp_tac 1);
3.795 -qed "MPair_eq_HPair";
3.796 -
3.797 -Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
3.798 -by Auto_tac;
3.799 -qed "HPair_eq_MPair";
3.800 -
3.801 -AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
3.802 -
3.803 -
3.804 -(*** Specialized laws, proved in terms of those for Hash and MPair ***)
3.805 -
3.806 -Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
3.807 -by (Simp_tac 1);
3.808 -qed "keysFor_insert_HPair";
3.809 -
3.810 -Goalw [HPair_def]
3.811 - "parts (insert (Hash[X] Y) H) = \
3.812 -\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
3.813 -by (Simp_tac 1);
3.814 -qed "parts_insert_HPair";
3.815 -
3.816 -Goalw [HPair_def]
3.817 - "analz (insert (Hash[X] Y) H) = \
3.818 -\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
3.819 -by (Simp_tac 1);
3.820 -qed "analz_insert_HPair";
3.821 -
3.822 -Goalw [HPair_def] "X ~: synth (analz H) \
3.823 -\ ==> (Hash[X] Y : synth (analz H)) = \
3.824 -\ (Hash {|X, Y|} : analz H & Y : synth (analz H))";
3.825 -by (Simp_tac 1);
3.826 -by (Blast_tac 1);
3.827 -qed "HPair_synth_analz";
3.828 -
3.829 -Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair,
3.830 - HPair_synth_analz, HPair_synth_analz];
3.831 -
3.832 -
3.833 -(*We do NOT want Crypt... messages broken up in protocols!!*)
3.834 -Delrules [make_elim parts.Body];
3.835 -
3.836 -
3.837 -(** Rewrites to push in Key and Crypt messages, so that other messages can
3.838 - be pulled out using the analz_insert rules **)
3.839 -
3.840 -fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)]
3.841 - insert_commute;
3.842 -
3.843 -val pushKeys = map (insComm thy "Key ?K")
3.844 - ["Agent ?C", "Nonce ?N", "Number ?N",
3.845 - "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
3.846 -
3.847 -val pushCrypts = map (insComm thy "Crypt ?X ?K")
3.848 - ["Agent ?C", "Nonce ?N", "Number ?N",
3.849 - "Hash ?X'", "MPair ?X' ?Y"];
3.850 -
3.851 -(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
3.852 -bind_thms ("pushes", pushKeys@pushCrypts);
3.853 -
3.854 -
3.855 -(*** Tactics useful for many protocol proofs ***)
3.856 -
3.857 -(*Prove base case (subgoal i) and simplify others. A typical base case
3.858 - concerns Crypt K X ~: Key`shrK`bad and cannot be proved by rewriting
3.859 - alone.*)
3.860 -fun prove_simple_subgoals_tac i =
3.861 - force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
3.862 - ALLGOALS Asm_simp_tac;
3.863 -
3.864 -fun Fake_parts_insert_tac i =
3.865 - blast_tac (claset() addIs [parts_insertI]
3.866 - addDs [impOfSubs analz_subset_parts,
3.867 - impOfSubs Fake_parts_insert]) i;
3.868 -
3.869 -(*Apply rules to break down assumptions of the form
3.870 - Y : parts(insert X H) and Y : analz(insert X H)
3.871 -*)
3.872 -val Fake_insert_tac =
3.873 - dresolve_tac [impOfSubs Fake_analz_insert,
3.874 - impOfSubs Fake_parts_insert] THEN'
3.875 - eresolve_tac [asm_rl, synth.Inj];
3.876 -
3.877 -fun Fake_insert_simp_tac i =
3.878 - REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i;
3.879 -
3.880 -
3.881 -(*Analysis of Fake cases. Also works for messages that forward unknown parts,
3.882 - but this application is no longer necessary if analz_insert_eq is used.
3.883 - Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
3.884 - DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
3.885 -
3.886 -val atomic_spy_analz_tac = SELECT_GOAL
3.887 - (Fake_insert_simp_tac 1
3.888 - THEN
3.889 - IF_UNSOLVED (Blast.depth_tac
3.890 - (claset() addIs [analz_insertI,
3.891 - impOfSubs analz_subset_parts]) 4 1));
3.892 -
3.893 -fun spy_analz_tac i =
3.894 - DETERM
3.895 - (SELECT_GOAL
3.896 - (EVERY
3.897 - [ (*push in occurrences of X...*)
3.898 - (REPEAT o CHANGED)
3.899 - (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
3.900 - (*...allowing further simplifications*)
3.901 - Simp_tac 1,
3.902 - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
3.903 - DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
3.904 -
3.905 -
3.906 -(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
3.907 -goal Set.thy "A Un (B Un A) = B Un A";
3.908 -by (Blast_tac 1);
3.909 -val Un_absorb3 = result();
3.910 -Addsimps [Un_absorb3];
3.911 -
3.912 -(*By default only o_apply is built-in. But in the presence of eta-expansion
3.913 - this means that some terms displayed as (f o g) will be rewritten, and others
3.914 - will not!*)
3.915 -Addsimps [o_def];
4.1 --- a/src/HOL/Auth/Message.thy Fri Mar 02 13:14:37 2001 +0100
4.2 +++ b/src/HOL/Auth/Message.thy Fri Mar 02 13:18:31 2001 +0100
4.3 @@ -7,22 +7,31 @@
4.4 Inductive relations "parts", "analz" and "synth"
4.5 *)
4.6
4.7 -Message = Main +
4.8 +theory Message = Main
4.9 +files ("Message_lemmas.ML"):
4.10 +
4.11 +(*Eliminates a commonly-occurring expression*)
4.12 +lemma [simp] : "~ (ALL x. x~=y)"
4.13 +by blast
4.14 +
4.15 +(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
4.16 +lemma [simp] : "A Un (B Un A) = B Un A"
4.17 +by blast
4.18
4.19 types
4.20 key = nat
4.21
4.22 consts
4.23 - invKey :: key=>key
4.24 + invKey :: "key=>key"
4.25
4.26 -rules
4.27 - invKey "invKey (invKey K) = K"
4.28 +axioms
4.29 + invKey [simp] : "invKey (invKey K) = K"
4.30
4.31 (*The inverse of a symmetric key is itself;
4.32 that of a public key is the private key and vice versa*)
4.33
4.34 constdefs
4.35 - isSymKey :: key=>bool
4.36 + isSymKey :: "key=>bool"
4.37 "isSymKey K == (invKey K = K)"
4.38
4.39 datatype (*We allow any number of friendly agents*)
4.40 @@ -43,7 +52,7 @@
4.41 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
4.42
4.43 syntax (xsymbols)
4.44 - "@MTuple" :: "['a, args] => 'a * 'b" ("(2\\<lbrace>_,/ _\\<rbrace>)")
4.45 + "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
4.46
4.47 translations
4.48 "{|x, y, z|}" == "{|x, {|y, z|}|}"
4.49 @@ -52,50 +61,86 @@
4.50
4.51 constdefs
4.52 (*Message Y, paired with a MAC computed with the help of X*)
4.53 - HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000])
4.54 + HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000])
4.55 "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
4.56
4.57 (*Keys useful to decrypt elements of a message set*)
4.58 - keysFor :: msg set => key set
4.59 + keysFor :: "msg set => key set"
4.60 "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
4.61
4.62 (** Inductive definition of all "parts" of a message. **)
4.63
4.64 -consts parts :: msg set => msg set
4.65 +consts parts :: "msg set => msg set"
4.66 inductive "parts H"
4.67 - intrs
4.68 - Inj "X: H ==> X: parts H"
4.69 - Fst "{|X,Y|} : parts H ==> X : parts H"
4.70 - Snd "{|X,Y|} : parts H ==> Y : parts H"
4.71 - Body "Crypt K X : parts H ==> X : parts H"
4.72 + intros
4.73 + Inj [intro] : "X: H ==> X : parts H"
4.74 + Fst: "{|X,Y|} : parts H ==> X : parts H"
4.75 + Snd: "{|X,Y|} : parts H ==> Y : parts H"
4.76 + Body: "Crypt K X : parts H ==> X : parts H"
4.77 +
4.78 +
4.79 +(*Monotonicity*)
4.80 +lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
4.81 +apply auto
4.82 +apply (erule parts.induct)
4.83 +apply (auto dest: Fst Snd Body)
4.84 +done
4.85
4.86
4.87 (** Inductive definition of "analz" -- what can be broken down from a set of
4.88 messages, including keys. A form of downward closure. Pairs can
4.89 be taken apart; messages decrypted with known keys. **)
4.90
4.91 -consts analz :: msg set => msg set
4.92 +consts analz :: "msg set => msg set"
4.93 inductive "analz H"
4.94 - intrs
4.95 - Inj "X: H ==> X: analz H"
4.96 - Fst "{|X,Y|} : analz H ==> X : analz H"
4.97 - Snd "{|X,Y|} : analz H ==> Y : analz H"
4.98 - Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
4.99 + intros
4.100 + Inj [intro,simp] : "X: H ==> X: analz H"
4.101 + Fst: "{|X,Y|} : analz H ==> X : analz H"
4.102 + Snd: "{|X,Y|} : analz H ==> Y : analz H"
4.103 + Decrypt [dest]:
4.104 + "[|Crypt K X : analz H; Key(invKey K): analz H|] ==> X : analz H"
4.105
4.106
4.107 +(*Monotonicity; Lemma 1 of Lowe's paper*)
4.108 +lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
4.109 +apply auto
4.110 +apply (erule analz.induct)
4.111 +apply (auto dest: Fst Snd)
4.112 +done
4.113 +
4.114 (** Inductive definition of "synth" -- what can be built up from a set of
4.115 messages. A form of upward closure. Pairs can be built, messages
4.116 encrypted with known keys. Agent names are public domain.
4.117 Numbers can be guessed, but Nonces cannot be. **)
4.118
4.119 -consts synth :: msg set => msg set
4.120 +consts synth :: "msg set => msg set"
4.121 inductive "synth H"
4.122 - intrs
4.123 - Inj "X: H ==> X: synth H"
4.124 - Agent "Agent agt : synth H"
4.125 - Number "Number n : synth H"
4.126 - Hash "X: synth H ==> Hash X : synth H"
4.127 - MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H"
4.128 - Crypt "[| X: synth H; Key(K) : H |] ==> Crypt K X : synth H"
4.129 + intros
4.130 + Inj [intro]: "X: H ==> X: synth H"
4.131 + Agent [intro]: "Agent agt : synth H"
4.132 + Number [intro]: "Number n : synth H"
4.133 + Hash [intro]: "X: synth H ==> Hash X : synth H"
4.134 + MPair [intro]: "[|X: synth H; Y: synth H|] ==> {|X,Y|} : synth H"
4.135 + Crypt [intro]: "[|X: synth H; Key(K) : H|] ==> Crypt K X : synth H"
4.136 +
4.137 +(*Monotonicity*)
4.138 +lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
4.139 +apply auto
4.140 +apply (erule synth.induct)
4.141 +apply (auto dest: Fst Snd Body)
4.142 +done
4.143 +
4.144 +(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*)
4.145 +inductive_cases Nonce_synth [elim!]: "Nonce n : synth H"
4.146 +inductive_cases Key_synth [elim!]: "Key K : synth H"
4.147 +inductive_cases Hash_synth [elim!]: "Hash X : synth H"
4.148 +inductive_cases MPair_synth [elim!]: "{|X,Y|} : synth H"
4.149 +inductive_cases Crypt_synth [elim!]: "Crypt K X : synth H"
4.150 +
4.151 +use "Message_lemmas.ML"
4.152 +
4.153 +method_setup spy_analz = {*
4.154 + Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
4.155 + "for proving the Fake case when analz is involved"
4.156
4.157 end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Auth/Message_lemmas.ML Fri Mar 02 13:18:31 2001 +0100
5.3 @@ -0,0 +1,900 @@
5.4 +(* Title: HOL/Auth/Message
5.5 + ID: $Id$
5.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5.7 + Copyright 1996 University of Cambridge
5.8 +
5.9 +Datatypes of agents and messages;
5.10 +Inductive relations "parts", "analz" and "synth"
5.11 +*)
5.12 +
5.13 +(*ML bindings for definitions and axioms*)
5.14 +val invKey = thm "invKey";
5.15 +val keysFor_def = thm "keysFor_def";
5.16 +val parts_mono = thm "parts_mono";
5.17 +val analz_mono = thm "analz_mono";
5.18 +val synth_mono = thm "synth_mono";
5.19 +val HPair_def = thm "HPair_def";
5.20 +val isSymKey_def = thm "isSymKey_def";
5.21 +
5.22 +structure parts =
5.23 + struct
5.24 + val induct = thm "parts.induct";
5.25 + val Inj = thm "parts.Inj";
5.26 + val Fst = thm "parts.Fst";
5.27 + val Snd = thm "parts.Snd";
5.28 + val Body = thm "parts.Body";
5.29 + end;
5.30 +
5.31 +structure analz =
5.32 + struct
5.33 + val induct = thm "analz.induct";
5.34 + val Inj = thm "analz.Inj";
5.35 + val Fst = thm "analz.Fst";
5.36 + val Snd = thm "analz.Snd";
5.37 + val Decrypt = thm "analz.Decrypt";
5.38 + end;
5.39 +
5.40 +structure synth =
5.41 + struct
5.42 + val induct = thm "synth.induct";
5.43 + val Inj = thm "synth.Inj";
5.44 + val Agent = thm "synth.Agent";
5.45 + val Number = thm "synth.Number";
5.46 + val Hash = thm "synth.Hash";
5.47 + val Crypt = thm "synth.Crypt";
5.48 + end;
5.49 +
5.50 +
5.51 +(*Equations hold because constructors are injective; cannot prove for all f*)
5.52 +Goal "(Friend x : Friend`A) = (x:A)";
5.53 +by Auto_tac;
5.54 +qed "Friend_image_eq";
5.55 +
5.56 +Goal "(Key x : Key`A) = (x:A)";
5.57 +by Auto_tac;
5.58 +qed "Key_image_eq";
5.59 +
5.60 +Goal "(Nonce x ~: Key`A)";
5.61 +by Auto_tac;
5.62 +qed "Nonce_Key_image_eq";
5.63 +Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
5.64 +
5.65 +
5.66 +(** Inverse of keys **)
5.67 +
5.68 +Goal "(invKey K = invKey K') = (K=K')";
5.69 +by Safe_tac;
5.70 +by (rtac box_equals 1);
5.71 +by (REPEAT (rtac invKey 2));
5.72 +by (Asm_simp_tac 1);
5.73 +qed "invKey_eq";
5.74 +
5.75 +Addsimps [invKey_eq];
5.76 +
5.77 +
5.78 +(**** keysFor operator ****)
5.79 +
5.80 +Goalw [keysFor_def] "keysFor {} = {}";
5.81 +by (Blast_tac 1);
5.82 +qed "keysFor_empty";
5.83 +
5.84 +Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
5.85 +by (Blast_tac 1);
5.86 +qed "keysFor_Un";
5.87 +
5.88 +Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
5.89 +by (Blast_tac 1);
5.90 +qed "keysFor_UN";
5.91 +
5.92 +(*Monotonicity*)
5.93 +Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)";
5.94 +by (Blast_tac 1);
5.95 +qed "keysFor_mono";
5.96 +
5.97 +Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
5.98 +by Auto_tac;
5.99 +qed "keysFor_insert_Agent";
5.100 +
5.101 +Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
5.102 +by Auto_tac;
5.103 +qed "keysFor_insert_Nonce";
5.104 +
5.105 +Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
5.106 +by Auto_tac;
5.107 +qed "keysFor_insert_Number";
5.108 +
5.109 +Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
5.110 +by Auto_tac;
5.111 +qed "keysFor_insert_Key";
5.112 +
5.113 +Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
5.114 +by Auto_tac;
5.115 +qed "keysFor_insert_Hash";
5.116 +
5.117 +Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
5.118 +by Auto_tac;
5.119 +qed "keysFor_insert_MPair";
5.120 +
5.121 +Goalw [keysFor_def]
5.122 + "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
5.123 +by Auto_tac;
5.124 +qed "keysFor_insert_Crypt";
5.125 +
5.126 +Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
5.127 + keysFor_insert_Agent, keysFor_insert_Nonce,
5.128 + keysFor_insert_Number, keysFor_insert_Key,
5.129 + keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
5.130 +AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
5.131 + keysFor_UN RS equalityD1 RS subsetD RS UN_E];
5.132 +
5.133 +Goalw [keysFor_def] "keysFor (Key`E) = {}";
5.134 +by Auto_tac;
5.135 +qed "keysFor_image_Key";
5.136 +Addsimps [keysFor_image_Key];
5.137 +
5.138 +Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H";
5.139 +by (Blast_tac 1);
5.140 +qed "Crypt_imp_invKey_keysFor";
5.141 +
5.142 +
5.143 +(**** Inductive relation "parts" ****)
5.144 +
5.145 +val major::prems =
5.146 +Goal "[| {|X,Y|} : parts H; \
5.147 +\ [| X : parts H; Y : parts H |] ==> P \
5.148 +\ |] ==> P";
5.149 +by (cut_facts_tac [major] 1);
5.150 +by (resolve_tac prems 1);
5.151 +by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
5.152 +qed "MPair_parts";
5.153 +
5.154 +AddSEs [MPair_parts, make_elim parts.Body];
5.155 +(*NB These two rules are UNSAFE in the formal sense, as they discard the
5.156 + compound message. They work well on THIS FILE.
5.157 + MPair_parts is left as SAFE because it speeds up proofs.
5.158 + The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*)
5.159 +
5.160 +Goal "H <= parts(H)";
5.161 +by (Blast_tac 1);
5.162 +qed "parts_increasing";
5.163 +
5.164 +val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
5.165 +
5.166 +Goal "parts{} = {}";
5.167 +by Safe_tac;
5.168 +by (etac parts.induct 1);
5.169 +by (ALLGOALS Blast_tac);
5.170 +qed "parts_empty";
5.171 +Addsimps [parts_empty];
5.172 +
5.173 +Goal "X: parts{} ==> P";
5.174 +by (Asm_full_simp_tac 1);
5.175 +qed "parts_emptyE";
5.176 +AddSEs [parts_emptyE];
5.177 +
5.178 +(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
5.179 +Goal "X: parts H ==> EX Y:H. X: parts {Y}";
5.180 +by (etac parts.induct 1);
5.181 +by (ALLGOALS Blast_tac);
5.182 +qed "parts_singleton";
5.183 +
5.184 +
5.185 +(** Unions **)
5.186 +
5.187 +Goal "parts(G) Un parts(H) <= parts(G Un H)";
5.188 +by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
5.189 +val parts_Un_subset1 = result();
5.190 +
5.191 +Goal "parts(G Un H) <= parts(G) Un parts(H)";
5.192 +by (rtac subsetI 1);
5.193 +by (etac parts.induct 1);
5.194 +by (ALLGOALS Blast_tac);
5.195 +val parts_Un_subset2 = result();
5.196 +
5.197 +Goal "parts(G Un H) = parts(G) Un parts(H)";
5.198 +by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
5.199 +qed "parts_Un";
5.200 +
5.201 +Goal "parts (insert X H) = parts {X} Un parts H";
5.202 +by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
5.203 +by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
5.204 +qed "parts_insert";
5.205 +
5.206 +(*TWO inserts to avoid looping. This rewrite is better than nothing.
5.207 + Not suitable for Addsimps: its behaviour can be strange.*)
5.208 +Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
5.209 +by (simp_tac (simpset() addsimps [Un_assoc]) 1);
5.210 +by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
5.211 +qed "parts_insert2";
5.212 +
5.213 +Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
5.214 +by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
5.215 +val parts_UN_subset1 = result();
5.216 +
5.217 +Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
5.218 +by (rtac subsetI 1);
5.219 +by (etac parts.induct 1);
5.220 +by (ALLGOALS Blast_tac);
5.221 +val parts_UN_subset2 = result();
5.222 +
5.223 +Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))";
5.224 +by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
5.225 +qed "parts_UN";
5.226 +
5.227 +(*Added to simplify arguments to parts, analz and synth.
5.228 + NOTE: the UN versions are no longer used!*)
5.229 +Addsimps [parts_Un, parts_UN];
5.230 +AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
5.231 + parts_UN RS equalityD1 RS subsetD RS UN_E];
5.232 +
5.233 +Goal "insert X (parts H) <= parts(insert X H)";
5.234 +by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
5.235 +qed "parts_insert_subset";
5.236 +
5.237 +(** Idempotence and transitivity **)
5.238 +
5.239 +Goal "X: parts (parts H) ==> X: parts H";
5.240 +by (etac parts.induct 1);
5.241 +by (ALLGOALS Blast_tac);
5.242 +qed "parts_partsD";
5.243 +AddSDs [parts_partsD];
5.244 +
5.245 +Goal "parts (parts H) = parts H";
5.246 +by (Blast_tac 1);
5.247 +qed "parts_idem";
5.248 +Addsimps [parts_idem];
5.249 +
5.250 +Goal "[| X: parts G; G <= parts H |] ==> X: parts H";
5.251 +by (dtac parts_mono 1);
5.252 +by (Blast_tac 1);
5.253 +qed "parts_trans";
5.254 +
5.255 +(*Cut*)
5.256 +Goal "[| Y: parts (insert X G); X: parts H |] \
5.257 +\ ==> Y: parts (G Un H)";
5.258 +by (etac parts_trans 1);
5.259 +by Auto_tac;
5.260 +qed "parts_cut";
5.261 +
5.262 +Goal "X: parts H ==> parts (insert X H) = parts H";
5.263 +by (fast_tac (claset() addSDs [parts_cut]
5.264 + addIs [parts_insertI]
5.265 + addss (simpset())) 1);
5.266 +qed "parts_cut_eq";
5.267 +
5.268 +Addsimps [parts_cut_eq];
5.269 +
5.270 +
5.271 +(** Rewrite rules for pulling out atomic messages **)
5.272 +
5.273 +fun parts_tac i =
5.274 + EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
5.275 + etac parts.induct i,
5.276 + Auto_tac];
5.277 +
5.278 +Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
5.279 +by (parts_tac 1);
5.280 +qed "parts_insert_Agent";
5.281 +
5.282 +Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
5.283 +by (parts_tac 1);
5.284 +qed "parts_insert_Nonce";
5.285 +
5.286 +Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
5.287 +by (parts_tac 1);
5.288 +qed "parts_insert_Number";
5.289 +
5.290 +Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
5.291 +by (parts_tac 1);
5.292 +qed "parts_insert_Key";
5.293 +
5.294 +Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
5.295 +by (parts_tac 1);
5.296 +qed "parts_insert_Hash";
5.297 +
5.298 +Goal "parts (insert (Crypt K X) H) = \
5.299 +\ insert (Crypt K X) (parts (insert X H))";
5.300 +by (rtac equalityI 1);
5.301 +by (rtac subsetI 1);
5.302 +by (etac parts.induct 1);
5.303 +by Auto_tac;
5.304 +by (etac parts.induct 1);
5.305 +by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
5.306 +qed "parts_insert_Crypt";
5.307 +
5.308 +Goal "parts (insert {|X,Y|} H) = \
5.309 +\ insert {|X,Y|} (parts (insert X (insert Y H)))";
5.310 +by (rtac equalityI 1);
5.311 +by (rtac subsetI 1);
5.312 +by (etac parts.induct 1);
5.313 +by Auto_tac;
5.314 +by (etac parts.induct 1);
5.315 +by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
5.316 +qed "parts_insert_MPair";
5.317 +
5.318 +Addsimps [parts_insert_Agent, parts_insert_Nonce,
5.319 + parts_insert_Number, parts_insert_Key,
5.320 + parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
5.321 +
5.322 +
5.323 +Goal "parts (Key`N) = Key`N";
5.324 +by Auto_tac;
5.325 +by (etac parts.induct 1);
5.326 +by Auto_tac;
5.327 +qed "parts_image_Key";
5.328 +Addsimps [parts_image_Key];
5.329 +
5.330 +
5.331 +(*In any message, there is an upper bound N on its greatest nonce.*)
5.332 +Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
5.333 +by (induct_tac "msg" 1);
5.334 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
5.335 +(*MPair case: blast_tac works out the necessary sum itself!*)
5.336 +by (blast_tac (claset() addSEs [add_leE]) 2);
5.337 +(*Nonce case*)
5.338 +by (res_inst_tac [("x","N + Suc nat")] exI 1);
5.339 +by (auto_tac (claset() addSEs [add_leE], simpset()));
5.340 +qed "msg_Nonce_supply";
5.341 +
5.342 +
5.343 +(**** Inductive relation "analz" ****)
5.344 +
5.345 +val major::prems =
5.346 +Goal "[| {|X,Y|} : analz H; \
5.347 +\ [| X : analz H; Y : analz H |] ==> P \
5.348 +\ |] ==> P";
5.349 +by (cut_facts_tac [major] 1);
5.350 +by (resolve_tac prems 1);
5.351 +by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
5.352 +qed "MPair_analz";
5.353 +
5.354 +AddSEs [MPair_analz]; (*Making it safe speeds up proofs*)
5.355 +
5.356 +Goal "H <= analz(H)";
5.357 +by (Blast_tac 1);
5.358 +qed "analz_increasing";
5.359 +
5.360 +Goal "analz H <= parts H";
5.361 +by (rtac subsetI 1);
5.362 +by (etac analz.induct 1);
5.363 +by (ALLGOALS Blast_tac);
5.364 +qed "analz_subset_parts";
5.365 +
5.366 +bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
5.367 +
5.368 +
5.369 +Goal "parts (analz H) = parts H";
5.370 +by (rtac equalityI 1);
5.371 +by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
5.372 +by (Simp_tac 1);
5.373 +by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1);
5.374 +qed "parts_analz";
5.375 +Addsimps [parts_analz];
5.376 +
5.377 +Goal "analz (parts H) = parts H";
5.378 +by Auto_tac;
5.379 +by (etac analz.induct 1);
5.380 +by Auto_tac;
5.381 +qed "analz_parts";
5.382 +Addsimps [analz_parts];
5.383 +
5.384 +bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono));
5.385 +
5.386 +(** General equational properties **)
5.387 +
5.388 +Goal "analz{} = {}";
5.389 +by Safe_tac;
5.390 +by (etac analz.induct 1);
5.391 +by (ALLGOALS Blast_tac);
5.392 +qed "analz_empty";
5.393 +Addsimps [analz_empty];
5.394 +
5.395 +(*Converse fails: we can analz more from the union than from the
5.396 + separate parts, as a key in one might decrypt a message in the other*)
5.397 +Goal "analz(G) Un analz(H) <= analz(G Un H)";
5.398 +by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
5.399 +qed "analz_Un";
5.400 +
5.401 +Goal "insert X (analz H) <= analz(insert X H)";
5.402 +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
5.403 +qed "analz_insert";
5.404 +
5.405 +(** Rewrite rules for pulling out atomic messages **)
5.406 +
5.407 +fun analz_tac i =
5.408 + EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
5.409 + etac analz.induct i,
5.410 + Auto_tac];
5.411 +
5.412 +Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
5.413 +by (analz_tac 1);
5.414 +qed "analz_insert_Agent";
5.415 +
5.416 +Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
5.417 +by (analz_tac 1);
5.418 +qed "analz_insert_Nonce";
5.419 +
5.420 +Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
5.421 +by (analz_tac 1);
5.422 +qed "analz_insert_Number";
5.423 +
5.424 +Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
5.425 +by (analz_tac 1);
5.426 +qed "analz_insert_Hash";
5.427 +
5.428 +(*Can only pull out Keys if they are not needed to decrypt the rest*)
5.429 +Goalw [keysFor_def]
5.430 + "K ~: keysFor (analz H) ==> \
5.431 +\ analz (insert (Key K) H) = insert (Key K) (analz H)";
5.432 +by (analz_tac 1);
5.433 +qed "analz_insert_Key";
5.434 +
5.435 +Goal "analz (insert {|X,Y|} H) = \
5.436 +\ insert {|X,Y|} (analz (insert X (insert Y H)))";
5.437 +by (rtac equalityI 1);
5.438 +by (rtac subsetI 1);
5.439 +by (etac analz.induct 1);
5.440 +by Auto_tac;
5.441 +by (etac analz.induct 1);
5.442 +by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
5.443 +qed "analz_insert_MPair";
5.444 +
5.445 +(*Can pull out enCrypted message if the Key is not known*)
5.446 +Goal "Key (invKey K) ~: analz H ==> \
5.447 +\ analz (insert (Crypt K X) H) = \
5.448 +\ insert (Crypt K X) (analz H)";
5.449 +by (analz_tac 1);
5.450 +qed "analz_insert_Crypt";
5.451 +
5.452 +Goal "Key (invKey K) : analz H ==> \
5.453 +\ analz (insert (Crypt K X) H) <= \
5.454 +\ insert (Crypt K X) (analz (insert X H))";
5.455 +by (rtac subsetI 1);
5.456 +by (eres_inst_tac [("xa","x")] analz.induct 1);
5.457 +by Auto_tac;
5.458 +val lemma1 = result();
5.459 +
5.460 +Goal "Key (invKey K) : analz H ==> \
5.461 +\ insert (Crypt K X) (analz (insert X H)) <= \
5.462 +\ analz (insert (Crypt K X) H)";
5.463 +by Auto_tac;
5.464 +by (eres_inst_tac [("xa","x")] analz.induct 1);
5.465 +by Auto_tac;
5.466 +by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
5.467 +val lemma2 = result();
5.468 +
5.469 +Goal "Key (invKey K) : analz H ==> \
5.470 +\ analz (insert (Crypt K X) H) = \
5.471 +\ insert (Crypt K X) (analz (insert X H))";
5.472 +by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
5.473 +qed "analz_insert_Decrypt";
5.474 +
5.475 +(*Case analysis: either the message is secure, or it is not!
5.476 + Effective, but can cause subgoals to blow up!
5.477 + Use with split_if; apparently split_tac does not cope with patterns
5.478 + such as "analz (insert (Crypt K X) H)" *)
5.479 +Goal "analz (insert (Crypt K X) H) = \
5.480 +\ (if (Key (invKey K) : analz H) \
5.481 +\ then insert (Crypt K X) (analz (insert X H)) \
5.482 +\ else insert (Crypt K X) (analz H))";
5.483 +by (case_tac "Key (invKey K) : analz H " 1);
5.484 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt,
5.485 + analz_insert_Decrypt])));
5.486 +qed "analz_Crypt_if";
5.487 +
5.488 +Addsimps [analz_insert_Agent, analz_insert_Nonce,
5.489 + analz_insert_Number, analz_insert_Key,
5.490 + analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
5.491 +
5.492 +(*This rule supposes "for the sake of argument" that we have the key.*)
5.493 +Goal "analz (insert (Crypt K X) H) <= \
5.494 +\ insert (Crypt K X) (analz (insert X H))";
5.495 +by (rtac subsetI 1);
5.496 +by (etac analz.induct 1);
5.497 +by Auto_tac;
5.498 +qed "analz_insert_Crypt_subset";
5.499 +
5.500 +
5.501 +Goal "analz (Key`N) = Key`N";
5.502 +by Auto_tac;
5.503 +by (etac analz.induct 1);
5.504 +by Auto_tac;
5.505 +qed "analz_image_Key";
5.506 +
5.507 +Addsimps [analz_image_Key];
5.508 +
5.509 +
5.510 +(** Idempotence and transitivity **)
5.511 +
5.512 +Goal "X: analz (analz H) ==> X: analz H";
5.513 +by (etac analz.induct 1);
5.514 +by (ALLGOALS Blast_tac);
5.515 +qed "analz_analzD";
5.516 +AddSDs [analz_analzD];
5.517 +
5.518 +Goal "analz (analz H) = analz H";
5.519 +by (Blast_tac 1);
5.520 +qed "analz_idem";
5.521 +Addsimps [analz_idem];
5.522 +
5.523 +Goal "[| X: analz G; G <= analz H |] ==> X: analz H";
5.524 +by (dtac analz_mono 1);
5.525 +by (Blast_tac 1);
5.526 +qed "analz_trans";
5.527 +
5.528 +(*Cut; Lemma 2 of Lowe*)
5.529 +Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
5.530 +by (etac analz_trans 1);
5.531 +by (Blast_tac 1);
5.532 +qed "analz_cut";
5.533 +
5.534 +(*Cut can be proved easily by induction on
5.535 + "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
5.536 +*)
5.537 +
5.538 +(*This rewrite rule helps in the simplification of messages that involve
5.539 + the forwarding of unknown components (X). Without it, removing occurrences
5.540 + of X can be very complicated. *)
5.541 +Goal "X: analz H ==> analz (insert X H) = analz H";
5.542 +by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
5.543 +qed "analz_insert_eq";
5.544 +
5.545 +
5.546 +(** A congruence rule for "analz" **)
5.547 +
5.548 +Goal "[| analz G <= analz G'; analz H <= analz H' \
5.549 +\ |] ==> analz (G Un H) <= analz (G' Un H')";
5.550 +by (Clarify_tac 1);
5.551 +by (etac analz.induct 1);
5.552 +by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
5.553 +qed "analz_subset_cong";
5.554 +
5.555 +Goal "[| analz G = analz G'; analz H = analz H' \
5.556 +\ |] ==> analz (G Un H) = analz (G' Un H')";
5.557 +by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
5.558 + ORELSE' etac equalityE));
5.559 +qed "analz_cong";
5.560 +
5.561 +
5.562 +Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
5.563 +by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
5.564 + setloop (rtac analz_cong)) 1);
5.565 +qed "analz_insert_cong";
5.566 +
5.567 +(*If there are no pairs or encryptions then analz does nothing*)
5.568 +Goal "[| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \
5.569 +\ analz H = H";
5.570 +by Safe_tac;
5.571 +by (etac analz.induct 1);
5.572 +by (ALLGOALS Blast_tac);
5.573 +qed "analz_trivial";
5.574 +
5.575 +(*These two are obsolete (with a single Spy) but cost little to prove...*)
5.576 +Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
5.577 +by (etac analz.induct 1);
5.578 +by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
5.579 +val lemma = result();
5.580 +
5.581 +Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
5.582 +by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
5.583 +qed "analz_UN_analz";
5.584 +Addsimps [analz_UN_analz];
5.585 +
5.586 +
5.587 +(**** Inductive relation "synth" ****)
5.588 +
5.589 +Goal "H <= synth(H)";
5.590 +by (Blast_tac 1);
5.591 +qed "synth_increasing";
5.592 +
5.593 +(** Unions **)
5.594 +
5.595 +(*Converse fails: we can synth more from the union than from the
5.596 + separate parts, building a compound message using elements of each.*)
5.597 +Goal "synth(G) Un synth(H) <= synth(G Un H)";
5.598 +by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
5.599 +qed "synth_Un";
5.600 +
5.601 +Goal "insert X (synth H) <= synth(insert X H)";
5.602 +by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
5.603 +qed "synth_insert";
5.604 +
5.605 +(** Idempotence and transitivity **)
5.606 +
5.607 +Goal "X: synth (synth H) ==> X: synth H";
5.608 +by (etac synth.induct 1);
5.609 +by (ALLGOALS Blast_tac);
5.610 +qed "synth_synthD";
5.611 +AddSDs [synth_synthD];
5.612 +
5.613 +Goal "synth (synth H) = synth H";
5.614 +by (Blast_tac 1);
5.615 +qed "synth_idem";
5.616 +
5.617 +Goal "[| X: synth G; G <= synth H |] ==> X: synth H";
5.618 +by (dtac synth_mono 1);
5.619 +by (Blast_tac 1);
5.620 +qed "synth_trans";
5.621 +
5.622 +(*Cut; Lemma 2 of Lowe*)
5.623 +Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
5.624 +by (etac synth_trans 1);
5.625 +by (Blast_tac 1);
5.626 +qed "synth_cut";
5.627 +
5.628 +Goal "Agent A : synth H";
5.629 +by (Blast_tac 1);
5.630 +qed "Agent_synth";
5.631 +
5.632 +Goal "Number n : synth H";
5.633 +by (Blast_tac 1);
5.634 +qed "Number_synth";
5.635 +
5.636 +Goal "(Nonce N : synth H) = (Nonce N : H)";
5.637 +by (Blast_tac 1);
5.638 +qed "Nonce_synth_eq";
5.639 +
5.640 +Goal "(Key K : synth H) = (Key K : H)";
5.641 +by (Blast_tac 1);
5.642 +qed "Key_synth_eq";
5.643 +
5.644 +Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
5.645 +by (Blast_tac 1);
5.646 +qed "Crypt_synth_eq";
5.647 +
5.648 +Addsimps [Agent_synth, Number_synth,
5.649 + Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
5.650 +
5.651 +
5.652 +Goalw [keysFor_def]
5.653 + "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}";
5.654 +by (Blast_tac 1);
5.655 +qed "keysFor_synth";
5.656 +Addsimps [keysFor_synth];
5.657 +
5.658 +
5.659 +(*** Combinations of parts, analz and synth ***)
5.660 +
5.661 +Goal "parts (synth H) = parts H Un synth H";
5.662 +by (rtac equalityI 1);
5.663 +by (rtac subsetI 1);
5.664 +by (etac parts.induct 1);
5.665 +by (ALLGOALS
5.666 + (blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD,
5.667 + parts.Fst, parts.Snd, parts.Body])));
5.668 +qed "parts_synth";
5.669 +Addsimps [parts_synth];
5.670 +
5.671 +Goal "analz (analz G Un H) = analz (G Un H)";
5.672 +by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
5.673 +by (ALLGOALS Simp_tac);
5.674 +qed "analz_analz_Un";
5.675 +
5.676 +Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
5.677 +by (rtac equalityI 1);
5.678 +by (rtac subsetI 1);
5.679 +by (etac analz.induct 1);
5.680 +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5);
5.681 +by (ALLGOALS
5.682 + (blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt])));
5.683 +qed "analz_synth_Un";
5.684 +
5.685 +Goal "analz (synth H) = analz H Un synth H";
5.686 +by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
5.687 +by (Full_simp_tac 1);
5.688 +qed "analz_synth";
5.689 +Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
5.690 +
5.691 +
5.692 +(** For reasoning about the Fake rule in traces **)
5.693 +
5.694 +Goal "X: G ==> parts(insert X H) <= parts G Un parts H";
5.695 +by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
5.696 +by (Blast_tac 1);
5.697 +qed "parts_insert_subset_Un";
5.698 +
5.699 +(*More specifically for Fake. Very occasionally we could do with a version
5.700 + of the form parts{X} <= synth (analz H) Un parts H *)
5.701 +Goal "X: synth (analz H) ==> \
5.702 +\ parts (insert X H) <= synth (analz H) Un parts H";
5.703 +by (dtac parts_insert_subset_Un 1);
5.704 +by (Full_simp_tac 1);
5.705 +by (Blast_tac 1);
5.706 +qed "Fake_parts_insert";
5.707 +
5.708 +(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
5.709 +Goal "X: synth (analz G) ==> \
5.710 +\ analz (insert X H) <= synth (analz G) Un analz (G Un H)";
5.711 +by (rtac subsetI 1);
5.712 +by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
5.713 +by (blast_tac (claset() addIs [impOfSubs analz_mono,
5.714 + impOfSubs (analz_mono RS synth_mono)]) 2);
5.715 +by (Full_simp_tac 1);
5.716 +by (Blast_tac 1);
5.717 +qed "Fake_analz_insert";
5.718 +
5.719 +Goal "(X: analz H & X: parts H) = (X: analz H)";
5.720 +by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
5.721 +val analz_conj_parts = result();
5.722 +
5.723 +Goal "(X: analz H | X: parts H) = (X: parts H)";
5.724 +by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
5.725 +val analz_disj_parts = result();
5.726 +
5.727 +AddIffs [analz_conj_parts, analz_disj_parts];
5.728 +
5.729 +(*Without this equation, other rules for synth and analz would yield
5.730 + redundant cases*)
5.731 +Goal "({|X,Y|} : synth (analz H)) = \
5.732 +\ (X : synth (analz H) & Y : synth (analz H))";
5.733 +by (Blast_tac 1);
5.734 +qed "MPair_synth_analz";
5.735 +
5.736 +AddIffs [MPair_synth_analz];
5.737 +
5.738 +Goal "[| Key K : analz H; Key (invKey K) : analz H |] \
5.739 +\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
5.740 +by (Blast_tac 1);
5.741 +qed "Crypt_synth_analz";
5.742 +
5.743 +
5.744 +Goal "X ~: synth (analz H) \
5.745 +\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
5.746 +by (Blast_tac 1);
5.747 +qed "Hash_synth_analz";
5.748 +Addsimps [Hash_synth_analz];
5.749 +
5.750 +
5.751 +(**** HPair: a combination of Hash and MPair ****)
5.752 +
5.753 +(*** Freeness ***)
5.754 +
5.755 +Goalw [HPair_def] "Agent A ~= Hash[X] Y";
5.756 +by (Simp_tac 1);
5.757 +qed "Agent_neq_HPair";
5.758 +
5.759 +Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
5.760 +by (Simp_tac 1);
5.761 +qed "Nonce_neq_HPair";
5.762 +
5.763 +Goalw [HPair_def] "Number N ~= Hash[X] Y";
5.764 +by (Simp_tac 1);
5.765 +qed "Number_neq_HPair";
5.766 +
5.767 +Goalw [HPair_def] "Key K ~= Hash[X] Y";
5.768 +by (Simp_tac 1);
5.769 +qed "Key_neq_HPair";
5.770 +
5.771 +Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
5.772 +by (Simp_tac 1);
5.773 +qed "Hash_neq_HPair";
5.774 +
5.775 +Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
5.776 +by (Simp_tac 1);
5.777 +qed "Crypt_neq_HPair";
5.778 +
5.779 +val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair,
5.780 + Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
5.781 +
5.782 +AddIffs HPair_neqs;
5.783 +AddIffs (HPair_neqs RL [not_sym]);
5.784 +
5.785 +Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
5.786 +by (Simp_tac 1);
5.787 +qed "HPair_eq";
5.788 +
5.789 +Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
5.790 +by (Simp_tac 1);
5.791 +qed "MPair_eq_HPair";
5.792 +
5.793 +Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
5.794 +by Auto_tac;
5.795 +qed "HPair_eq_MPair";
5.796 +
5.797 +AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
5.798 +
5.799 +
5.800 +(*** Specialized laws, proved in terms of those for Hash and MPair ***)
5.801 +
5.802 +Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
5.803 +by (Simp_tac 1);
5.804 +qed "keysFor_insert_HPair";
5.805 +
5.806 +Goalw [HPair_def]
5.807 + "parts (insert (Hash[X] Y) H) = \
5.808 +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
5.809 +by (Simp_tac 1);
5.810 +qed "parts_insert_HPair";
5.811 +
5.812 +Goalw [HPair_def]
5.813 + "analz (insert (Hash[X] Y) H) = \
5.814 +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
5.815 +by (Simp_tac 1);
5.816 +qed "analz_insert_HPair";
5.817 +
5.818 +Goalw [HPair_def] "X ~: synth (analz H) \
5.819 +\ ==> (Hash[X] Y : synth (analz H)) = \
5.820 +\ (Hash {|X, Y|} : analz H & Y : synth (analz H))";
5.821 +by (Simp_tac 1);
5.822 +by (Blast_tac 1);
5.823 +qed "HPair_synth_analz";
5.824 +
5.825 +Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair,
5.826 + HPair_synth_analz, HPair_synth_analz];
5.827 +
5.828 +
5.829 +(*We do NOT want Crypt... messages broken up in protocols!!*)
5.830 +Delrules [make_elim parts.Body];
5.831 +
5.832 +
5.833 +(** Rewrites to push in Key and Crypt messages, so that other messages can
5.834 + be pulled out using the analz_insert rules **)
5.835 +
5.836 +fun insComm x y = inst "x" x (inst "y" y insert_commute);
5.837 +
5.838 +val pushKeys = map (insComm "Key ?K")
5.839 + ["Agent ?C", "Nonce ?N", "Number ?N",
5.840 + "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
5.841 +
5.842 +val pushCrypts = map (insComm "Crypt ?X ?K")
5.843 + ["Agent ?C", "Nonce ?N", "Number ?N",
5.844 + "Hash ?X'", "MPair ?X' ?Y"];
5.845 +
5.846 +(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
5.847 +bind_thms ("pushes", pushKeys@pushCrypts);
5.848 +
5.849 +
5.850 +(*** Tactics useful for many protocol proofs ***)
5.851 +
5.852 +(*Prove base case (subgoal i) and simplify others. A typical base case
5.853 + concerns Crypt K X ~: Key`shrK`bad and cannot be proved by rewriting
5.854 + alone.*)
5.855 +fun prove_simple_subgoals_tac i =
5.856 + force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
5.857 + ALLGOALS Asm_simp_tac;
5.858 +
5.859 +fun Fake_parts_insert_tac i =
5.860 + blast_tac (claset() addIs [parts_insertI]
5.861 + addDs [impOfSubs analz_subset_parts,
5.862 + impOfSubs Fake_parts_insert]) i;
5.863 +
5.864 +(*Apply rules to break down assumptions of the form
5.865 + Y : parts(insert X H) and Y : analz(insert X H)
5.866 +*)
5.867 +val Fake_insert_tac =
5.868 + dresolve_tac [impOfSubs Fake_analz_insert,
5.869 + impOfSubs Fake_parts_insert] THEN'
5.870 + eresolve_tac [asm_rl, synth.Inj];
5.871 +
5.872 +fun Fake_insert_simp_tac i =
5.873 + REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i;
5.874 +
5.875 +
5.876 +(*Analysis of Fake cases. Also works for messages that forward unknown parts,
5.877 + but this application is no longer necessary if analz_insert_eq is used.
5.878 + Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
5.879 + DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
5.880 +
5.881 +val atomic_spy_analz_tac = SELECT_GOAL
5.882 + (Fake_insert_simp_tac 1
5.883 + THEN
5.884 + IF_UNSOLVED (Blast.depth_tac
5.885 + (claset() addIs [analz_insertI,
5.886 + impOfSubs analz_subset_parts]) 4 1));
5.887 +
5.888 +fun spy_analz_tac i =
5.889 + DETERM
5.890 + (SELECT_GOAL
5.891 + (EVERY
5.892 + [ (*push in occurrences of X...*)
5.893 + (REPEAT o CHANGED)
5.894 + (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
5.895 + (*...allowing further simplifications*)
5.896 + Simp_tac 1,
5.897 + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
5.898 + DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
5.899 +
5.900 +(*By default only o_apply is built-in. But in the presence of eta-expansion
5.901 + this means that some terms displayed as (f o g) will be rewritten, and others
5.902 + will not!*)
5.903 +Addsimps [o_def];