1839

1 
(* Title: HOL/Auth/Message


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1996 University of Cambridge


5 


6 
Datatypes of agents and messages;


7 
Inductive relations "parts", "analyze" and "synthesize"


8 
*)


9 


10 
open Message;


11 


12 


13 
(**************** INSTALL CENTRALLY SOMEWHERE? ****************)


14 


15 
(*Maybe swap the safe_tac and simp_tac lines?**)


16 
fun auto_tac (cs,ss) =


17 
TRY (safe_tac cs) THEN


18 
ALLGOALS (asm_full_simp_tac ss) THEN


19 
REPEAT (FIRSTGOAL (best_tac (cs addss ss)));


20 


21 
fun Auto_tac() = auto_tac (!claset, !simpset);


22 


23 
fun auto() = by (Auto_tac());


24 


25 
fun imp_of_subset th = th RSN (2, rev_subsetD);


26 


27 
(**************** INSTALL CENTRALLY SOMEWHERE? ****************)


28 


29 


30 


31 
(** Inverse of keys **)


32 


33 
goal thy "!!K K'. (invKey K = invKey K') = (K=K')";


34 
by (Step_tac 1);


35 
br box_equals 1;


36 
by (REPEAT (rtac invKey 2));


37 
by (Asm_simp_tac 1);


38 
qed "invKey_eq";


39 


40 
Addsimps [invKey, invKey_eq];


41 


42 


43 
(**** keysFor operator ****)


44 


45 
goalw thy [keysFor_def] "keysFor {} = {}";


46 
by (Fast_tac 1);


47 
qed "keysFor_empty";


48 


49 
goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";


50 
by (Fast_tac 1);


51 
qed "keysFor_Un";


52 


53 
goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";


54 
by (Fast_tac 1);


55 
qed "keysFor_UN";


56 


57 
(*Monotonicity*)


58 
goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";


59 
by (Fast_tac 1);


60 
qed "keysFor_mono";


61 


62 
goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";


63 
by (fast_tac (!claset addss (!simpset)) 1);


64 
qed "keysFor_insert_Agent";


65 


66 
goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";


67 
by (fast_tac (!claset addss (!simpset)) 1);


68 
qed "keysFor_insert_Nonce";


69 


70 
goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";


71 
by (fast_tac (!claset addss (!simpset)) 1);


72 
qed "keysFor_insert_Key";


73 


74 
goalw thy [keysFor_def] "keysFor (insert {X,Y} H) = keysFor H";


75 
by (fast_tac (!claset addss (!simpset)) 1);


76 
qed "keysFor_insert_MPair";


77 


78 
goalw thy [keysFor_def]


79 
"keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";


80 
by (Auto_tac());


81 
by (fast_tac (!claset addIs [image_eqI]) 1);


82 
qed "keysFor_insert_Crypt";


83 


84 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,


85 
keysFor_insert_Agent, keysFor_insert_Nonce,


86 
keysFor_insert_Key, keysFor_insert_MPair,


87 
keysFor_insert_Crypt];


88 


89 


90 
(**** Inductive relation "parts" ****)


91 


92 
val major::prems =


93 
goal thy "[ {X,Y} : parts H; \


94 
\ [ X : parts H; Y : parts H ] ==> P \


95 
\ ] ==> P";


96 
by (cut_facts_tac [major] 1);


97 
brs prems 1;


98 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));


99 
qed "MPair_parts";


100 


101 
AddIs [parts.Inj];


102 
AddSEs [MPair_parts];


103 
AddDs [parts.Body];


104 


105 
goal thy "H <= parts(H)";


106 
by (Fast_tac 1);


107 
qed "parts_increasing";


108 


109 
(*Monotonicity*)


110 
goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";


111 
by (rtac lfp_mono 1);


112 
by (REPEAT (ares_tac basic_monos 1));


113 
qed "parts_mono";


114 


115 
goal thy "parts{} = {}";


116 
by (Step_tac 1);


117 
be parts.induct 1;


118 
by (ALLGOALS Fast_tac);


119 
qed "parts_empty";


120 
Addsimps [parts_empty];


121 


122 
goal thy "!!X. X: parts{} ==> P";


123 
by (Asm_full_simp_tac 1);


124 
qed "parts_emptyE";


125 
AddSEs [parts_emptyE];


126 


127 


128 
(** Unions **)


129 


130 
goal thy "parts(G) Un parts(H) <= parts(G Un H)";


131 
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));


132 
val parts_Un_subset1 = result();


133 


134 
goal thy "parts(G Un H) <= parts(G) Un parts(H)";


135 
br subsetI 1;


136 
be parts.induct 1;


137 
by (ALLGOALS Fast_tac);


138 
val parts_Un_subset2 = result();


139 


140 
goal thy "parts(G Un H) = parts(G) Un parts(H)";


141 
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));


142 
qed "parts_Un";


143 


144 
goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";


145 
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));


146 
val parts_UN_subset1 = result();


147 


148 
goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";


149 
br subsetI 1;


150 
be parts.induct 1;


151 
by (ALLGOALS Fast_tac);


152 
val parts_UN_subset2 = result();


153 


154 
goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";


155 
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));


156 
qed "parts_UN";


157 


158 
goal thy "parts(UN x. H x) = (UN x. parts(H x))";


159 
by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);


160 
qed "parts_UN1";


161 


162 
(*Added to simplify arguments to parts, analyze and synthesize*)


163 
Addsimps [parts_Un, parts_UN, parts_UN1];


164 


165 
goal thy "insert X (parts H) <= parts(insert X H)";


166 
by (fast_tac (!claset addEs [imp_of_subset parts_mono]) 1);


167 
qed "parts_insert_subset";


168 


169 
(*Especially for reasoning about the Fake rule in traces*)


170 
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";


171 
br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;


172 
by (Fast_tac 1);


173 
qed "parts_insert_subset_Un";


174 


175 
(** Idempotence and transitivity **)


176 


177 
goal thy "!!H. X: parts (parts H) ==> X: parts H";


178 
be parts.induct 1;


179 
by (ALLGOALS Fast_tac);


180 
qed "parts_partsE";


181 
AddSEs [parts_partsE];


182 


183 
goal thy "parts (parts H) = parts H";


184 
by (Fast_tac 1);


185 
qed "parts_idem";


186 
Addsimps [parts_idem];


187 


188 
goal thy "!!H. [ X: parts G; G <= parts H ] ==> X: parts H";


189 
by (dtac parts_mono 1);


190 
by (Fast_tac 1);


191 
qed "parts_trans";


192 


193 
(*Cut*)


194 
goal thy "!!H. [ X: parts H; Y: parts (insert X H) ] ==> Y: parts H";


195 
be parts_trans 1;


196 
by (Fast_tac 1);


197 
qed "parts_cut";


198 


199 


200 
(** Rewrite rules for pulling out atomic messages **)


201 


202 
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";


203 
by (rtac (parts_insert_subset RSN (2, equalityI)) 1);


204 
br subsetI 1;


205 
be parts.induct 1;


206 
(*Simplification breaks up equalities between messages;


207 
how to make it work for fast_tac??*)


208 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


209 
qed "parts_insert_Agent";


210 


211 
goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";


212 
by (rtac (parts_insert_subset RSN (2, equalityI)) 1);


213 
br subsetI 1;


214 
be parts.induct 1;


215 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


216 
qed "parts_insert_Nonce";


217 


218 
goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";


219 
by (rtac (parts_insert_subset RSN (2, equalityI)) 1);


220 
br subsetI 1;


221 
be parts.induct 1;


222 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


223 
qed "parts_insert_Key";


224 


225 
goal thy "parts (insert (Crypt X K) H) = \


226 
\ insert (Crypt X K) (parts (insert X H))";


227 
br equalityI 1;


228 
br subsetI 1;


229 
be parts.induct 1;


230 
by (Auto_tac());


231 
be parts.induct 1;


232 
by (ALLGOALS (best_tac (!claset addIs [parts.Body])));


233 
qed "parts_insert_Crypt";


234 


235 
goal thy "parts (insert {X,Y} H) = \


236 
\ insert {X,Y} (parts (insert X (insert Y H)))";


237 
br equalityI 1;


238 
br subsetI 1;


239 
be parts.induct 1;


240 
by (Auto_tac());


241 
be parts.induct 1;


242 
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));


243 
qed "parts_insert_MPair";


244 


245 
Addsimps [parts_insert_Agent, parts_insert_Nonce,


246 
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];


247 


248 


249 
(**** Inductive relation "analyze" ****)


250 


251 
val major::prems =


252 
goal thy "[ {X,Y} : analyze H; \


253 
\ [ X : analyze H; Y : analyze H ] ==> P \


254 
\ ] ==> P";


255 
by (cut_facts_tac [major] 1);


256 
brs prems 1;


257 
by (REPEAT (eresolve_tac [asm_rl, analyze.Fst, analyze.Snd] 1));


258 
qed "MPair_analyze";


259 


260 
AddIs [analyze.Inj];


261 
AddSEs [MPair_analyze];


262 
AddDs [analyze.Decrypt];


263 


264 
goal thy "H <= analyze(H)";


265 
by (Fast_tac 1);


266 
qed "analyze_increasing";


267 


268 
goal thy "analyze H <= parts H";


269 
by (rtac subsetI 1);


270 
be analyze.induct 1;


271 
by (ALLGOALS Fast_tac);


272 
qed "analyze_subset_parts";


273 


274 
bind_thm ("not_parts_not_analyze", analyze_subset_parts RS contra_subsetD);


275 


276 


277 
goal thy "parts (analyze H) = parts H";


278 
br equalityI 1;


279 
br (analyze_subset_parts RS parts_mono RS subset_trans) 1;


280 
by (Simp_tac 1);


281 
by (fast_tac (!claset addDs [analyze_increasing RS parts_mono RS subsetD]) 1);


282 
qed "parts_analyze";


283 
Addsimps [parts_analyze];


284 


285 
(*Monotonicity; Lemma 1 of Lowe*)


286 
goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";


287 
by (rtac lfp_mono 1);


288 
by (REPEAT (ares_tac basic_monos 1));


289 
qed "analyze_mono";


290 


291 
(** General equational properties **)


292 


293 
goal thy "analyze{} = {}";


294 
by (Step_tac 1);


295 
be analyze.induct 1;


296 
by (ALLGOALS Fast_tac);


297 
qed "analyze_empty";


298 
Addsimps [analyze_empty];


299 


300 
(*Converse fails: we can analyze more from the union than from the


301 
separate parts, as a key in one might decrypt a message in the other*)


302 
goal thy "analyze(G) Un analyze(H) <= analyze(G Un H)";


303 
by (REPEAT (ares_tac [Un_least, analyze_mono, Un_upper1, Un_upper2] 1));


304 
qed "analyze_Un";


305 


306 
goal thy "insert X (analyze H) <= analyze(insert X H)";


307 
by (fast_tac (!claset addEs [imp_of_subset analyze_mono]) 1);


308 
qed "analyze_insert";


309 


310 
(** Rewrite rules for pulling out atomic messages **)


311 


312 
goal thy "analyze (insert (Agent agt) H) = insert (Agent agt) (analyze H)";


313 
by (rtac (analyze_insert RSN (2, equalityI)) 1);


314 
br subsetI 1;


315 
be analyze.induct 1;


316 
(*Simplification breaks up equalities between messages;


317 
how to make it work for fast_tac??*)


318 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


319 
qed "analyze_insert_Agent";


320 


321 
goal thy "analyze (insert (Nonce N) H) = insert (Nonce N) (analyze H)";


322 
by (rtac (analyze_insert RSN (2, equalityI)) 1);


323 
br subsetI 1;


324 
be analyze.induct 1;


325 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


326 
qed "analyze_insert_Nonce";


327 


328 
(*Can only pull out Keys if they are not needed to decrypt the rest*)


329 
goalw thy [keysFor_def]


330 
"!!K. K ~: keysFor (analyze H) ==> \


331 
\ analyze (insert (Key K) H) = insert (Key K) (analyze H)";


332 
by (rtac (analyze_insert RSN (2, equalityI)) 1);


333 
br subsetI 1;


334 
be analyze.induct 1;


335 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


336 
qed "analyze_insert_Key";


337 


338 
goal thy "!!H. Key (invKey K) ~: analyze H ==> \


339 
\ analyze (insert (Crypt X K) H) = \


340 
\ insert (Crypt X K) (analyze H)";


341 
by (rtac (analyze_insert RSN (2, equalityI)) 1);


342 
br subsetI 1;


343 
be analyze.induct 1;


344 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


345 
qed "analyze_insert_Crypt";


346 


347 
goal thy "!!H. Key (invKey K) : analyze H ==> \


348 
\ analyze (insert (Crypt X K) H) <= \


349 
\ insert (Crypt X K) (analyze (insert X H))";


350 
br subsetI 1;


351 
by (eres_inst_tac [("za","x")] analyze.induct 1);


352 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


353 
val lemma1 = result();


354 


355 
goal thy "!!H. Key (invKey K) : analyze H ==> \


356 
\ insert (Crypt X K) (analyze (insert X H)) <= \


357 
\ analyze (insert (Crypt X K) H)";


358 
by (Auto_tac());


359 
by (eres_inst_tac [("za","x")] analyze.induct 1);


360 
by (Auto_tac());


361 
by (best_tac (!claset addIs [subset_insertI RS analyze_mono RS subsetD,


362 
analyze.Decrypt]) 1);


363 
val lemma2 = result();


364 


365 
goal thy "!!H. Key (invKey K) : analyze H ==> \


366 
\ analyze (insert (Crypt X K) H) = \


367 
\ insert (Crypt X K) (analyze (insert X H))";


368 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));


369 
qed "analyze_insert_Decrypt";


370 


371 
Addsimps [analyze_insert_Agent, analyze_insert_Nonce,


372 
analyze_insert_Key, analyze_insert_Crypt,


373 
analyze_insert_Decrypt];


374 


375 


376 
(*This rule supposes "for the sake of argument" that we have the key.*)


377 
goal thy "analyze (insert (Crypt X K) H) <= \


378 
\ insert (Crypt X K) (analyze (insert X H))";


379 
br subsetI 1;


380 
be analyze.induct 1;


381 
by (Auto_tac());


382 
qed "analyze_insert_Crypt_subset";


383 


384 


385 
(** Rewrite rules for pulling out atomic parts of messages **)


386 


387 
goal thy "analyze (insert X H) <= analyze (insert {X,Y} H)";


388 
br subsetI 1;


389 
be analyze.induct 1;


390 
by (ALLGOALS (best_tac (!claset addIs [analyze.Fst])));


391 
qed "analyze_insert_subset_MPair1";


392 


393 
goal thy "analyze (insert Y H) <= analyze (insert {X,Y} H)";


394 
br subsetI 1;


395 
be analyze.induct 1;


396 
by (ALLGOALS (best_tac (!claset addIs [analyze.Snd])));


397 
qed "analyze_insert_subset_MPair2";


398 


399 
goal thy "analyze (insert {Agent agt,Y} H) = \


400 
\ insert {Agent agt,Y} (insert (Agent agt) (analyze (insert Y H)))";


401 
by (rtac equalityI 1);


402 
by (best_tac (!claset addIs [analyze.Fst,


403 
imp_of_subset analyze_insert_subset_MPair2]) 2);


404 
br subsetI 1;


405 
be analyze.induct 1;


406 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


407 
qed "analyze_insert_Agent_MPair";


408 


409 
goal thy "analyze (insert {Nonce N,Y} H) = \


410 
\ insert {Nonce N,Y} (insert (Nonce N) (analyze (insert Y H)))";


411 
by (rtac equalityI 1);


412 
by (best_tac (!claset addIs [analyze.Fst,


413 
imp_of_subset analyze_insert_subset_MPair2]) 2);


414 
br subsetI 1;


415 
be analyze.induct 1;


416 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


417 
qed "analyze_insert_Nonce_MPair";


418 


419 
(*Can only pull out Keys if they are not needed to decrypt the rest*)


420 
goalw thy [keysFor_def]


421 
"!!K. K ~: keysFor (analyze (insert Y H)) ==> \


422 
\ analyze (insert {Key K, Y} H) = \


423 
\ insert {Key K, Y} (insert (Key K) (analyze (insert Y H)))";


424 
by (rtac equalityI 1);


425 
by (best_tac (!claset addIs [analyze.Fst,


426 
imp_of_subset analyze_insert_subset_MPair2]) 2);


427 
br subsetI 1;


428 
be analyze.induct 1;


429 
by (ALLGOALS (fast_tac (!claset addss (!simpset))));


430 
qed "analyze_insert_Key_MPair";


431 


432 
Addsimps [analyze_insert_Agent_MPair, analyze_insert_Nonce_MPair,


433 
analyze_insert_Key_MPair];


434 


435 
(** Idempotence and transitivity **)


436 


437 
goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";


438 
be analyze.induct 1;


439 
by (ALLGOALS Fast_tac);


440 
qed "analyze_analyzeE";


441 
AddSEs [analyze_analyzeE];


442 


443 
goal thy "analyze (analyze H) = analyze H";


444 
by (Fast_tac 1);


445 
qed "analyze_idem";


446 
Addsimps [analyze_idem];


447 


448 
goal thy "!!H. [ X: analyze G; G <= analyze H ] ==> X: analyze H";


449 
by (dtac analyze_mono 1);


450 
by (Fast_tac 1);


451 
qed "analyze_trans";


452 


453 
(*Cut; Lemma 2 of Lowe*)


454 
goal thy "!!H. [ X: analyze H; Y: analyze (insert X H) ] ==> Y: analyze H";


455 
be analyze_trans 1;


456 
by (Fast_tac 1);


457 
qed "analyze_cut";


458 


459 
(*Cut can be proved easily by induction on


460 
"!!H. Y: analyze (insert X H) ==> X: analyze H > Y: analyze H"


461 
*)


462 


463 
(*If there are no pairs or encryptions then analyze does nothing*)


464 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt X K ~: H ] ==> \


465 
\ analyze H = H";


466 
by (Step_tac 1);


467 
be analyze.induct 1;


468 
by (ALLGOALS Fast_tac);


469 
qed "analyze_trivial";


470 


471 
(*Helps to prove Fake cases*)


472 
goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)";


473 
be analyze.induct 1;


474 
by (ALLGOALS (fast_tac (!claset addEs [imp_of_subset analyze_mono])));


475 
val lemma = result();


476 


477 
goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";


478 
by (fast_tac (!claset addIs [lemma]


479 
addEs [imp_of_subset analyze_mono]) 1);


480 
qed "analyze_UN_analyze";


481 
Addsimps [analyze_UN_analyze];


482 


483 


484 
(**** Inductive relation "synthesize" ****)


485 


486 
AddIs synthesize.intrs;


487 


488 
goal thy "H <= synthesize(H)";


489 
by (Fast_tac 1);


490 
qed "synthesize_increasing";


491 


492 
(*Monotonicity*)


493 
goalw thy synthesize.defs "!!G H. G<=H ==> synthesize(G) <= synthesize(H)";


494 
by (rtac lfp_mono 1);


495 
by (REPEAT (ares_tac basic_monos 1));


496 
qed "synthesize_mono";


497 


498 
(** Unions **)


499 


500 
(*Converse fails: we can synthesize more from the union than from the


501 
separate parts, building a compound message using elements of each.*)


502 
goal thy "synthesize(G) Un synthesize(H) <= synthesize(G Un H)";


503 
by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));


504 
qed "synthesize_Un";


505 


506 
(** Idempotence and transitivity **)


507 


508 
goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";


509 
be synthesize.induct 1;


510 
by (ALLGOALS Fast_tac);


511 
qed "synthesize_synthesizeE";


512 
AddSEs [synthesize_synthesizeE];


513 


514 
goal thy "synthesize (synthesize H) = synthesize H";


515 
by (Fast_tac 1);


516 
qed "synthesize_idem";


517 


518 
goal thy "!!H. [ X: synthesize G; G <= synthesize H ] ==> X: synthesize H";


519 
by (dtac synthesize_mono 1);


520 
by (Fast_tac 1);


521 
qed "synthesize_trans";


522 


523 
(*Cut; Lemma 2 of Lowe*)


524 
goal thy "!!H. [ X: synthesize H; Y: synthesize (insert X H) \


525 
\ ] ==> Y: synthesize H";


526 
be synthesize_trans 1;


527 
by (Fast_tac 1);


528 
qed "synthesize_cut";


529 


530 


531 
(*Can only produce a nonce or key if it is already known,


532 
but can synthesize a pair or encryption from its components...*)


533 
val mk_cases = synthesize.mk_cases msg.simps;


534 


535 
val Nonce_synthesize = mk_cases "Nonce n : synthesize H";


536 
val Key_synthesize = mk_cases "Key K : synthesize H";


537 
val MPair_synthesize = mk_cases "{X,Y} : synthesize H";


538 
val Crypt_synthesize = mk_cases "Crypt X K : synthesize H";


539 


540 
AddSEs [Nonce_synthesize, Key_synthesize, MPair_synthesize, Crypt_synthesize];


541 


542 
goal thy "(Nonce N : synthesize H) = (Nonce N : H)";


543 
by (Fast_tac 1);


544 
qed "Nonce_synthesize_eq";


545 


546 
goal thy "(Key K : synthesize H) = (Key K : H)";


547 
by (Fast_tac 1);


548 
qed "Key_synthesize_eq";


549 


550 
Addsimps [Nonce_synthesize_eq, Key_synthesize_eq];


551 


552 


553 
goalw thy [keysFor_def]


554 
"keysFor (synthesize H) = keysFor H Un invKey``{K. Key K : H}";


555 
by (Fast_tac 1);


556 
qed "keysFor_synthesize";


557 
Addsimps [keysFor_synthesize];


558 


559 


560 
(*** Combinations of parts, analyze and synthesize ***)


561 


562 
(*Not that useful, in view of the following one...*)


563 
goal thy "parts (synthesize H) <= synthesize (parts H)";


564 
by (Step_tac 1);


565 
be parts.induct 1;


566 
be (parts_increasing RS synthesize_mono RS subsetD) 1;


567 
by (ALLGOALS Fast_tac);


568 
qed "parts_synthesize_subset";


569 


570 
goal thy "parts (synthesize H) = parts H Un synthesize H";


571 
br equalityI 1;


572 
br subsetI 1;


573 
be parts.induct 1;


574 
by (ALLGOALS


575 
(best_tac (!claset addIs ((synthesize_increasing RS parts_mono RS subsetD)


576 
::parts.intrs))));


577 
qed "parts_synthesize";


578 
Addsimps [parts_synthesize];


579 


580 
goal thy "analyze (synthesize H) = analyze H Un synthesize H";


581 
br equalityI 1;


582 
br subsetI 1;


583 
be analyze.induct 1;


584 
by (best_tac


585 
(!claset addIs [synthesize_increasing RS analyze_mono RS subsetD]) 5);


586 
(*Strange that best_tac just can't hack this one...*)


587 
by (ALLGOALS (deepen_tac (!claset addIs analyze.intrs) 0));


588 
qed "analyze_synthesize";


589 
Addsimps [analyze_synthesize];


590 


591 
(*Hard to prove; still needed now that there's only one Enemy?*)


592 
goal thy "analyze (UN i. synthesize (H i)) = \


593 
\ analyze (UN i. H i) Un (UN i. synthesize (H i))";


594 
br equalityI 1;


595 
br subsetI 1;


596 
be analyze.induct 1;


597 
by (best_tac


598 
(!claset addEs [imp_of_subset synthesize_increasing,


599 
imp_of_subset analyze_mono]) 5);


600 
by (Best_tac 1);


601 
by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);


602 
by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);


603 
by (deepen_tac (!claset addSEs [analyze.Decrypt]


604 
addIs [analyze.Decrypt]) 0 1);


605 
qed "analyze_UN1_synthesize";


606 
Addsimps [analyze_UN1_synthesize];
