--- a/src/HOL/Auth/Event.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Event.ML Thu Sep 26 12:50:48 1996 +0200
@@ -6,7 +6,7 @@
Datatype of events;
inductive relation "traces" for Needham-Schroeder (shared keys)
-Rewrites should not refer to initState (Friend i) -- not in normal form
+Rewrites should not refer to initState (Friend i) -- not in normal form
*)
Addsimps [parts_cut_eq];
@@ -58,7 +58,7 @@
val newN_inject = inj_newN RS injD
and newK_inject = inj_newK RS injD;
AddSEs [shrK_inject, newN_inject, newK_inject,
- fresh_newK RS notE, fresh_newN RS notE];
+ fresh_newK RS notE, fresh_newN RS notE];
Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
Addsimps [fresh_newN, fresh_newK];
@@ -75,7 +75,7 @@
(*Good for talking about Server's initial state*)
goal thy "!!H. H <= Key``E ==> parts H = H";
by (Auto_tac ());
-be parts.induct 1;
+by (etac parts.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "parts_image_subset";
@@ -83,7 +83,7 @@
goal thy "!!H. H <= Key``E ==> analz H = H";
by (Auto_tac ());
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "analz_image_subset";
@@ -118,7 +118,7 @@
qed "analz_own_shrK";
bind_thm ("parts_own_shrK",
- [analz_subset_parts, analz_own_shrK] MRS subsetD);
+ [analz_subset_parts, analz_own_shrK] MRS subsetD);
Addsimps [analz_own_shrK, parts_own_shrK];
@@ -130,7 +130,7 @@
val Says_tracesE = mk_cases "Says A B X # evs: traces";
val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
-val Says_Enemy_tracesE = mk_cases "Says Enemy B X # evs: traces";
+val Says_Spy_tracesE = mk_cases "Says Spy B X # evs: traces";
val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
val Notes_tracesE = mk_cases "Notes A X # evs: traces";
@@ -160,9 +160,9 @@
by (Asm_simp_tac 1);
qed "sees_Friend";
-goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
+goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
by (Simp_tac 1);
-qed "sees_Enemy";
+qed "sees_Spy";
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
@@ -178,19 +178,19 @@
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
\ parts {Y} Un (UN A. parts (sees A evs))";
by (Step_tac 1);
-be rev_mp 1; (*for some reason, split_tac does not work on assumptions*)
+by (etac rev_mp 1); (*for some reason, split_tac does not work on assumptions*)
val ss = (!simpset addsimps [parts_Un, sees_Cons]
- setloop split_tac [expand_if]);
+ setloop split_tac [expand_if]);
by (ALLGOALS (fast_tac (!claset addss ss)));
qed "UN_parts_sees_Says";
-goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
+goal thy "Says A B X : set_of_list evs --> X : sees Spy evs";
by (list.induct_tac "evs" 1);
by (Auto_tac ());
-qed_spec_mp "Says_imp_sees_Enemy";
+qed_spec_mp "Says_imp_sees_Spy";
-Addsimps [Says_imp_sees_Enemy];
-AddIs [Says_imp_sees_Enemy];
+Addsimps [Says_imp_sees_Spy];
+AddIs [Says_imp_sees_Spy];
goal thy "initState C <= Key `` range shrK";
by (agent.induct_tac "C" 1);
@@ -204,7 +204,7 @@
by (list.induct_tac "evs" 1);
by (ALLGOALS Asm_simp_tac);
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
-br conjI 1;
+by (rtac conjI 1);
by (Fast_tac 2);
by (event.induct_tac "a" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
@@ -212,32 +212,32 @@
qed_spec_mp "seesD";
-Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
-Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
+Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy];
+Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
(**** Inductive proofs about traces ****)
-(*The Enemy can see more than anybody else, except for their initial state*)
+(*The Spy can see more than anybody else, except for their initial state*)
goal thy
"!!evs. evs : traces ==> \
-\ sees A evs <= initState A Un sees Enemy evs";
-be traces.induct 1;
+\ sees A evs <= initState A Un sees Spy evs";
+by (etac traces.induct 1);
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]
- addss (!simpset))));
-qed "sees_agent_subset_sees_Enemy";
+ addss (!simpset))));
+qed "sees_agent_subset_sees_Spy";
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs";
-be traces.induct 1;
+by (etac traces.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs";
-be traces.induct 1;
+by (etac traces.induct 1);
by (Auto_tac());
qed "not_Notes";
Addsimps [not_Notes];
@@ -245,60 +245,60 @@
goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
-\ X : parts (sees Enemy evs)";
+\ X : parts (sees Spy evs)";
by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-qed "NS3_msg_in_parts_sees_Enemy";
-
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+qed "NS3_msg_in_parts_sees_Spy";
+
(*** Server keys are not betrayed ***)
-(*Enemy never sees another agent's server key!*)
+(*Spy never sees another agent's server key!*)
goal thy
- "!!evs. [| evs : traces; A ~= Enemy |] ==> \
-\ Key (shrK A) ~: parts (sees Enemy evs)";
-be traces.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+ "!!evs. [| evs : traces; A ~= Spy |] ==> \
+\ Key (shrK A) ~: parts (sees Spy evs)";
+by (etac traces.induct 1);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
by (Auto_tac());
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs synth_analz_parts_insert_subset_Un]) 1);
-qed "Enemy_not_see_shrK";
+ impOfSubs synth_analz_parts_insert_subset_Un]) 1);
+qed "Spy_not_see_shrK";
-bind_thm ("Enemy_not_analz_shrK",
- [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
+bind_thm ("Spy_not_analz_shrK",
+ [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
-Addsimps [Enemy_not_see_shrK,
- not_sym RSN (2, Enemy_not_see_shrK),
- Enemy_not_analz_shrK,
- not_sym RSN (2, Enemy_not_analz_shrK)];
+Addsimps [Spy_not_see_shrK,
+ not_sym RSN (2, Spy_not_see_shrK),
+ Spy_not_analz_shrK,
+ not_sym RSN (2, Spy_not_analz_shrK)];
(*We go to some trouble to preserve R in the 3rd subgoal*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
+goal thy "[| Key (shrK A) : parts (sees Spy evs); \
\ evs : traces; \
-\ A=Enemy ==> R \
+\ A=Spy ==> R \
\ |] ==> R";
-br ccontr 1;
-br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
+by (rtac ccontr 1);
+by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
by (swap_res_tac prems 2);
by (ALLGOALS (fast_tac (!claset addIs prems)));
-qed "Enemy_see_shrK_E";
+qed "Spy_see_shrK_E";
-bind_thm ("Enemy_analz_shrK_E",
- analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
+bind_thm ("Spy_analz_shrK_E",
+ analz_subset_parts RS subsetD RS Spy_see_shrK_E);
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
-AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
+AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
(*No Friend will ever see another agent's server key
- (excluding the Enemy, who might transmit his).
+ (excluding the Spy, who might transmit his).
The Server, of course, knows all server keys.*)
goal thy
- "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \
+ "!!evs. [| evs : traces; A ~= Spy; A ~= Friend j |] ==> \
\ Key (shrK A) ~: parts (sees (Friend j) evs)";
-br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
+by (rtac (sees_agent_subset_sees_Spy RS parts_mono RS contra_subsetD) 1);
by (ALLGOALS Asm_simp_tac);
qed "Friend_not_see_shrK";
@@ -307,11 +307,11 @@
goal thy
"!!evs. evs : traces ==> \
\ (Key (shrK A) \
-\ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \
-\ (A=B | A=Enemy)";
+\ : analz (insert (Key (shrK B)) (sees Spy evs))) = \
+\ (A=B | A=Spy)";
by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
- addIs [impOfSubs (subset_insertI RS analz_mono)]
- addss (!simpset)) 1);
+ addIs [impOfSubs (subset_insertI RS analz_mono)]
+ addss (!simpset)) 1);
qed "shrK_mem_analz";
@@ -328,14 +328,14 @@
goal thy "!!evs. evs : traces ==> \
\ length evs <= length evs' --> \
\ Key (newK evs') ~: (UN C. parts (sees C evs))";
-be traces.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+by (etac traces.induct 1);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
(*auto_tac does not work here, as it performs safe_tac first*)
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
+ impOfSubs parts_insert_subset_Un,
+ Suc_leD]
+ addss (!simpset))));
val lemma = result();
(*Variant needed for the main theorem below*)
@@ -352,14 +352,14 @@
\ Key (newK evt) : parts {X}; \
\ evs : traces \
\ |] ==> length evt < length evs";
-br ccontr 1;
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
- addIs [impOfSubs parts_mono, leI]) 1);
+by (rtac ccontr 1);
+by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
+ addIs [impOfSubs parts_mono, leI]) 1);
qed "Says_imp_old_keys";
goal thy "!!K. newK evs = invKey K ==> newK evs = K";
-br (invKey_eq RS iffD1) 1;
+by (rtac (invKey_eq RS iffD1) 1);
by (Simp_tac 1);
val newK_invKey = result();
@@ -371,24 +371,24 @@
goal thy "!!evs. evs : traces ==> \
\ length evs <= length evs' --> \
\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
-be traces.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+by (etac traces.induct 1);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
by (ALLGOALS Asm_simp_tac);
(*NS1 and NS2*)
map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
(*Fake and NS3*)
map (by o best_tac
(!claset addSDs [newK_invKey]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
- addss (!simpset)))
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
+ addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
+ addss (!simpset)))
[2,1];
(*NS4 and NS5: nonce exchange*)
by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
- addIs [less_SucI, impOfSubs keysFor_mono]
- addss (!simpset addsimps [le_def])) 0));
+ addIs [less_SucI, impOfSubs keysFor_mono]
+ addss (!simpset addsimps [le_def])) 0));
val lemma = result();
goal thy
@@ -398,8 +398,8 @@
qed "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
- [analz_subset_parts RS keysFor_mono,
- new_keys_not_used] MRS contra_subsetD);
+ [analz_subset_parts RS keysFor_mono,
+ new_keys_not_used] MRS contra_subsetD);
Addsimps [new_keys_not_used, new_keys_not_analzd];
@@ -434,14 +434,14 @@
\ X = (Crypt {|K, Agent A|} (shrK B)) & \
\ K' = shrK A & \
\ length evt < length evs)";
-be rev_mp 1;
-be traces.induct 1;
+by (etac rev_mp 1);
+by (etac traces.induct 1);
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
qed "Says_Server_message_form";
(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *)
bind_thm ("not_parts_not_keysFor_analz",
- analz_subset_parts RS keysFor_mono RS contra_subsetD);
+ analz_subset_parts RS keysFor_mono RS contra_subsetD);
@@ -451,13 +451,13 @@
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \
\ evs : traces; i~=k \
\ |] ==> \
-\ K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))";
-be rev_mp 1;
-be traces.induct 1;
+\ K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))";
+by (etac rev_mp 1);
+by (etac traces.induct 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
by (Step_tac 1);
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
-val Enemy_not_see_encrypted_key_lemma = result();
+val Spy_not_see_encrypted_key_lemma = result();
*)
@@ -466,44 +466,44 @@
"!!evs. evs : traces ==> \
\ ALL A NA B K X. \
\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
-\ : parts (sees Enemy evs) & A ~= Enemy --> \
+\ : parts (sees Spy evs) & A ~= Spy --> \
\ (EX evt:traces. K = newK evt & \
\ X = (Crypt {|Key K, Agent A|} (shrK B)))";
-be traces.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+by (etac traces.induct 1);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
by (Step_tac 1);
by (ALLGOALS Asm_full_simp_tac);
(*Remaining cases are Fake and NS2*)
by (fast_tac (!claset addSDs [spec]) 2);
(*Now for the Fake case*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs synth_analz_parts_insert_subset_Un]
- addss (!simpset)) 1);
+ impOfSubs synth_analz_parts_insert_subset_Un]
+ addss (!simpset)) 1);
qed_spec_mp "encrypted_form";
-(*For eliminating the A ~= Enemy condition from the previous result*)
+(*For eliminating the A ~= Spy condition from the previous result*)
goal thy
"!!evs. evs : traces ==> \
\ ALL S A NA B K X. \
\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
\ : set_of_list evs --> \
-\ S = Server | S = Enemy";
-be traces.induct 1;
+\ S = Server | S = Spy";
+by (etac traces.induct 1);
by (ALLGOALS Asm_simp_tac);
(*We are left with NS3*)
-by (subgoal_tac "S = Server | S = Enemy" 1);
+by (subgoal_tac "S = Server | S = Spy" 1);
(*First justify this assumption!*)
by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
by (Step_tac 1);
-bd Says_Server_message_form 1;
+by (dtac Says_Server_message_form 1);
by (ALLGOALS Full_simp_tac);
(*Final case. Clear out needless quantifiers to speed the following step*)
by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
-bd encrypted_form 1;
-br (parts.Inj RS conjI) 1;
+by (dtac encrypted_form 1);
+by (rtac (parts.Inj RS conjI) 1);
auto();
-qed_spec_mp "Server_or_Enemy";
+qed_spec_mp "Server_or_Spy";
(*Describes the form of X when the following message is sent;
@@ -514,12 +514,12 @@
\ evs : traces \
\ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
\ X = (Crypt {|Key K, Agent A|} (shrK B)))";
-by (forward_tac [Server_or_Enemy] 1);
-ba 1;
+by (forward_tac [Server_or_Spy] 1);
+by (assume_tac 1);
by (Step_tac 1);
by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
by (forward_tac [encrypted_form] 1);
-br (parts.Inj RS conjI) 1;
+by (rtac (parts.Inj RS conjI) 1);
by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
qed "Says_S_message_form";
@@ -533,7 +533,7 @@
\ X = (Crypt {|Key K, Agent A|} (shrK B)))";
by (forward_tac [traces_eq_ConsE] 1);
by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
-by (Auto_tac());
+by (Auto_tac());
qed "Says_S_message_form_eq";
@@ -542,8 +542,8 @@
The following is to prove theorems of the form
Key K : analz (insert (Key (newK evt))
- (insert (Key (shrK C)) (sees Enemy evs))) ==>
- Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
+ (insert (Key (shrK C)) (sees Spy evs))) ==>
+ Key K : analz (insert (Key (shrK C)) (sees Spy evs))
A more general formula must be proved inductively.
@@ -555,14 +555,14 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. evs : traces ==> \
-\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees Enemy evs)";
-be traces.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+\ (Crypt X (newK evt)) : parts (sees Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees Spy evs)";
+by (etac traces.induct 1);
+by (dtac NS3_msg_in_parts_sees_Spy 5);
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
(*Deals with Faked messages*)
by (best_tac (!claset addSEs partsEs
- addDs [impOfSubs analz_subset_parts,
+ addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1);
(*NS4 and NS5*)
@@ -591,17 +591,17 @@
goal thy
"!!evs. evs : traces ==> \
\ ALL K E. (Key K : analz (insert (Key (shrK C)) \
-\ (Key``(newK``E) Un (sees Enemy evs)))) = \
+\ (Key``(newK``E) Un (sees Spy evs)))) = \
\ (K : newK``E | \
\ Key K : analz (insert (Key (shrK C)) \
-\ (sees Enemy evs)))";
-be traces.induct 1;
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
+\ (sees Spy evs)))";
+by (etac traces.induct 1);
+by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ @ pushes)
setloop split_tac [expand_if])));
(*Cases NS2 and NS3!! Simple, thanks to auto case splits*)
by (REPEAT (Fast_tac 3));
@@ -615,7 +615,7 @@
"Key K : analz \
\ (synth \
\ (analz (insert (Key (shrK C)) \
-\ (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
+\ (Key``(newK``E) Un (sees Spy evsa)))))" 1);
(*First, justify this subgoal*)
(*Discard formulae for better speed*)
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
@@ -631,28 +631,28 @@
"!!evs. evs : traces ==> \
\ Key K : analz (insert (Key (newK evt)) \
\ (insert (Key (shrK C)) \
-\ (sees Enemy evs))) = \
+\ (sees Spy evs))) = \
\ (K = newK evt | \
\ Key K : analz (insert (Key (shrK C)) \
-\ (sees Enemy evs)))";
+\ (sees Spy evs)))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
+ insert_Key_singleton]) 1);
by (Fast_tac 1);
qed "analz_insert_Key_newK";
(*This says that the Key, K, uniquely identifies the message.
- But if C=Enemy then he could send all sorts of nonsense.*)
+ But if C=Spy then he could send all sorts of nonsense.*)
goal thy
"!!evs. evs : traces ==> \
\ EX X'. ALL C S A Y N B X. \
-\ C ~= Enemy --> \
+\ C ~= Spy --> \
\ Says S A Y : set_of_list evs --> \
\ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \
\ (X = X'))";
-be traces.induct 1;
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
+by (etac traces.induct 1);
+by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
(*NS2: Case split propagates some context to other subgoal...*)
@@ -660,28 +660,28 @@
by (Asm_simp_tac 2);
(*...we assume X is a very new message, and handle this case by contradiction*)
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
- addSEs partsEs
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 2);
+ addSEs partsEs
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 2);
(*NS3: No relevant messages*)
by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2);
(*Fake*)
by (Step_tac 1);
-br exI 1;
-br conjI 1;
-ba 2;
+by (rtac exI 1);
+by (rtac conjI 1);
+by (assume_tac 2);
by (Step_tac 1);
(** LEVEL 12 **)
by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \
-\ : parts (sees Enemy evsa)" 1);
+\ : parts (sees Spy evsa)" 1);
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
- addDs [impOfSubs parts_insert_subset_Un]
+ addDs [impOfSubs parts_insert_subset_Un]
addss (!simpset)) 2);
by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
-bd parts_singleton 1;
+by (dtac parts_singleton 1);
by (Step_tac 1);
-bd seesD 1;
+by (dtac seesD 1);
by (Step_tac 1);
by (Full_simp_tac 2);
by (fast_tac (!claset addSDs [spec]) 1);
@@ -696,25 +696,25 @@
\ Says S' A' \
\ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
\ : set_of_list evs; \
-\ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'";
-bd lemma 1;
-be exE 1;
+\ evs : traces; C ~= Spy; C' ~= Spy |] ==> X = X'";
+by (dtac lemma 1);
+by (etac exE 1);
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
by (Fast_tac 1);
qed "unique_session_keys";
-(*Crucial security property: Enemy does not see the keys sent in msg NS2
+(*Crucial security property: Spy does not see the keys sent in msg NS2
-- even if another key is compromised*)
goal thy
"!!evs. [| Says Server (Friend i) \
\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \
\ evs : traces; Friend i ~= C; Friend j ~= C \
\ |] ==> \
-\ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
-be rev_mp 1;
-be traces.induct 1;
+\ K ~: analz (insert (Key (shrK C)) (sees Spy evs))";
+by (etac rev_mp 1);
+by (etac traces.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
@@ -723,21 +723,21 @@
by (ALLGOALS
(asm_full_simp_tac
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
- analz_insert_Key_newK] @ pushes)
+ analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
(*NS2*)
by (fast_tac (!claset addSEs [less_irrefl]) 2);
(** LEVEL 8 **)
(*Now for the Fake case*)
-br notI 1;
+by (rtac notI 1);
by (subgoal_tac
"Key (newK evt) : \
\ analz (synth (analz (insert (Key (shrK C)) \
-\ (sees Enemy evsa))))" 1);
-be (impOfSubs analz_mono) 2;
+\ (sees Spy evsa))))" 1);
+by (etac (impOfSubs analz_mono) 2);
by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
- impOfSubs synth_increasing,
- impOfSubs analz_increasing]) 0 2);
+ impOfSubs synth_increasing,
+ impOfSubs analz_increasing]) 0 2);
(*Proves the Fake goal*)
by (fast_tac (!claset addss (!simpset)) 1);
@@ -750,12 +750,12 @@
(!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
by (Step_tac 1);
(**LEVEL 18 **)
-bd unique_session_keys 1;
+by (dtac unique_session_keys 1);
by (REPEAT_FIRST assume_tac);
by (ALLGOALS Full_simp_tac);
by (Step_tac 1);
by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1);
-qed "Enemy_not_see_encrypted_key";
+qed "Spy_not_see_encrypted_key";
@@ -772,8 +772,8 @@
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \
\ evs : traces; i~=j \
\ |] ==> K ~: analz (sees (Friend j) evs)";
-br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1;
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
+by (rtac (sees_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Spy_not_see_encrypted_key])));
qed "Friend_not_see_encrypted_key";
goal thy
@@ -786,8 +786,8 @@
by (agent.induct_tac "A" 1);
by (ALLGOALS Simp_tac);
by (asm_simp_tac (!simpset addsimps [eq_sym_conv,
- Friend_not_see_encrypted_key]) 1);
-br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
+ Friend_not_see_encrypted_key]) 1);
+by (rtac ([analz_mono, Spy_not_see_encrypted_key] MRS contra_subsetD) 1);
(* hyp_subst_tac would deletes the equality assumption... *)
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
qed "Agent_not_see_encrypted_key";
@@ -801,7 +801,7 @@
\ |] ==> knownBy evs K <= {Friend i, Server}";
by (Step_tac 1);
-br ccontr 1;
+by (rtac ccontr 1);
by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
qed "knownBy_encrypted_key";
@@ -817,13 +817,13 @@
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \
\ evs : traces; i~=k \
\ |] ==> \
-\ K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))";
-be rev_mp 1;
-be traces.induct 1;
+\ K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))";
+by (etac rev_mp 1);
+by (etac traces.induct 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
by (Step_tac 1);
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
-val Enemy_not_see_encrypted_key_lemma = result();
+val Spy_not_see_encrypted_key_lemma = result();
@@ -835,10 +835,10 @@
with the aid of analz_subset_parts RS contra_subsetD might do the
same thing.*)
goal thy
- "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \
+ "!!evs. [| evs : traces; A ~= Spy; A ~= Friend j |] ==> \
\ Key (shrK A) ~: \
-\ analz (insert (Key (shrK (Friend j))) (sees Enemy evs))";
-br (analz_subset_parts RS contra_subsetD) 1;
+\ analz (insert (Key (shrK (Friend j))) (sees Spy evs))";
+by (rtac (analz_subset_parts RS contra_subsetD) 1);
by (Asm_simp_tac 1);
qed "insert_not_analz_shrK";
@@ -862,15 +862,15 @@
\ : set_of_list evs --> \
\ (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \
\ Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)";
-be traces.induct 1;
+by (etac traces.induct 1);
by (Step_tac 1);
by (ALLGOALS Asm_full_simp_tac);
(*Remaining cases are Fake, NS2 and NS3*)
-by (Fast_tac 2); (*Proves the NS2 case*)
+by (Fast_tac 2); (*Proves the NS2 case*)
by (REPEAT (dtac spec 2));
fe conjE;
-bd mp 2;
+by (dtac mp 2);
by (REPEAT (resolve_tac [refl, conjI] 2));
by (ALLGOALS Asm_full_simp_tac);
@@ -879,7 +879,7 @@
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
-be conjE 2;
+by (etac conjE 2);
by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
(*The NS3 case needs the induction hypothesis twice!
@@ -887,18 +887,18 @@
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2);
by (Fast_tac 3);
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
-be conjE 2;
+by (etac conjE 2);
(*DELETE the first quantified formula: it's now useless*)
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
by (fast_tac (!claset addss (!simpset)) 2);
(*Now for the Fake case*)
-be disjE 1;
+by (etac disjE 1);
(*The subcase of Fake, where the message in question is NOT the most recent*)
by (Best_tac 2);
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
-be Crypt_synth 1;
-be Key_synth 2;
+by (etac Crypt_synth 1);
+by (etac Key_synth 2);
(*Split up the possibilities of that message being synthd...*)
by (Step_tac 1);