--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Dec 19 11:58:39 1996 +0100
@@ -132,9 +132,8 @@
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : otway ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway ==> \
+\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -146,10 +145,10 @@
(*Variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
-\ evs : otway \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : otway \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -159,9 +158,8 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : otway ==> \
-\ length evs <= length evs' --> \
-\ Nonce (newN evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway ==> \
+\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST
(fast_tac (!claset addSEs partsEs
@@ -175,10 +173,10 @@
(*Variant: old messages must contain old nonces!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN evt) : parts {X}; \
-\ evs : otway \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN i) : parts {X}; \
+\ evs : otway \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
@@ -188,9 +186,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : otway ==> \
+\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
(*OR1 and OR3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
@@ -219,8 +216,8 @@
goal thy
"!!evs. [| Says Server B \
\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ evs : otway |] \
-\ ==> (EX evt: otway. K = Key(newK evt)) & \
+\ evs : otway |] \
+\ ==> (EX n. K = Key(newK n)) & \
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
@@ -234,14 +231,14 @@
dtac OR4_analz_sees_Spy 6 THEN
forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -267,12 +264,11 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, lemma]));
-by (ALLGOALS
+by (ALLGOALS (*Takes 18 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
-(** LEVEL 7 **)
(*OR4, OR2, Fake*)
by (EVERY (map spy_analz_tac [5,3,2]));
(*Oops, OR3, Base*)
@@ -282,8 +278,8 @@
goal thy
"!!evs. evs : otway ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -293,7 +289,7 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway ==> \
+ "!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
@@ -332,8 +328,8 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
+ analz_insert_Key_newK]
setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]