132 |
132 |
133 goal thy "parts(G Un H) = parts(G) Un parts(H)"; |
133 goal thy "parts(G Un H) = parts(G) Un parts(H)"; |
134 by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); |
134 by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); |
135 qed "parts_Un"; |
135 qed "parts_Un"; |
136 |
136 |
137 (*TWO inserts to avoid looping. This rewrite is better than nothing...*) |
137 goal thy "parts (insert X H) = parts {X} Un parts H"; |
|
138 by (stac (read_instantiate [("A","H")] insert_is_Un) 1); |
|
139 by (simp_tac (HOL_ss addsimps [parts_Un]) 1); |
|
140 qed "parts_insert"; |
|
141 |
|
142 (*TWO inserts to avoid looping. This rewrite is better than nothing. |
|
143 Not suitable for Addsimps: its behaviour can be strange.*) |
138 goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; |
144 goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; |
139 by (stac (read_instantiate [("A","H")] insert_is_Un) 1); |
145 by (simp_tac (!simpset addsimps [Un_assoc]) 1); |
140 by (stac (read_instantiate [("A","{Y} Un H")] insert_is_Un) 1); |
146 by (simp_tac (!simpset addsimps [parts_insert RS sym]) 1); |
141 by (simp_tac (HOL_ss addsimps [parts_Un, Un_assoc]) 1); |
|
142 qed "parts_insert2"; |
147 qed "parts_insert2"; |
143 |
148 |
144 goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; |
149 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)); |
150 by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); |
146 val parts_UN_subset1 = result(); |
151 val parts_UN_subset1 = result(); |
188 goal thy "!!H. [| Y: parts (insert X H); X: parts H |] ==> Y: parts H"; |
193 goal thy "!!H. [| Y: parts (insert X H); X: parts H |] ==> Y: parts H"; |
189 be parts_trans 1; |
194 be parts_trans 1; |
190 by (Fast_tac 1); |
195 by (Fast_tac 1); |
191 qed "parts_cut"; |
196 qed "parts_cut"; |
192 |
197 |
|
198 val parts_insertI = impOfSubs (subset_insertI RS parts_mono); |
|
199 |
193 goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; |
200 goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; |
194 by (fast_tac (!claset addSEs [parts_cut] |
201 by (fast_tac (!claset addSEs [parts_cut] |
195 addIs [impOfSubs (subset_insertI RS parts_mono)]) 1); |
202 addIs [parts_insertI]) 1); |
196 qed "parts_cut_eq"; |
203 qed "parts_cut_eq"; |
197 |
204 |
198 |
205 |
199 (** Rewrite rules for pulling out atomic messages **) |
206 (** Rewrite rules for pulling out atomic messages **) |
200 |
207 |
255 brs prems 1; |
262 brs prems 1; |
256 by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); |
263 by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); |
257 qed "MPair_analz"; |
264 qed "MPair_analz"; |
258 |
265 |
259 AddIs [analz.Inj]; |
266 AddIs [analz.Inj]; |
260 AddSEs [MPair_analz]; |
267 AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) |
261 AddDs [analz.Decrypt]; |
268 AddDs [analz.Decrypt]; |
262 |
269 |
263 Addsimps [analz.Inj]; |
270 Addsimps [analz.Inj]; |
264 |
271 |
265 goal thy "H <= analz(H)"; |
272 goal thy "H <= analz(H)"; |
486 |
493 |
487 (**** Inductive relation "synth" ****) |
494 (**** Inductive relation "synth" ****) |
488 |
495 |
489 AddIs synth.intrs; |
496 AddIs synth.intrs; |
490 |
497 |
|
498 (*Can only produce a nonce or key if it is already known, |
|
499 but can synth a pair or encryption from its components...*) |
|
500 val mk_cases = synth.mk_cases msg.simps; |
|
501 |
|
502 (*NO Agent_synth, as any Agent name can be synthd*) |
|
503 val Nonce_synth = mk_cases "Nonce n : synth H"; |
|
504 val Key_synth = mk_cases "Key K : synth H"; |
|
505 val MPair_synth = mk_cases "{|X,Y|} : synth H"; |
|
506 val Crypt_synth = mk_cases "Crypt X K : synth H"; |
|
507 |
|
508 AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth]; |
|
509 |
491 goal thy "H <= synth(H)"; |
510 goal thy "H <= synth(H)"; |
492 by (Fast_tac 1); |
511 by (Fast_tac 1); |
493 qed "synth_increasing"; |
512 qed "synth_increasing"; |
494 |
513 |
495 (*Monotonicity*) |
514 (*Monotonicity*) |
531 goal thy "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; |
550 goal thy "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; |
532 be synth_trans 1; |
551 be synth_trans 1; |
533 by (Fast_tac 1); |
552 by (Fast_tac 1); |
534 qed "synth_cut"; |
553 qed "synth_cut"; |
535 |
554 |
536 |
|
537 (*Can only produce a nonce or key if it is already known, |
|
538 but can synth a pair or encryption from its components...*) |
|
539 val mk_cases = synth.mk_cases msg.simps; |
|
540 |
|
541 (*NO Agent_synth, as any Agent name can be synthd*) |
|
542 val Nonce_synth = mk_cases "Nonce n : synth H"; |
|
543 val Key_synth = mk_cases "Key K : synth H"; |
|
544 val MPair_synth = mk_cases "{|X,Y|} : synth H"; |
|
545 val Crypt_synth = mk_cases "Crypt X K : synth H"; |
|
546 |
|
547 AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth]; |
|
548 |
|
549 goal thy "Agent A : synth H"; |
555 goal thy "Agent A : synth H"; |
550 by (Fast_tac 1); |
556 by (Fast_tac 1); |
551 qed "Agent_synth"; |
557 qed "Agent_synth"; |
552 |
558 |
553 goal thy "(Nonce N : synth H) = (Nonce N : H)"; |
559 goal thy "(Nonce N : synth H) = (Nonce N : H)"; |
556 |
562 |
557 goal thy "(Key K : synth H) = (Key K : H)"; |
563 goal thy "(Key K : synth H) = (Key K : H)"; |
558 by (Fast_tac 1); |
564 by (Fast_tac 1); |
559 qed "Key_synth_eq"; |
565 qed "Key_synth_eq"; |
560 |
566 |
561 Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq]; |
567 goal thy "!!K. Key K ~: H ==> (Crypt X K : synth H) = (Crypt X K: H)"; |
|
568 by (Fast_tac 1); |
|
569 qed "Crypt_synth_eq"; |
|
570 |
|
571 Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; |
562 |
572 |
563 |
573 |
564 goalw thy [keysFor_def] |
574 goalw thy [keysFor_def] |
565 "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; |
575 "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; |
566 by (Fast_tac 1); |
576 by (Fast_tac 1); |
632 addSEs [impOfSubs analz_mono]) 2); |
642 addSEs [impOfSubs analz_mono]) 2); |
633 by (Full_simp_tac 1); |
643 by (Full_simp_tac 1); |
634 by (Fast_tac 1); |
644 by (Fast_tac 1); |
635 qed "Fake_analz_insert"; |
645 qed "Fake_analz_insert"; |
636 |
646 |
|
647 goal thy "(X: analz H & X: parts H) = (X: analz H)"; |
|
648 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); |
|
649 val analz_conj_parts = result(); |
|
650 |
|
651 goal thy "(X: analz H | X: parts H) = (X: parts H)"; |
|
652 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); |
|
653 val analz_disj_parts = result(); |
|
654 |
|
655 AddIffs [analz_conj_parts, analz_disj_parts]; |
|
656 |
637 (*Without this equation, other rules for synth and analz would yield |
657 (*Without this equation, other rules for synth and analz would yield |
638 redundant cases*) |
658 redundant cases*) |
639 goal thy "({|X,Y|} : synth (analz H)) = \ |
659 goal thy "({|X,Y|} : synth (analz H)) = \ |
640 \ (X : synth (analz H) & Y : synth (analz H))"; |
660 \ (X : synth (analz H) & Y : synth (analz H))"; |
641 by (Fast_tac 1); |
661 by (Fast_tac 1); |