--- a/src/HOL/Auth/OtwayRees.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Thu Dec 19 11:58:39 1996 +0100
@@ -16,7 +16,6 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 15;
(*A "possibility property": there are traces that reach the end*)
@@ -132,9 +131,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 lost ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway lost ==> \
+\ 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 +144,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 lost \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : otway lost \
+\ |] ==> 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 +157,9 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!evs. evs : otway lost ==> \
+\ 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 @@
Addsimps [new_nonces_not_seen];
(*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 lost \
-\ |] ==> length evt < length evs";
+goal thy "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN i) : parts {X}; \
+\ evs : otway lost \
+\ |] ==> 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 lost ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : otway lost ==> \
+\ 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]));
@@ -218,9 +215,9 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ evs : otway lost |] \
-\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
+\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
+\ evs : otway lost |] \
+\ ==> (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 @@
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] 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.
****)
@@ -257,10 +254,10 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 12 secs*)
+by (ALLGOALS (*Takes 11 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])));
(*OR4, OR2, Fake*)
by (EVERY (map spy_analz_tac [5,3,2]));
@@ -271,8 +268,8 @@
goal thy
"!!evs. evs : otway lost ==> \
-\ 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);
@@ -442,8 +439,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]