--- a/src/HOL/Auth/Yahalom2.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Tue Nov 05 11:20:52 1996 +0100
@@ -126,30 +126,19 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The Union over C is essential for the induction! *)
+(*Nobody can have SEEN keys that will be generated in the future. *)
goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evs' --> \
-\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
@@ -166,31 +155,26 @@
...very like new_keys_not_seen*)
goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
-(*Fake and YM4: these messages send unknown (X) components*)
-by (stac insert_commute 2);
-by (Simp_tac 2);
-(*YM4: the only way K could have been used is if it had been seen,
- contradicting new_keys_not_seen*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
+(*Fake and Oops: these messages send unknown (X) components*)
+by (EVERY
+ (map (fast_tac
+ (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
+ addss (!simpset))) [3,1]));
+(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
+by (fast_tac
+ (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
addEs [new_keys_not_seen RSN(2,rev_notE)]
- addss (!simpset)) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+ addDs [Suc_leD]) 1);
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,