--- 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);
--- a/src/HOL/Auth/Event.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Event.thy Thu Sep 26 12:50:48 1996 +0200
@@ -28,7 +28,7 @@
(*Server knows all keys; other agents know only their own*)
initState_Server "initState Server = Key `` range shrK"
initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
- initState_Enemy "initState Enemy = {Key (shrK Enemy)}"
+ initState_Spy "initState Spy = {Key (shrK Spy)}"
(**
For asymmetric keys: server knows all public and private keys,
@@ -45,7 +45,7 @@
primrec sees1 event
(*First agent recalls all that it says, but NOT everything
that is sent to it; it must note such things if/when received*)
- sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})"
+ sees1_Says "sees1 A (Says A' B X) = (if A:{A',Spy} then {X} else {})"
(*part of A's internal state*)
sees1_Notes "sees1 A (Notes A' X) = (if A=A' then {X} else {})"
@@ -89,11 +89,11 @@
(*Initial trace is empty*)
Nil "[]: traces"
- (*The enemy MAY say anything he CAN say. We do not expect him to
+ (*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: traces; B ~= Enemy; X: synth (analz (sees Enemy evs))
- |] ==> (Says Enemy B X) # evs : traces"
+ Fake "[| evs: traces; B ~= Spy; X: synth (analz (sees Spy evs))
+ |] ==> (Says Spy B X) # evs : traces"
(*Alice initiates a protocol run*)
NS1 "[| evs: traces; A ~= Server
@@ -112,7 +112,7 @@
(shrK A))) # evs : traces"
(*We can't assume S=Server. Agent A "remembers" her nonce.
- May assume WLOG that she is NOT the Enemy: the Fake rule
+ May assume WLOG that she is NOT the Spy: the Fake rule
covers this case. Can inductively show A ~= Server*)
NS3 "[| evs: traces; A ~= B;
(Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)))
--- a/src/HOL/Auth/Message.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Message.ML Thu Sep 26 12:50:48 1996 +0200
@@ -14,7 +14,7 @@
goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
by (Step_tac 1);
-br box_equals 1;
+by (rtac box_equals 1);
by (REPEAT (rtac invKey 2));
by (Asm_simp_tac 1);
qed "invKey_eq";
@@ -64,9 +64,9 @@
qed "keysFor_insert_Crypt";
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
- keysFor_insert_Agent, keysFor_insert_Nonce,
- keysFor_insert_Key, keysFor_insert_MPair,
- keysFor_insert_Crypt];
+ keysFor_insert_Agent, keysFor_insert_Nonce,
+ keysFor_insert_Key, keysFor_insert_MPair,
+ keysFor_insert_Crypt];
(**** Inductive relation "parts" ****)
@@ -76,7 +76,7 @@
\ [| X : parts H; Y : parts H |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
-brs prems 1;
+by (resolve_tac prems 1);
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
qed "MPair_parts";
@@ -101,7 +101,7 @@
goal thy "parts{} = {}";
by (Step_tac 1);
-be parts.induct 1;
+by (etac parts.induct 1);
by (ALLGOALS Fast_tac);
qed "parts_empty";
Addsimps [parts_empty];
@@ -113,7 +113,7 @@
(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
-be parts.induct 1;
+by (etac parts.induct 1);
by (ALLGOALS Fast_tac);
qed "parts_singleton";
@@ -125,8 +125,8 @@
val parts_Un_subset1 = result();
goal thy "parts(G Un H) <= parts(G) Un parts(H)";
-br subsetI 1;
-be parts.induct 1;
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (ALLGOALS Fast_tac);
val parts_Un_subset2 = result();
@@ -151,8 +151,8 @@
val parts_UN_subset1 = result();
goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
-br subsetI 1;
-be parts.induct 1;
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (ALLGOALS Fast_tac);
val parts_UN_subset2 = result();
@@ -174,7 +174,7 @@
(** Idempotence and transitivity **)
goal thy "!!H. X: parts (parts H) ==> X: parts H";
-be parts.induct 1;
+by (etac parts.induct 1);
by (ALLGOALS Fast_tac);
qed "parts_partsE";
AddSEs [parts_partsE];
@@ -191,7 +191,7 @@
(*Cut*)
goal thy "!!H. [| Y: parts (insert X H); X: parts H |] ==> Y: parts H";
-be parts_trans 1;
+by (etac parts_trans 1);
by (Fast_tac 1);
qed "parts_cut";
@@ -209,8 +209,8 @@
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
-br subsetI 1;
-be parts.induct 1;
+by (rtac subsetI 1);
+by (etac parts.induct 1);
(*Simplification breaks up equalities between messages;
how to make it work for fast_tac??*)
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -218,45 +218,45 @@
goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
-br subsetI 1;
-be parts.induct 1;
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "parts_insert_Nonce";
goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
-br subsetI 1;
-be parts.induct 1;
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "parts_insert_Key";
goal thy "parts (insert (Crypt X K) H) = \
\ insert (Crypt X K) (parts (insert X H))";
-br equalityI 1;
-br subsetI 1;
-be parts.induct 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (Auto_tac());
-be parts.induct 1;
+by (etac parts.induct 1);
by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
qed "parts_insert_Crypt";
goal thy "parts (insert {|X,Y|} H) = \
\ insert {|X,Y|} (parts (insert X (insert Y H)))";
-br equalityI 1;
-br subsetI 1;
-be parts.induct 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (Auto_tac());
-be parts.induct 1;
+by (etac parts.induct 1);
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
qed "parts_insert_MPair";
Addsimps [parts_insert_Agent, parts_insert_Nonce,
- parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
+ parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
goal thy "parts (Key``N) = Key``N";
by (Auto_tac());
-be parts.induct 1;
+by (etac parts.induct 1);
by (Auto_tac());
qed "parts_image_Key";
@@ -270,7 +270,7 @@
\ [| X : analz H; Y : analz H |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
-brs prems 1;
+by (resolve_tac prems 1);
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
qed "MPair_analz";
@@ -286,7 +286,7 @@
goal thy "analz H <= parts H";
by (rtac subsetI 1);
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS Fast_tac);
qed "analz_subset_parts";
@@ -294,8 +294,8 @@
goal thy "parts (analz H) = parts H";
-br equalityI 1;
-br (analz_subset_parts RS parts_mono RS subset_trans) 1;
+by (rtac equalityI 1);
+by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
by (Simp_tac 1);
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
qed "parts_analz";
@@ -303,7 +303,7 @@
goal thy "analz (parts H) = parts H";
by (Auto_tac());
-be analz.induct 1;
+by (etac analz.induct 1);
by (Auto_tac());
qed "analz_parts";
Addsimps [analz_parts];
@@ -318,7 +318,7 @@
goal thy "analz{} = {}";
by (Step_tac 1);
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS Fast_tac);
qed "analz_empty";
Addsimps [analz_empty];
@@ -337,8 +337,8 @@
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
by (rtac (analz_insert RSN (2, equalityI)) 1);
-br subsetI 1;
-be analz.induct 1;
+by (rtac subsetI 1);
+by (etac analz.induct 1);
(*Simplification breaks up equalities between messages;
how to make it work for fast_tac??*)
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -346,8 +346,8 @@
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
by (rtac (analz_insert RSN (2, equalityI)) 1);
-br subsetI 1;
-be analz.induct 1;
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "analz_insert_Nonce";
@@ -356,18 +356,18 @@
"!!K. K ~: keysFor (analz H) ==> \
\ analz (insert (Key K) H) = insert (Key K) (analz H)";
by (rtac (analz_insert RSN (2, equalityI)) 1);
-br subsetI 1;
-be analz.induct 1;
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "analz_insert_Key";
goal thy "analz (insert {|X,Y|} H) = \
\ insert {|X,Y|} (analz (insert X (insert Y H)))";
-br equalityI 1;
-br subsetI 1;
-be analz.induct 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (Auto_tac());
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
qed "analz_insert_MPair";
@@ -376,15 +376,15 @@
\ analz (insert (Crypt X K) H) = \
\ insert (Crypt X K) (analz H)";
by (rtac (analz_insert RSN (2, equalityI)) 1);
-br subsetI 1;
-be analz.induct 1;
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "analz_insert_Crypt";
goal thy "!!H. Key (invKey K) : analz H ==> \
\ analz (insert (Crypt X K) H) <= \
\ insert (Crypt X K) (analz (insert X H))";
-br subsetI 1;
+by (rtac subsetI 1);
by (eres_inst_tac [("za","x")] analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
val lemma1 = result();
@@ -396,7 +396,7 @@
by (eres_inst_tac [("za","x")] analz.induct 1);
by (Auto_tac());
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
- analz.Decrypt]) 1);
+ analz.Decrypt]) 1);
val lemma2 = result();
goal thy "!!H. Key (invKey K) : analz H ==> \
@@ -415,25 +415,25 @@
\ else insert (Crypt X' K) (analz H))";
by (excluded_middle_tac "Key (invKey K) : analz H " 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt,
- analz_insert_Decrypt])));
+ analz_insert_Decrypt])));
qed "analz_Crypt_if";
Addsimps [analz_insert_Agent, analz_insert_Nonce,
- analz_insert_Key, analz_insert_MPair,
- analz_Crypt_if];
+ analz_insert_Key, analz_insert_MPair,
+ analz_Crypt_if];
(*This rule supposes "for the sake of argument" that we have the key.*)
goal thy "analz (insert (Crypt X K) H) <= \
\ insert (Crypt X K) (analz (insert X H))";
-br subsetI 1;
-be analz.induct 1;
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (Auto_tac());
qed "analz_insert_Crypt_subset";
goal thy "analz (Key``N) = Key``N";
by (Auto_tac());
-be analz.induct 1;
+by (etac analz.induct 1);
by (Auto_tac());
qed "analz_image_Key";
@@ -443,7 +443,7 @@
(** Idempotence and transitivity **)
goal thy "!!H. X: analz (analz H) ==> X: analz H";
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS Fast_tac);
qed "analz_analzE";
AddSEs [analz_analzE];
@@ -460,7 +460,7 @@
(*Cut; Lemma 2 of Lowe*)
goal thy "!!H. [| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
-be analz_trans 1;
+by (etac analz_trans 1);
by (Fast_tac 1);
qed "analz_cut";
@@ -474,39 +474,39 @@
goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
\ |] ==> analz (G Un H) <= analz (G' Un H')";
by (Step_tac 1);
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD])));
qed "analz_subset_cong";
goal thy "!!H. [| analz G = analz G'; analz H = analz H' \
\ |] ==> analz (G Un H) = analz (G' Un H')";
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
- ORELSE' etac equalityE));
+ ORELSE' etac equalityE));
qed "analz_cong";
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
by (asm_simp_tac (!simpset addsimps [insert_def]
- setloop (rtac analz_cong)) 1);
+ setloop (rtac analz_cong)) 1);
qed "analz_insert_cong";
(*If there are no pairs or encryptions then analz does nothing*)
goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt X K ~: H |] ==> \
\ analz H = H";
by (Step_tac 1);
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS Fast_tac);
qed "analz_trivial";
(*Helps to prove Fake cases*)
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
-be analz.induct 1;
+by (etac analz.induct 1);
by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
val lemma = result();
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
by (fast_tac (!claset addIs [lemma]
- addEs [impOfSubs analz_mono]) 1);
+ addEs [impOfSubs analz_mono]) 1);
qed "analz_UN_analz";
Addsimps [analz_UN_analz];
@@ -552,7 +552,7 @@
(** Idempotence and transitivity **)
goal thy "!!H. X: synth (synth H) ==> X: synth H";
-be synth.induct 1;
+by (etac synth.induct 1);
by (ALLGOALS Fast_tac);
qed "synth_synthE";
AddSEs [synth_synthE];
@@ -568,7 +568,7 @@
(*Cut; Lemma 2 of Lowe*)
goal thy "!!H. [| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
-be synth_trans 1;
+by (etac synth_trans 1);
by (Fast_tac 1);
qed "synth_cut";
@@ -601,19 +601,19 @@
(*** Combinations of parts, analz and synth ***)
goal thy "parts (synth H) = parts H Un synth H";
-br equalityI 1;
-br subsetI 1;
-be parts.induct 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac parts.induct 1);
by (ALLGOALS
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
- ::parts.intrs))));
+ ::parts.intrs))));
qed "parts_synth";
Addsimps [parts_synth];
goal thy "analz (synth H) = analz H Un synth H";
-br equalityI 1;
-br subsetI 1;
-be analz.induct 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (best_tac
(!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5);
(*Strange that best_tac just can't hack this one...*)
@@ -621,20 +621,20 @@
qed "analz_synth";
Addsimps [analz_synth];
-(*Hard to prove; still needed now that there's only one Enemy?*)
+(*Hard to prove; still needed now that there's only one Spy?*)
goal thy "analz (UN i. synth (H i)) = \
\ analz (UN i. H i) Un (UN i. synth (H i))";
-br equalityI 1;
-br subsetI 1;
-be analz.induct 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac analz.induct 1);
by (best_tac
(!claset addEs [impOfSubs synth_increasing,
- impOfSubs analz_mono]) 5);
+ impOfSubs analz_mono]) 5);
by (Best_tac 1);
by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
by (deepen_tac (!claset addSEs [analz.Decrypt]
- addIs [analz.Decrypt]) 0 1);
+ addIs [analz.Decrypt]) 0 1);
qed "analz_UN1_synth";
Addsimps [analz_UN1_synth];
@@ -642,21 +642,21 @@
(** For reasoning about the Fake rule in traces **)
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
-br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;
+by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
by (Fast_tac 1);
qed "parts_insert_subset_Un";
(*More specifically for Fake*)
goal thy "!!H. X: synth (analz G) ==> \
\ parts (insert X H) <= synth (analz G) Un parts G Un parts H";
-bd parts_insert_subset_Un 1;
+by (dtac parts_insert_subset_Un 1);
by (Full_simp_tac 1);
by (Deepen_tac 0 1);
qed "Fake_parts_insert";
goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
\ analz (insert X H) <= synth (analz H) Un analz H";
-br subsetI 1;
+by (rtac subsetI 1);
by (subgoal_tac "x : analz (synth (analz H))" 1);
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
addSEs [impOfSubs analz_mono]) 2);
--- a/src/HOL/Auth/Message.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Message.thy Thu Sep 26 12:50:48 1996 +0200
@@ -36,15 +36,15 @@
inductive definition instead of a datatype.*)
datatype (*We allow any number of friendly agents*)
- agent = Server | Friend nat | Enemy
+ agent = Server | Friend nat | Spy
consts
- isEnemy :: agent => bool
+ isSpy :: agent => bool
-primrec isEnemy agent
- isEnemy_Server "isEnemy Server = False"
- isEnemy_Friend "isEnemy (Friend i) = False"
- isEnemy_Enemy "isEnemy Enemy = True"
+primrec isSpy agent
+ isSpy_Server "isSpy Server = False"
+ isSpy_Friend "isSpy (Friend i) = False"
+ isSpy_Spy "isSpy Spy = True"
datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)
msg = Agent agent
--- a/src/HOL/Auth/NS_Shared.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Thu Sep 26 12:50:48 1996 +0200
@@ -19,10 +19,10 @@
(*Weak liveness: there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX N K. EX evs: ns_shared. \
+\ ==> EX N K. EX evs: ns_shared lost. \
\ Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-br (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2;
+by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
@@ -31,19 +31,38 @@
(**** Inductive proofs about ns_shared ****)
-(*The Enemy can see more than anybody else, except for their initial state*)
+goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
+by (rtac subsetI 1);
+by (etac ns_shared.induct 1);
+by (REPEAT_FIRST
+ (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ :: ns_shared.intrs))));
+qed "ns_shared_mono";
+
+
+(*The Spy can see more than anybody else, except for their initial state*)
goal thy
- "!!evs. evs : ns_shared ==> \
-\ sees A evs <= initState A Un sees Enemy evs";
-be ns_shared.induct 1;
+ "!!evs. evs : ns_shared lost ==> \
+\ sees lost A evs <= initState lost A Un sees lost Spy evs";
+by (etac ns_shared.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";
+
+
+(*The Spy can see more than anybody else who's lost their key!*)
+goal thy
+ "!!evs. evs : ns_shared lost ==> \
+\ A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
+by (etac ns_shared.induct 1);
+by (agent.induct_tac "A" 1);
+by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+qed_spec_mp "sees_lost_agent_subset_sees_Spy";
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set_of_list evs";
-be ns_shared.induct 1;
+goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set_of_list evs";
+by (etac ns_shared.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
@@ -51,56 +70,58 @@
(*For reasoning about the encrypted portion of message NS3*)
goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
-\ X : parts (sees Enemy evs)";
+\ X : parts (sees lost 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";
+
+val parts_Fake_tac =
+ dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5;
-(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Enemy never sees another agent's shared key!*)
+(*Spy never sees lost another agent's shared key!*)
goal thy
- "!!evs. [| evs : ns_shared; A ~: bad |] \
-\ ==> Key (shrK A) ~: parts (sees Enemy evs)";
-be ns_shared.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+ "!!evs. [| evs : ns_shared lost; A ~: lost |] \
+\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+by (etac ns_shared.induct 1);
+by parts_Fake_tac;
by (Auto_tac());
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
-qed "Enemy_not_see_shrK";
+ impOfSubs Fake_parts_insert]) 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, Enemy_not_analz_shrK];
+Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
(*We go to some trouble to preserve R in the 3rd and 4th subgoals
As usual fast_tac cannot be used because it uses the equalities too soon*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
-\ evs : ns_shared; \
-\ A:bad ==> R \
+goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : ns_shared lost; \
+\ A:lost ==> 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);
-AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
+AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
goal thy
- "!!evs. evs : ns_shared ==> \
-\ (Key (shrK A) : analz (sees Enemy evs)) = (A : bad)";
+ "!!evs. evs : ns_shared lost ==> \
+\ (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
- addss (!simpset)) 1);
+ addss (!simpset)) 1);
qed "shrK_mem_analz";
Addsimps [shrK_mem_analz];
@@ -114,23 +135,23 @@
standard Fake rule.
The length comparison, and Union over C, are essential for the
induction! *)
-goal thy "!!evs. evs : ns_shared ==> \
+goal thy "!!evs. evs : ns_shared lost ==> \
\ length evs <= length evs' --> \
-\ Key (newK evs') ~: (UN C. parts (sees C evs))";
-be ns_shared.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+by (etac ns_shared.induct 1);
+by parts_Fake_tac;
(*auto_tac does not work here, as it performs safe_tac first*)
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (fast_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*)
goal thy
- "!!evs. [| evs : ns_shared; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees C evs)";
+ "!!evs. [| evs : ns_shared 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";
Addsimps [new_keys_not_seen];
@@ -139,22 +160,22 @@
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
-\ evs : ns_shared \
+\ evs : ns_shared lost \
\ |] ==> length evt < length evs";
-br ccontr 1;
-bd leI 1;
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
+by (rtac ccontr 1);
+by (dtac leI 1);
+by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
addIs [impOfSubs parts_mono]) 1);
qed "Says_imp_old_keys";
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : ns_shared ==> \
+goal thy "!!evs. evs : ns_shared lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
-be ns_shared.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+by (etac ns_shared.induct 1);
+by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*NS1 and NS2*)
map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
@@ -162,25 +183,25 @@
map (by o best_tac
(!claset 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)))
+ 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 [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
- "!!evs. [| evs : ns_shared; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees C evs))";
+ "!!evs. [| evs : ns_shared 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";
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];
@@ -190,13 +211,13 @@
(*Describes the form of K, X and K' when the Server sends this message.*)
goal thy
"!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
-\ evs : ns_shared |] \
-\ ==> (EX evt:ns_shared. \
+\ evs : ns_shared lost |] \
+\ ==> (EX evt: ns_shared lost. \
\ K = Key(newK evt) & \
\ X = (Crypt {|K, Agent A|} (shrK B)) & \
\ K' = shrK A)";
-be rev_mp 1;
-be ns_shared.induct 1;
+by (etac rev_mp 1);
+by (etac ns_shared.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "Says_Server_message_form";
@@ -205,24 +226,24 @@
"parts" strengthens the induction hyp for proving the Fake case. The
assumptions on A are needed to prevent its being a Faked message.*)
goal thy
- "!!evs. evs : ns_shared ==> \
+ "!!evs. evs : ns_shared lost ==> \
\ Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A) \
-\ : parts (sees Enemy evs) & \
-\ A ~: bad --> \
-\ (EX evt:ns_shared. K = newK evt & \
+\ : parts (sees lost Spy evs) & \
+\ A ~: lost --> \
+\ (EX evt: ns_shared lost. K = newK evt & \
\ X = (Crypt {|Key K, Agent A|} (shrK B)))";
-be ns_shared.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+by (etac ns_shared.induct 1);
+by parts_Fake_tac;
(*Fake case*)
by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
+ addDs [impOfSubs analz_subset_parts]
+ addss (!simpset)) 2);
by (Auto_tac());
val lemma = result() RS mp;
(*The following theorem is proved by cases. If the message was sent with a
- bad key then the Enemy reads it -- even if he didn't send it in the first
+ bad key then the Spy reads it -- even if he didn't send it in the first
place.*)
@@ -231,16 +252,16 @@
Use Says_Server_message_form if applicable.*)
goal thy
"!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
-\ : set_of_list evs; evs : ns_shared |] \
-\ ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
+\ : set_of_list evs; evs : ns_shared lost |] \
+\ ==> (EX evt: ns_shared lost. K = newK evt & length evt < length evs & \
\ X = (Crypt {|Key K, Agent A|} (shrK B))) | \
-\ X : analz (sees Enemy evs)";
-by (excluded_middle_tac "A : bad" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
- addss (!simpset)) 2);
+\ X : analz (sees lost Spy evs)";
+by (excluded_middle_tac "A : lost" 1);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+ addss (!simpset)) 2);
by (forward_tac [lemma] 1);
by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
by (fast_tac (!claset addIs [Says_imp_old_keys] addss (!simpset)) 1);
qed "Says_S_message_form";
@@ -249,8 +270,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
- Key K : analz (sees Enemy evs)
+ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -261,15 +282,15 @@
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
- "!!evs. evs : ns_shared ==> \
-\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees Enemy evs)";
-be ns_shared.induct 1;
-bd NS3_msg_in_parts_sees_Enemy 5;
+ "!!evs. evs : ns_shared lost ==> \
+\ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
+by (etac ns_shared.induct 1);
+by parts_Fake_tac;
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
(*Deals with Faked messages*)
by (best_tac (!claset addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]
+ addDs [impOfSubs parts_insert_subset_Un]
addss (!simpset)) 2);
(*Base, NS4 and NS5*)
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -284,8 +305,8 @@
Delsimps [image_Un];
Addsimps [image_Un RS sym];
-goal thy "insert (Key (newK x)) (sees A evs) = \
-\ Key `` (newK``{x}) Un (sees A evs)";
+goal thy "insert (Key (newK x)) (sees lost A evs) = \
+\ Key `` (newK``{x}) Un (sees lost A evs)";
by (Fast_tac 1);
val insert_Key_singleton = result();
@@ -307,36 +328,36 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : ns_shared ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
-\ (K : newK``E | Key K : analz (sees Enemy evs))";
-be ns_shared.induct 1;
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
+ "!!evs. evs : ns_shared lost ==> \
+\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
+\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+by (etac ns_shared.induct 1);
+by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
by (REPEAT_FIRST (resolve_tac [allI, lemma]));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ @ pushes)
setloop split_tac [expand_if])));
(** LEVEL 5 **)
(*NS3, Fake subcase*)
-by (enemy_analz_tac 5);
+by (spy_analz_tac 5);
(*Cases NS2 and NS3!! Simple, thanks to auto case splits*)
by (REPEAT (Fast_tac 3));
(*Fake case*) (** LEVEL 7 **)
-by (enemy_analz_tac 2);
+by (spy_analz_tac 2);
(*Base case*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
qed_spec_mp "analz_image_newK";
goal thy
- "!!evs. evs : ns_shared ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
-\ (K = newK evt | Key K : analz (sees Enemy evs))";
+ "!!evs. evs : ns_shared lost ==> \
+\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
+\ (K = newK evt | Key K : analz (sees lost 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";
@@ -347,32 +368,32 @@
fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
goal thy
- "!!evs. evs : ns_shared ==> \
+ "!!evs. evs : ns_shared lost ==> \
\ EX X'. ALL A X N B. \
-\ A ~: bad --> \
-\ Crypt {|N, Agent B, Key K, X|} (shrK A) : parts (sees Enemy evs) --> \
+\ A ~: lost --> \
+\ Crypt {|N, Agent B, Key K, X|} (shrK A) : parts (sees lost Spy evs) --> \
\ X=X'";
-by (Simp_tac 1); (*Miniscoping*)
-be ns_shared.induct 1;
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
+by (Simp_tac 1); (*Miniscoping*)
+by (etac ns_shared.induct 1);
+by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
- imp_conj_distrib, parts_insert_sees])));
+ imp_conj_distrib, parts_insert_sees])));
by (REPEAT_FIRST (eresolve_tac [exE,disjE]));
(*NS2: Cextraction of K = newK evsa to global context...*)
(** LEVEL 5 **)
by (excluded_middle_tac "K = newK evsa" 3);
by (Asm_simp_tac 3);
-be exI 3;
+by (etac exI 3);
(*...we assume X is a very new message, and handle this case by contradiction*)
by (fast_tac (!claset addSEs partsEs
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 3);
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 3);
(*Base, Fake, NS3*) (** LEVEL 9 **)
by (REPEAT_FIRST ex_strip_tac);
-bd synth.Inj 4;
+by (dtac synth.Inj 4);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
- addss (!simpset))));
+ addss (!simpset))));
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
@@ -383,52 +404,54 @@
\ Says S' A' \
\ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
\ : set_of_list evs; \
-\ evs : ns_shared; C ~= Enemy; C ~: bad; C' ~: bad |] ==> X = X'";
-bd lemma 1;
-be exE 1;
+\ evs : ns_shared lost; C ~: lost; C' ~: lost |] ==> X = X'";
+by (dtac lemma 1);
+by (etac exE 1);
(*Duplicate the assumption*)
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "unique_session_keys";
-(** Crucial secrecy property: Enemy does not see the keys sent in msg NS2 **)
+(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : ns_shared; evt: ns_shared |] \
+ "!!evs. [| A ~: lost; B ~: lost; \
+\ evs : ns_shared lost; evt: ns_shared lost |] \
\ ==> Says Server A \
\ (Crypt {|N, Agent B, Key(newK evt), \
\ Crypt {|Key(newK evt), Agent A|} (shrK B)|} (shrK A)) \
\ : set_of_list evs --> \
-\ Key(newK evt) ~: analz (sees Enemy evs)";
-be ns_shared.induct 1;
+\ Key(newK evt) ~: analz (sees lost Spy evs)";
+by (etac ns_shared.induct 1);
by (ALLGOALS
(asm_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 addIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 2);
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 2);
(*Fake case*)
-by (enemy_analz_tac 1);
+by (spy_analz_tac 1);
(*NS3: that message from the Server was sent earlier*)
by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
by (Step_tac 1);
-by (enemy_analz_tac 2); (*Prove the Fake subcase*)
+by (REPEAT_FIRST assume_tac);
+by (spy_analz_tac 2); (*Prove the Fake subcase*)
by (asm_full_simp_tac
(!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
by (Step_tac 1);
-(**LEVEL 9 **)
-by (excluded_middle_tac "Aa : bad" 1);
-(*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
-bd (Says_imp_sees_Enemy RS analz.Inj) 2;
+(**LEVEL 10 **)
+by (excluded_middle_tac "Aa : lost" 1);
+(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
+by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
by (fast_tac (!claset addSDs [analz.Decrypt]
- addss (!simpset)) 2);
-(*So now we have Aa ~: bad *)
-bd unique_session_keys 1;
+ addss (!simpset)) 2);
+(*So now we have Aa ~: lost *)
+by (dtac unique_session_keys 1);
by (Auto_tac ());
val lemma = result() RS mp RSN(2,rev_notE);
@@ -437,9 +460,22 @@
goal thy
"!!evs. [| Says Server A \
\ (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
-\ A ~: bad; B ~: bad; evs : ns_shared \
+\ A ~: lost; B ~: lost; evs : ns_shared lost \
\ |] ==> \
-\ K ~: analz (sees Enemy evs)";
+\ K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
-qed "Enemy_not_see_encrypted_key";
+qed "Spy_not_see_encrypted_key";
+
+
+goal thy
+ "!!evs. [| C ~: {A,B,Server}; \
+\ Says Server A \
+\ (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
+\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
+\ ==> K ~: analz (sees lost C evs)";
+by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
+by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
+by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
+by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
+qed "Agent_not_see_encrypted_key";
--- a/src/HOL/Auth/NS_Shared.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Thu Sep 26 12:50:48 1996 +0200
@@ -12,57 +12,58 @@
NS_Shared = Shared +
-consts ns_shared :: "event list set"
-inductive ns_shared
+consts ns_shared :: "agent set => event list set"
+inductive "ns_shared lost"
intrs
(*Initial trace is empty*)
- Nil "[]: ns_shared"
+ Nil "[]: ns_shared lost"
- (*The enemy MAY say anything he CAN say. We do not expect him to
+ (*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: ns_shared; B ~= Enemy; X: synth (analz (sees Enemy evs)) |]
- ==> Says Enemy B X # evs : ns_shared"
+ Fake "[| evs: ns_shared lost; B ~= Spy;
+ X: synth (analz (sees lost Spy evs)) |]
+ ==> Says Spy B X # evs : ns_shared lost"
(*Alice initiates a protocol run, requesting to talk to any B*)
- NS1 "[| evs: ns_shared; A ~= Server |]
+ NS1 "[| evs: ns_shared lost; A ~= Server |]
==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
- : ns_shared"
+ : ns_shared lost"
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
- NS2 "[| evs: ns_shared; A ~= B; A ~= Server;
+ NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server;
Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
==> Says Server A
(Crypt {|Nonce NA, Agent B, Key (newK evs),
(Crypt {|Key (newK evs), Agent A|} (shrK B))|}
- (shrK A)) # evs : ns_shared"
+ (shrK A)) # evs : ns_shared lost"
(*We can't assume S=Server. Agent A "remembers" her nonce.
Can inductively show A ~= Server*)
- NS3 "[| evs: ns_shared; A ~= B;
+ NS3 "[| evs: ns_shared lost; A ~= B;
Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
: set_of_list evs;
Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
- ==> Says A B X # evs : ns_shared"
+ ==> Says A B X # evs : ns_shared lost"
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
- NS4 "[| evs: ns_shared; A ~= B;
+ NS4 "[| evs: ns_shared lost; A ~= B;
Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
- ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
+ ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
(*Alice responds with the Nonce, if she has seen the key before.
- We do NOT use N-1 or similar as the Enemy cannot spoof such things.
- Allowing the Enemy to add or subtract 1 allows him to send ALL
+ We do NOT use N-1 or similar as the Spy cannot spoof such things.
+ Allowing the Spy to add or subtract 1 allows him to send ALL
nonces. Instead we distinguish the messages by sending the
nonce twice.*)
- NS5 "[| evs: ns_shared; A ~= B;
+ NS5 "[| evs: ns_shared lost; A ~= B;
Says B' A (Crypt (Nonce N) K) : set_of_list evs;
Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
: set_of_list evs |]
- ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
+ ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared lost"
end
--- a/src/HOL/Auth/OtwayRees.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Sep 26 12:50:48 1996 +0200
@@ -22,11 +22,11 @@
(*Weak liveness: there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: otway. \
+\ ==> EX K. EX NA. EX evs: otway lost. \
\ Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
+by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
@@ -35,19 +35,37 @@
(**** Inductive proofs about otway ****)
-(*The Enemy can see more than anybody else, except for their initial state*)
+goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
+by (rtac subsetI 1);
+by (etac otway.induct 1);
+by (REPEAT_FIRST
+ (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ :: otway.intrs))));
+qed "otway_mono";
+
+
+(*The Spy can see more than anybody else, except for their initial state*)
goal thy
- "!!evs. evs : otway ==> \
-\ sees A evs <= initState A Un sees Enemy evs";
-be otway.induct 1;
+ "!!evs. evs : otway lost ==> \
+\ sees lost A evs <= initState lost A Un sees lost Spy evs";
+by (etac otway.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";
+
+(*The Spy can see more than anybody else who's lost their key!*)
+goal thy
+ "!!evs. evs : otway lost ==> \
+\ A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
+by (etac otway.induct 1);
+by (agent.induct_tac "A" 1);
+by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
+qed_spec_mp "sees_lost_agent_subset_sees_Spy";
(*Nobody sends themselves messages*)
-goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
-be otway.induct 1;
+goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
+by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
@@ -57,69 +75,78 @@
(** For reasoning about the encrypted portion of messages **)
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
-\ X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "OR2_analz_sees_Enemy";
+\ X : analz (sees lost Spy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+qed "OR2_analz_sees_Spy";
goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
-\ X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "OR4_analz_sees_Enemy";
+\ X : analz (sees lost Spy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+qed "OR4_analz_sees_Spy";
goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
-\ K : parts (sees Enemy evs)";
+\ K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-qed "Reveal_parts_sees_Enemy";
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+qed "Reveal_parts_sees_Spy";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
argument as for the Fake case. This is possible for most, but not all,
proofs: Fake does not invent new nonces (as in OR2), and of course Fake
- messages originate from the Enemy. *)
+ messages originate from the Spy. *)
+bind_thm ("OR2_parts_sees_Spy",
+ OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_sees_Spy",
+ OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+
+(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
+ harder to complete, since simplification does less for us.*)
val parts_Fake_tac =
- forward_tac [OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 4 THEN
- forward_tac [OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 6 THEN
- forward_tac [Reveal_parts_sees_Enemy] 7;
+ let val tac = forw_inst_tac [("lost","lost")]
+ in tac OR2_parts_sees_Spy 4 THEN
+ tac OR4_parts_sees_Spy 6 THEN
+ tac Reveal_parts_sees_Spy 7
+ end;
-(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
goal thy
- "!!evs. [| evs : otway; A ~: bad |] \
-\ ==> Key (shrK A) ~: parts (sees Enemy evs)";
-be otway.induct 1;
+ "!!evs. [| evs : otway lost; A ~: lost |] \
+\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+by (etac otway.induct 1);
by parts_Fake_tac;
by (Auto_tac());
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
-qed "Enemy_not_see_shrK";
+ impOfSubs Fake_parts_insert]) 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, Enemy_not_analz_shrK];
+Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
(*We go to some trouble to preserve R in the 3rd and 4th subgoals
As usual fast_tac cannot be used because it uses the equalities too soon*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
-\ evs : otway; \
-\ A:bad ==> R \
+goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : otway lost; \
+\ A:lost ==> 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);
-AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
+AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
(*** Future keys can't be seen or used! ***)
@@ -129,23 +156,23 @@
but should go by similar reasoning every time. Hardest case is the
standard Fake rule.
The Union over C is essential for the induction! *)
-goal thy "!!evs. evs : otway ==> \
+goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evs' --> \
-\ Key (newK evs') ~: (UN C. parts (sees C evs))";
-be otway.induct 1;
+\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+by (etac otway.induct 1);
by parts_Fake_tac;
(*auto_tac does not work here, as it performs safe_tac first*)
by (ALLGOALS Asm_simp_tac);
by (REPEAT_FIRST (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*)
goal thy
- "!!evs. [| evs : otway; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees C evs)";
+ "!!evs. [| evs : otway 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";
Addsimps [new_keys_not_seen];
@@ -154,37 +181,37 @@
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
-\ evs : otway \
+\ evs : otway lost \
\ |] ==> length evt < length evs";
-br ccontr 1;
-bd leI 1;
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
+by (rtac ccontr 1);
+by (dtac leI 1);
+by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
addIs [impOfSubs parts_mono]) 1);
qed "Says_imp_old_keys";
(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
-goal thy "!!evs. evs : otway ==> \
+goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: (UN C. parts (sees C evs))";
-be otway.induct 1;
+\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
+by (etac otway.induct 1);
(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [ parts_insert2]
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
addcongs [disj_cong])));
by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
+ addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ 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 : otway; length evs <= length evs' |] \
-\ ==> Nonce (newN evs') ~: parts (sees C evs)";
+ "!!evs. [| evs : otway lost; length evs <= length evs' |] \
+\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
by (fast_tac (!claset addDs [lemma]) 1);
qed "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
@@ -193,21 +220,21 @@
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Nonce (newN evt) : parts {X}; \
-\ evs : otway \
+\ evs : otway lost \
\ |] ==> length evt < length evs";
-br ccontr 1;
-bd leI 1;
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
- addIs [impOfSubs parts_mono]) 1);
+by (rtac ccontr 1);
+by (dtac leI 1);
+by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
+ addIs [impOfSubs parts_mono]) 1);
qed "Says_imp_old_nonces";
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway ==> \
+goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
-be otway.induct 1;
+\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+by (etac otway.induct 1);
by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*OR1 and OR3*)
@@ -217,26 +244,26 @@
(map
(best_tac
(!claset 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)))
+ 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)))
[3,2,1]));
(*Reveal: dummy message*)
by (best_tac (!claset addEs [new_keys_not_seen RSN(2,rev_notE)]
- addIs [less_SucI, impOfSubs keysFor_mono]
- addss (!simpset addsimps [le_def])) 1);
+ addIs [less_SucI, impOfSubs keysFor_mono]
+ addss (!simpset addsimps [le_def])) 1);
val lemma = result();
goal thy
- "!!evs. [| evs : otway; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees C evs))";
+ "!!evs. [| evs : otway 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";
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];
@@ -247,8 +274,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
- Key K : analz (sees Enemy evs)
+ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -259,15 +286,15 @@
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
- "!!evs. evs : otway ==> \
-\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees Enemy evs)";
-be otway.induct 1;
+ "!!evs. evs : otway lost ==> \
+\ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
+by (etac otway.induct 1);
by parts_Fake_tac;
-by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
+by (ALLGOALS Asm_simp_tac);
(*Deals with Faked messages*)
by (best_tac (!claset addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]
+ addDs [impOfSubs parts_insert_subset_Un]
addss (!simpset)) 2);
(*Base case and Reveal*)
by (Auto_tac());
@@ -282,8 +309,8 @@
Delsimps [image_Un];
Addsimps [image_Un RS sym];
-goal thy "insert (Key (newK x)) (sees A evs) = \
-\ Key `` (newK``{x}) Un (sees A evs)";
+goal thy "insert (Key (newK x)) (sees lost A evs) = \
+\ Key `` (newK``{x}) Un (sees lost A evs)";
by (Fast_tac 1);
val insert_Key_singleton = result();
@@ -295,10 +322,10 @@
(*This lets us avoid analyzing the new message -- unless we have to!*)
(*NEEDED??*)
-goal thy "synth (analz (sees Enemy evs)) <= \
-\ synth (analz (sees Enemy (Says A B X # evs)))";
+goal thy "synth (analz (sees lost Spy evs)) <= \
+\ synth (analz (sees lost Spy (Says A B X # evs)))";
by (Simp_tac 1);
-br (subset_insertI RS analz_mono RS synth_mono) 1;
+by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
qed "synth_analz_thin";
AddIs [impOfSubs synth_analz_thin];
@@ -312,16 +339,17 @@
assumptions on A are needed to prevent its being a Faked message. (Based
on NS_Shared/Says_S_message_form) *)
goal thy
- "!!evs. evs: otway ==> \
-\ Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
-\ A ~: bad --> \
-\ (EX evt:otway. K = newK evt)";
-be otway.induct 1;
+ "!!evs. evs: otway lost ==> \
+\ Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
+\ A ~: lost --> \
+\ (EX evt: otway lost. K = newK evt)";
+by (etac otway.induct 1);
by parts_Fake_tac;
-by (Auto_tac());
+by (ALLGOALS Asm_simp_tac);
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
+ impOfSubs Fake_parts_insert]) 2);
+by (Auto_tac());
val lemma = result() RS mp;
@@ -329,14 +357,14 @@
OR reduces it to the Fake case.*)
goal thy
"!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \
-\ evs : otway |] \
-\ ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
-by (excluded_middle_tac "A : bad" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
- addss (!simpset)) 2);
+\ evs : otway lost |] \
+\ ==> (EX evt: otway lost. K = newK evt) | Key K : analz (sees lost Spy evs)";
+by (excluded_middle_tac "A : lost" 1);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+ addss (!simpset)) 2);
by (forward_tac [lemma] 1);
by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
by (Fast_tac 1);
qed "Reveal_message_form";
@@ -352,34 +380,34 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
-\ (K : newK``E | Key K : analz (sees Enemy evs))";
-be otway.induct 1;
-bd OR2_analz_sees_Enemy 4;
-bd OR4_analz_sees_Enemy 6;
-bd Reveal_message_form 7;
+ "!!evs. evs : otway lost ==> \
+\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
+\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+by (etac otway.induct 1);
+by (dtac OR2_analz_sees_Spy 4);
+by (dtac OR4_analz_sees_Spy 6);
+by (dtac Reveal_message_form 7);
by (REPEAT_FIRST (ares_tac [allI, lemma]));
by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
by (ALLGOALS (*Takes 28 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ @ pushes)
setloop split_tac [expand_if])));
(** LEVEL 7 **)
(*Reveal case 2, OR4, OR2, Fake*)
-by (EVERY (map enemy_analz_tac [7,5,3,2]));
+by (EVERY (map spy_analz_tac [7,5,3,2]));
(*Reveal case 1, OR3, Base*)
by (Auto_tac());
qed_spec_mp "analz_image_newK";
goal thy
- "!!evs. evs : otway ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
-\ (K = newK evt | Key K : analz (sees Enemy evs))";
+ "!!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))";
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";
@@ -389,13 +417,13 @@
fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
goal thy
- "!!evs. evs : otway ==> \
+ "!!evs. evs : otway lost ==> \
\ EX A' B' NA' NB'. ALL A B NA NB. \
\ Says Server B \
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
\ A=A' & B=B' & NA=NA' & NB=NB'";
-be otway.induct 1;
+by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
(*Remaining cases: OR3 and OR4*)
@@ -406,8 +434,8 @@
by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
(*...we assume X is a very new message, and handle this case by contradiction*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
- delrules [conjI] (*prevent split-up into 4 subgoals*)
- addss (!simpset addsimps [parts_insertI])) 1);
+ delrules [conjI] (*prevent split-up into 4 subgoals*)
+ addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
goal thy
@@ -419,9 +447,9 @@
\ {|NA', Crypt {|NA', K|} (shrK A'), \
\ Crypt {|NB', K|} (shrK B')|} \
\ : set_of_list evs; \
-\ evs : otway |] \
+\ evs : otway lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
-bd lemma 1;
+by (dtac lemma 1);
by (REPEAT (etac exE 1));
(*Duplicate the assumption*)
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
@@ -434,18 +462,18 @@
(*Only OR1 can have caused such a part of a message to appear.*)
goal thy
- "!!evs. [| A ~: bad; evs : otway |] \
+ "!!evs. [| A ~: lost; evs : otway lost |] \
\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
-\ : parts (sees Enemy evs) --> \
+\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
\ : set_of_list evs";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 2);
+ impOfSubs Fake_parts_insert]) 2);
by (Auto_tac());
qed_spec_mp "Crypt_imp_OR1";
@@ -453,16 +481,16 @@
(** The Nonce NA uniquely identifies A's message. **)
goal thy
- "!!evs. [| evs : otway; A ~: bad |] \
+ "!!evs. [| evs : otway lost; A ~: lost |] \
\ ==> EX B'. ALL B. \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs) --> \
+\ Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) --> \
\ B = B'";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 2);
+ impOfSubs Fake_parts_insert]) 2);
(*Base case*)
by (fast_tac (!claset addss (!simpset)) 1);
by (Step_tac 1);
@@ -471,16 +499,16 @@
by (Asm_simp_tac 1);
by (Fast_tac 1);
by (best_tac (!claset addSEs partsEs
- addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1);
+ addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1);
val lemma = result();
goal thy
- "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs); \
-\ Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees Enemy evs); \
-\ evs : otway; A ~: bad |] \
+ "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs); \
+\ Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees lost Spy evs); \
+\ evs : otway lost; A ~: lost |] \
\ ==> B = C";
-bd lemma 1;
-ba 1;
+by (dtac lemma 1);
+by (assume_tac 1);
by (etac exE 1);
(*Duplicate the assumption*)
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
@@ -494,22 +522,22 @@
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see OtwayRees_Bad.*)
goal thy
- "!!evs. [| A ~: bad; evs : otway |] \
+ "!!evs. [| A ~: lost; evs : otway lost |] \
\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
-\ : parts (sees Enemy evs) --> \
+\ : parts (sees lost Spy evs) --> \
\ Crypt {|NA', NA, Agent A', Agent A|} (shrK A) \
-\ ~: parts (sees Enemy evs)";
-be otway.induct 1;
+\ ~: parts (sees lost Spy evs)";
+by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2])));
(*It is hard to generate this proof in a reasonable amount of time*)
by (step_tac (!claset addSEs [MPair_parts, nonce_not_seen_now]
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
by (REPEAT_FIRST (fast_tac (!claset (*40 seconds??*)
- addSDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un]
- addss (!simpset))));
+ addSDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un]
+ addss (!simpset))));
by (REPEAT_FIRST (fast_tac (!claset
- addSEs (partsEs@[nonce_not_seen_now])
+ addSEs (partsEs@[nonce_not_seen_now])
addSDs [impOfSubs parts_insert_subset_Un]
addss (!simpset))));
qed_spec_mp"no_nonce_OR1_OR2";
@@ -519,8 +547,8 @@
(*If the encrypted message appears, and A has used Nonce NA to start a run,
then it originated with the Server!*)
goal thy
- "!!evs. [| A ~: bad; evs : otway |] \
-\ ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
+ "!!evs. [| A ~: lost; A ~= Spy; evs : otway lost |] \
+\ ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
\ Says A B {|Nonce NA, Agent A, Agent B, \
\ Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} \
\ : set_of_list evs --> \
@@ -529,43 +557,43 @@
\ Crypt {|Nonce NA, Key K|} (shrK A), \
\ Crypt {|Nonce NB, Key K|} (shrK B)|} \
\ : set_of_list evs)";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
+ impOfSubs Fake_parts_insert]) 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
- addss (!simpset)) 1);
+ addSEs partsEs
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 1);
(*OR3 and OR4*) (** LEVEL 5 **)
(*OR4*)
by (REPEAT (Safe_step_tac 2));
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
by (fast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs partsEs
- addDs [Says_imp_sees_Enemy RS parts.Inj]) 2);
+ addEs partsEs
+ addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
(*OR3*) (** LEVEL 8 **)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
by (step_tac (!claset delrules [disjCI, impCE]) 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
addSEs [MPair_parts]
addEs [unique_OR1_nonce]) 1);
by (fast_tac (!claset addSEs [MPair_parts]
- addSDs [Says_imp_sees_Enemy RS parts.Inj]
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)]
- delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
+ delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
qed_spec_mp "Crypt_imp_Server_msg";
(*Crucial property: if A receives B's OR4 message and the nonce NA agrees
then the key really did come from the Server! CANNOT prove this of the
- bad form of this protocol, even though we can prove
- Enemy_not_see_encrypted_key*)
+ lost form of this protocol, even though we can prove
+ Spy_not_see_encrypted_key*)
goal thy
- "!!evs. [| A ~: bad; evs : otway |] \
+ "!!evs. [| A ~: lost; A ~= Spy; evs : otway lost |] \
\ ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
\ : set_of_list evs --> \
\ Says A B {|Nonce NA, Agent A, Agent B, \
@@ -576,32 +604,30 @@
\ Crypt {|Nonce NA, Key K|} (shrK A), \
\ Crypt {|Nonce NB, Key K|} (shrK B)|} \
\ : set_of_list evs)";
-be otway.induct 1;
+by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
(*OR2*)
by (Fast_tac 3);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addEs [Says_imp_old_nonces RS less_irrefl]
- addss (!simpset)) 2);
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 2);
(*Fake, OR4*) (** LEVEL 4 **)
by (step_tac (!claset delrules [impCE]) 1);
by (ALLGOALS Asm_simp_tac);
by (Fast_tac 4);
by (fast_tac (!claset addSIs [Crypt_imp_OR1]
- addEs partsEs
- addDs [Says_imp_sees_Enemy RS parts.Inj]) 3);
+ addEs partsEs
+ addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
(** LEVEL 8 **)
(*Still subcases of Fake and OR4*)
by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
- addDs [impOfSubs analz_subset_parts]) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
- addEs partsEs
- addDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-val lemma = result();
-
+ addEs partsEs
+ addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
val OR4_imp_Says_Server_A =
- lemma RSN (2, rev_mp) RS mp |> standard;
+ result() RSN (2, rev_mp) RS mp |> standard;
@@ -610,48 +636,48 @@
"!!evs. [| Says Server B \
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ evs : otway |] \
-\ ==> (EX evt:otway. K = Key(newK evt)) & \
+\ evs : otway lost |] \
+\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
\ (EX i. NA = Nonce i)";
-be rev_mp 1;
-be otway.induct 1;
+by (etac rev_mp 1);
+by (etac otway.induct 1);
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
qed "Says_Server_message_form";
-(** Crucial secrecy property: Enemy does not see the keys sent in msg OR3 **)
+(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 **)
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : otway; evt : otway |] \
+ "!!evs. [| A ~: lost; B ~: lost; evs : otway lost; evt : otway lost |] \
\ ==> Says Server B \
\ {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
\ Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
-\ Says A Enemy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
-\ Key(newK evt) ~: analz (sees Enemy evs)";
-be otway.induct 1;
-bd OR2_analz_sees_Enemy 4;
-bd OR4_analz_sees_Enemy 6;
+\ Says A Spy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
+\ Key(newK evt) ~: analz (sees lost Spy evs)";
+by (etac otway.induct 1);
+by (dtac OR2_analz_sees_Spy 4);
+by (dtac OR4_analz_sees_Spy 6);
by (forward_tac [Reveal_message_form] 7);
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
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])));
(** LEVEL 6 **)
(*OR3*)
by (fast_tac (!claset addSIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 3);
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 3);
(*Reveal case 2, OR4, OR2, Fake*)
-by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' enemy_analz_tac));
+by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
(*Reveal case 1*) (** LEVEL 8 **)
-by (excluded_middle_tac "Aa : bad" 1);
-(*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
-bd (Says_imp_sees_Enemy RS analz.Inj) 2;
+by (excluded_middle_tac "Aa : lost" 1);
+(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
+by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
-(*So now we have Aa ~: bad *)
-by (dresolve_tac [OR4_imp_Says_Server_A] 1);
+(*So now we have Aa ~: lost *)
+by (dtac OR4_imp_Says_Server_A 1);
by (REPEAT (assume_tac 1));
by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -660,32 +686,46 @@
"!!evs. [| Says Server B \
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ Says A Enemy {|NA, K|} ~: set_of_list evs; \
-\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> K ~: analz (sees Enemy evs)";
+\ Says A Spy {|NA, K|} ~: set_of_list evs; \
+\ A ~: lost; B ~: lost; evs : otway lost |] \
+\ ==> K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
-qed "Enemy_not_see_encrypted_key";
+qed "Spy_not_see_encrypted_key";
+
+goal thy
+ "!!evs. [| C ~: {A,B,Server}; \
+\ Says Server B \
+\ {|NA, Crypt {|NA, K|} (shrK A), \
+\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ Says A Spy {|NA, K|} ~: set_of_list evs; \
+\ A ~: lost; B ~: lost; evs : otway lost |] \
+\ ==> K ~: analz (sees lost C evs)";
+by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
+by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
+by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
+by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
+qed "Agent_not_see_encrypted_key";
(** A session key uniquely identifies a pair of senders in the message
encrypted by a good agent C. **)
goal thy
- "!!evs. evs : otway ==> \
+ "!!evs. evs : otway lost ==> \
\ EX A B. ALL C N. \
-\ C ~: bad --> \
-\ Crypt {|N, Key K|} (shrK C) : parts (sees Enemy evs) --> \
+\ C ~: lost --> \
+\ Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
\ C=A | C=B";
-by (Simp_tac 1); (*Miniscoping*)
-be otway.induct 1;
-bd OR2_analz_sees_Enemy 4;
-bd OR4_analz_sees_Enemy 6;
-(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
+by (Simp_tac 1); (*Miniscoping*)
+by (etac otway.induct 1);
+by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4);
+by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6);
+(*spy_analz_tac just does not work here: it is an entirely different proof!*)
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
- imp_conj_distrib, parts_insert_sees,
- parts_insert2])));
+ imp_conj_distrib, parts_insert_sees,
+ parts_insert2])));
by (REPEAT_FIRST (etac exE));
(*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
by (excluded_middle_tac "K = newK evsa" 4);
@@ -693,13 +733,16 @@
by (REPEAT (ares_tac [exI] 4));
(*...we prove this case by contradiction: the key is too new!*)
by (fast_tac (!claset addSEs partsEs
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 4);
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 4);
(*Base, Fake, OR2, OR4*)
by (REPEAT_FIRST ex_strip_tac);
-bd synth.Inj 4;
-bd synth.Inj 3;
+by (dtac synth.Inj 4);
+by (dtac synth.Inj 3);
(*Now in effect there are three Fake cases*)
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
- addss (!simpset))));
+ delrules [disjCI, disjE]
+ addss (!simpset))));
qed "key_identifies_senders";
+
+
--- a/src/HOL/Auth/OtwayRees.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Sep 26 12:50:48 1996 +0200
@@ -14,40 +14,41 @@
OtwayRees = Shared +
-consts otway :: "event list set"
-inductive otway
+consts otway :: "agent set => event list set"
+inductive "otway lost"
intrs
(*Initial trace is empty*)
- Nil "[]: otway"
+ Nil "[]: otway lost"
- (*The enemy MAY say anything he CAN say. We do not expect him to
+ (*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) |]
- ==> Says Enemy B X # evs : otway"
+ Fake "[| evs: otway lost; B ~= Spy;
+ X: synth (analz (sees lost Spy evs)) |]
+ ==> Says Spy B X # evs : otway lost"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway; A ~= B; B ~= Server |]
+ OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
==> Says A B {|Nonce (newN evs), Agent A, Agent B,
Crypt {|Nonce (newN evs), Agent A, Agent B|}
(shrK A) |}
- # evs : otway"
+ # evs : otway lost"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
We modify the published protocol by NOT encrypting NB.*)
- OR2 "[| evs: otway; B ~= Server;
+ OR2 "[| evs: otway lost; B ~= Server;
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
Crypt {|Nonce NA, Nonce (newN evs),
Agent A, Agent B|} (shrK B)|}
- # evs : otway"
+ # evs : otway lost"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs: otway; B ~= Server;
+ OR3 "[| evs: otway lost; B ~= Server;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A),
@@ -57,27 +58,27 @@
{|Nonce NA,
Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
- # evs : otway"
+ # evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway; A ~= B; B ~= Server;
+ OR4 "[| evs: otway lost; A ~= B; B ~= Server;
Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
: set_of_list evs;
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|}
(shrK B)|}
: set_of_list evs |]
- ==> Says B A {|Nonce NA, X|} # evs : otway"
+ ==> Says B A {|Nonce NA, X|} # evs : otway lost"
(*This message models possible leaks of session keys. Alice's Nonce
identifies the protocol run.*)
- Reveal "[| evs: otway; A ~= Enemy;
+ Reveal "[| evs: otway lost; A ~= Spy;
Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
: set_of_list evs;
Says A B {|Nonce NA, Agent A, Agent B,
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
: set_of_list evs |]
- ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
+ ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
end
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Sep 26 12:50:48 1996 +0200
@@ -10,7 +10,7 @@
Proc. Royal Soc. 426 (1989)
This file illustrates the consequences of such errors. We can still prove
-impressive-looking properties such as Enemy_not_see_encrypted_key, yet the
+impressive-looking properties such as Spy_not_see_encrypted_key, yet the
protocol is open to a middleperson attack. Attempting to prove some key lemmas
indicates the possibility of this attack.
*)
@@ -28,7 +28,7 @@
\ Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
+by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
@@ -37,19 +37,19 @@
(**** Inductive proofs about otway ****)
-(*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 : otway ==> \
-\ sees A evs <= initState A Un sees Enemy evs";
-be otway.induct 1;
+\ sees A evs <= initState A Un sees Spy evs";
+by (etac otway.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 : otway ==> ALL A X. Says A A X ~: set_of_list evs";
-be otway.induct 1;
+by (etac otway.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
@@ -59,69 +59,69 @@
(** For reasoning about the encrypted portion of messages **)
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
-\ X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "OR2_analz_sees_Enemy";
+\ X : analz (sees Spy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+qed "OR2_analz_sees_Spy";
goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
-\ X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "OR4_analz_sees_Enemy";
+\ X : analz (sees Spy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+qed "OR4_analz_sees_Spy";
goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
-\ K : parts (sees Enemy evs)";
+\ K : parts (sees Spy evs)";
by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-qed "Reveal_parts_sees_Enemy";
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+qed "Reveal_parts_sees_Spy";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
argument as for the Fake case. This is possible for most, but not all,
proofs: Fake does not invent new nonces (as in OR2), and of course Fake
- messages originate from the Enemy. *)
+ messages originate from the Spy. *)
val parts_Fake_tac =
- dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
- dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
- dtac Reveal_parts_sees_Enemy 7;
+ dtac (OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 4 THEN
+ dtac (OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 6 THEN
+ dtac Reveal_parts_sees_Spy 7;
-(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
goal thy
"!!evs. [| evs : otway; A ~: bad |] \
-\ ==> Key (shrK A) ~: parts (sees Enemy evs)";
-be otway.induct 1;
+\ ==> Key (shrK A) ~: parts (sees Spy evs)";
+by (etac otway.induct 1);
by parts_Fake_tac;
by (Auto_tac());
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
-qed "Enemy_not_see_shrK";
+ impOfSubs Fake_parts_insert]) 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, Enemy_not_analz_shrK];
+Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
(*We go to some trouble to preserve R in the 3rd and 4th subgoals
As usual fast_tac cannot be used because it uses the equalities too soon*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
+goal thy "[| Key (shrK A) : parts (sees Spy evs); \
\ evs : otway; \
\ A:bad ==> 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);
-AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
+AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
(*** Future keys can't be seen or used! ***)
@@ -134,14 +134,14 @@
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
\ Key (newK evs') ~: (UN C. parts (sees C evs))";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
(*auto_tac does not work here, as it performs safe_tac first*)
by (ALLGOALS Asm_simp_tac);
by (REPEAT_FIRST (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*)
@@ -158,9 +158,9 @@
\ Key (newK evt) : parts {X}; \
\ evs : otway \
\ |] ==> 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";
@@ -169,17 +169,17 @@
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
\ Nonce (newN evs') ~: (UN C. parts (sees C evs))";
-be otway.induct 1;
+by (etac otway.induct 1);
(*auto_tac does not work here, as it performs safe_tac first*)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [de_Morgan_disj]
addcongs [conj_cong])));
by (REPEAT_FIRST (fast_tac (!claset (*60 seconds???*)
- addSEs [MPair_parts]
- addDs [Says_imp_sees_Enemy RS parts.Inj,
- impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
+ addSEs [MPair_parts]
+ addDs [Says_imp_sees_Spy RS parts.Inj,
+ impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un,
+ Suc_leD]
+ addss (!simpset))));
val lemma = result();
(*Variant needed for the main theorem below*)
@@ -196,9 +196,9 @@
\ Nonce (newN evt) : parts {X}; \
\ evs : otway \
\ |] ==> length evt < length evs";
-br ccontr 1;
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
- addIs [impOfSubs parts_mono, leI]) 1);
+by (rtac ccontr 1);
+by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
+ addIs [impOfSubs parts_mono, leI]) 1);
qed "Says_imp_old_nonces";
@@ -207,7 +207,7 @@
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*OR1 and OR3*)
@@ -217,15 +217,15 @@
(map
(best_tac
(!claset 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)))
+ 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)))
[3,2,1]));
(*Reveal: dummy message*)
by (best_tac (!claset addEs [new_keys_not_seen RSN(2,rev_notE)]
- addIs [less_SucI, impOfSubs keysFor_mono]
- addss (!simpset addsimps [le_def])) 1);
+ addIs [less_SucI, impOfSubs keysFor_mono]
+ addss (!simpset addsimps [le_def])) 1);
val lemma = result();
goal thy
@@ -235,8 +235,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];
@@ -247,8 +247,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
- Key K : analz (sees Enemy evs)
+ Key K : analz (insert (Key (newK evt)) (sees Spy evs)) ==>
+ Key K : analz (sees Spy evs)
A more general formula must be proved inductively.
@@ -260,14 +260,14 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. evs : otway ==> \
-\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees Enemy evs)";
-be otway.induct 1;
+\ (Crypt X (newK evt)) : parts (sees Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees Spy evs)";
+by (etac otway.induct 1);
by parts_Fake_tac;
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)) 2);
(*Base case and Reveal*)
@@ -296,10 +296,10 @@
(*This lets us avoid analyzing the new message -- unless we have to!*)
(*NEEDED??*)
-goal thy "synth (analz (sees Enemy evs)) <= \
-\ synth (analz (sees Enemy (Says A B X # evs)))";
+goal thy "synth (analz (sees Spy evs)) <= \
+\ synth (analz (sees Spy (Says A B X # evs)))";
by (Simp_tac 1);
-br (subset_insertI RS analz_mono RS synth_mono) 1;
+by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
qed "synth_analz_thin";
AddIs [impOfSubs synth_analz_thin];
@@ -314,15 +314,15 @@
on NS_Shared/Says_S_message_form) *)
goal thy
"!!evs. evs: otway ==> \
-\ Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
+\ Crypt {|N, Key K|} (shrK A) : parts (sees Spy evs) & \
\ A ~: bad --> \
\ (EX evt:otway. K = newK evt)";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
by (Auto_tac());
(*Deals with Fake message*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
+ impOfSubs Fake_parts_insert]) 1);
val lemma = result() RS mp;
@@ -331,13 +331,13 @@
goal thy
"!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \
\ evs : otway |] \
-\ ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
+\ ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Spy evs)";
by (excluded_middle_tac "A : bad" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
- addss (!simpset)) 2);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
+ addss (!simpset)) 2);
by (forward_tac [lemma] 1);
by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
by (Fast_tac 1);
qed "Reveal_message_form";
@@ -354,22 +354,22 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
"!!evs. evs : otway ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
-\ (K : newK``E | Key K : analz (sees Enemy evs))";
-be otway.induct 1;
-bd OR2_analz_sees_Enemy 4;
-bd OR4_analz_sees_Enemy 6;
-bd Reveal_message_form 7;
+\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Spy evs))) = \
+\ (K : newK``E | Key K : analz (sees Spy evs))";
+by (etac otway.induct 1);
+by (dtac OR2_analz_sees_Spy 4);
+by (dtac OR4_analz_sees_Spy 6);
+by (dtac Reveal_message_form 7);
by (REPEAT_FIRST (ares_tac [allI, lemma]));
by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
by (ALLGOALS (*Takes 28 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ @ pushes)
setloop split_tac [expand_if])));
(** LEVEL 7 **)
(*Reveal case 2, OR4, OR2, Fake*)
-by (EVERY (map enemy_analz_tac [7,5,3,2]));
+by (EVERY (map spy_analz_tac [7,5,3,2]));
(*Reveal case 1, OR3, Base*)
by (Auto_tac());
qed_spec_mp "analz_image_newK";
@@ -377,10 +377,10 @@
goal thy
"!!evs. evs : otway ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
-\ (K = newK evt | Key K : analz (sees Enemy evs))";
+\ Key K : analz (insert (Key (newK evt)) (sees Spy evs)) = \
+\ (K = newK evt | Key K : analz (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";
@@ -393,8 +393,8 @@
\ evs : otway |] \
\ ==> (EX evt:otway. K = Key(newK evt)) & \
\ (EX i. NA = Nonce i)";
-be rev_mp 1;
-be otway.induct 1;
+by (etac rev_mp 1);
+by (etac otway.induct 1);
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
qed "Says_Server_message_form";
@@ -402,34 +402,34 @@
(*Crucial security property, but not itself enough to guarantee correctness!
The need for quantification over N, C seems to indicate the problem.
Omitting the Reveal message from the description deprives us of even
- this clue. *)
+ this clue. *)
goal thy
"!!evs. [| A ~: bad; B ~: bad; evs : otway; evt : otway |] \
\ ==> Says Server B \
\ {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
\ Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
-\ (ALL N C. Says C Enemy {|N, Key(newK evt)|} ~: set_of_list evs) --> \
-\ Key(newK evt) ~: analz (sees Enemy evs)";
-be otway.induct 1;
-bd OR2_analz_sees_Enemy 4;
-bd OR4_analz_sees_Enemy 6;
-bd Reveal_message_form 7;
+\ (ALL N C. Says C Spy {|N, Key(newK evt)|} ~: set_of_list evs) --> \
+\ Key(newK evt) ~: analz (sees Spy evs)";
+by (etac otway.induct 1);
+by (dtac OR2_analz_sees_Spy 4);
+by (dtac OR4_analz_sees_Spy 6);
+by (dtac Reveal_message_form 7);
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
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])));
(** LEVEL 6 **)
(*Reveal case 1*)
by (Fast_tac 5);
(*OR3*)
by (fast_tac (!claset addSIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 3);
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 3);
(*Reveal case 2, OR4, OR2, Fake*)
-br conjI 3;
-by (REPEAT (enemy_analz_tac 1));
+by (rtac conjI 3);
+by (REPEAT (spy_analz_tac 1));
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -439,12 +439,12 @@
"!!evs. [| Says Server B \
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ (ALL N C. Says C Enemy {|N, K|} ~: set_of_list evs); \
+\ (ALL N C. Says C Spy {|N, K|} ~: set_of_list evs); \
\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> K ~: analz (sees Enemy evs)";
+\ ==> K ~: analz (sees Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
-qed "Enemy_not_see_encrypted_key";
+qed "Spy_not_see_encrypted_key";
(*** Attempting to prove stronger properties ***)
@@ -460,7 +460,7 @@
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
\ A=A' & B=B' & NA=NA' & NB=NB'";
-be otway.induct 1;
+by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
by (Step_tac 1);
(*Remaining cases: OR3 and OR4*)
@@ -471,8 +471,8 @@
by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
(*...we assume X is a very new message, and handle this case by contradiction*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
- delrules [conjI] (*prevent split-up into 4 subgoals*)
- addss (!simpset addsimps [parts_insertI])) 1);
+ delrules [conjI] (*prevent split-up into 4 subgoals*)
+ addss (!simpset addsimps [parts_insertI])) 1);
val lemma = result();
@@ -487,7 +487,7 @@
\ : set_of_list evs; \
\ evs : otway |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
-bd lemma 1;
+by (dtac lemma 1);
by (REPEAT (etac exE 1));
(*Duplicate the assumption*)
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
@@ -499,16 +499,16 @@
goal thy
"!!evs. [| A ~: bad; A ~= B; evs : otway |] \
\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
-\ : parts (sees Enemy evs) --> \
+\ : parts (sees Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
\ : set_of_list evs";
-be otway.induct 1;
+by (etac otway.induct 1);
by parts_Fake_tac;
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 2);
+ impOfSubs Fake_parts_insert]) 2);
by (Auto_tac());
qed_spec_mp "Crypt_imp_OR1";
@@ -517,7 +517,7 @@
substituting some other nonce NA' for NB.*)
goal thy
"!!evs. [| A ~: bad; evs : otway |] \
-\ ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
+\ ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Spy evs) --> \
\ Says A B {|Nonce NA, Agent A, Agent B, \
\ Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} \
\ : set_of_list evs --> \
@@ -526,23 +526,23 @@
\ Crypt {|Nonce NA, Key K|} (shrK A), \
\ Crypt {|Nonce NB, Key K|} (shrK B)|} \
\ : set_of_list evs)";
-be otway.induct 1;
+by (etac otway.induct 1);
fun ftac rl = forward_tac [rl];
by (
- ftac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
- ftac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
- ftac Reveal_parts_sees_Enemy 7);
+ ftac (OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 4 THEN
+ ftac (OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 6 THEN
+ ftac Reveal_parts_sees_Spy 7);
(* by parts_Fake_tac; ?*)
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
+ impOfSubs Fake_parts_insert]) 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_nonces RS less_irrefl]
- addss (!simpset)) 1);
+ addSEs partsEs
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 1);
(*OR3 and OR4*) (** LEVEL 5 **)
(*OR4*)
by (REPEAT (Safe_step_tac 2));
@@ -550,7 +550,7 @@
by (best_tac (!claset addSDs [parts_cut]) 3);
by (forward_tac [Crypt_imp_OR1] 2);
by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 4);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 4);
by (REPEAT (Fast_tac 2));
(*OR3*) (** LEVEL 11 **)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -577,14 +577,14 @@
\ Crypt {|Nonce NA, Key K|} (shrK A), \
\ Crypt {|Nonce NB, Key K|} (shrK B)|} \
\ : set_of_list evs)";
-be otway.induct 1;
+by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
(*OR2*)
by (Fast_tac 3);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
- addEs [Says_imp_old_nonces RS less_irrefl]
- addss (!simpset)) 2);
+ addEs [Says_imp_old_nonces RS less_irrefl]
+ addss (!simpset)) 2);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [all_conj_distrib, de_Morgan_disj, de_Morgan_conj])));
(*Fake, OR4*) (** LEVEL 5 **)
@@ -593,7 +593,7 @@
by (fast_tac (!claset addSDs [spec]) 4);
by (forward_tac [Crypt_imp_OR1] 3);
by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 5);
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 5);
by (REPEAT (Fast_tac 3));
(** LEVEL 11 **)
(*Fake (??) and OR4*)
@@ -607,12 +607,12 @@
(** First, two lemmas for the Fake, OR2 and OR4 cases **)
goal thy
- "!!evs. [| X : synth (analz (sees Enemy evs)); \
+ "!!evs. [| X : synth (analz (sees Spy evs)); \
\ Crypt X' (shrK C) : parts{X}; \
\ C ~: bad; evs : otway |] \
-\ ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
+\ ==> Crypt X' (shrK C) : parts (sees Spy evs)";
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
- addDs [impOfSubs parts_insert_subset_Un]
+ addDs [impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1);
qed "Crypt_Fake_parts";
@@ -620,12 +620,12 @@
"!!evs. [| Crypt X' K : parts (sees A evs); evs : otway |] \
\ ==> EX S S' Y. Says S S' Y : set_of_list evs & \
\ Crypt X' K : parts {Y}";
-bd parts_singleton 1;
+by (dtac parts_singleton 1);
by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
qed "Crypt_parts_singleton";
(*The Key K uniquely identifies a pair of senders in the message encrypted by
- C, but if C=Enemy then he could send all sorts of nonsense.*)
+ C, but if C=Spy then he could send all sorts of nonsense.*)
goal thy
"!!evs. evs : otway ==> \
\ EX A B. ALL C. \
@@ -633,33 +633,33 @@
\ (ALL S S' X. Says S S' X : set_of_list evs --> \
\ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
by (Simp_tac 1);
-be otway.induct 1;
-bd OR2_analz_sees_Enemy 4;
-bd OR4_analz_sees_Enemy 6;
+by (etac otway.induct 1);
+by (dtac OR2_analz_sees_Spy 4);
+by (dtac OR4_analz_sees_Spy 6);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
by (REPEAT_FIRST (etac exE));
(*OR4*)
by (ex_strip_tac 4);
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts,
- Crypt_parts_singleton]) 4);
+ Crypt_parts_singleton]) 4);
(*OR3: Case split propagates some context to other subgoal...*)
- (** LEVEL 8 **)
+ (** LEVEL 8 **)
by (excluded_middle_tac "K = newK evsa" 3);
by (Asm_simp_tac 3);
by (REPEAT (ares_tac [exI] 3));
(*...we prove this case by contradiction: the key is too new!*)
by (fast_tac (!claset addIs [parts_insertI]
- addSEs partsEs
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 3);
+ addSEs partsEs
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 3);
(*OR2*) (** LEVEL 12 **)
-(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
+(*spy_analz_tac just does not work here: it is an entirely different proof!*)
by (ex_strip_tac 2);
by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
by (Simp_tac 2);
by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts,
- Crypt_parts_singleton]) 2);
+ Crypt_parts_singleton]) 2);
(*Fake*) (** LEVEL 16 **)
by (ex_strip_tac 1);
by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
--- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Sep 26 12:50:48 1996 +0200
@@ -18,11 +18,11 @@
(*Initial trace is empty*)
Nil "[]: otway"
- (*The enemy MAY say anything he CAN say. We do not expect him to
+ (*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) |]
- ==> Says Enemy B X # evs : otway"
+ Fake "[| evs: otway; B ~= Spy; X: synth (analz (sees Spy evs)) |]
+ ==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
OR1 "[| evs: otway; A ~= B; B ~= Server |]
@@ -68,12 +68,12 @@
(*This message models possible leaks of session keys. Alice's Nonce
identifies the protocol run.*)
- Reveal "[| evs: otway; A ~= Enemy;
+ Reveal "[| evs: otway; A ~= Spy;
Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
: set_of_list evs;
Says A B {|Nonce NA, Agent A, Agent B,
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
: set_of_list evs |]
- ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
+ ==> Says A Spy {|Nonce NA, Key K|} # evs : otway"
end
--- a/src/HOL/Auth/Shared.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Shared.ML Thu Sep 26 12:50:48 1996 +0200
@@ -6,11 +6,41 @@
Theory of Shared Keys (common to all symmetric-key protocols)
Server keys; initial states of agents; new nonces and keys; function "sees"
+*)
+
-*)
+(****************DELETE****************)
-Addsimps [parts_cut_eq];
+local
+ fun string_of (a,0) = a
+ | string_of (a,i) = a ^ "_" ^ string_of_int i;
+in
+ fun freeze_thaw th =
+ let val fth = freezeT th
+ val {prop,sign,...} = rep_thm fth
+ fun mk_inst (Var(v,T)) =
+ (cterm_of sign (Var(v,T)),
+ cterm_of sign (Free(string_of v, T)))
+ val insts = map mk_inst (term_vars prop)
+ fun thaw th' =
+ th' |> forall_intr_list (map #2 insts)
+ |> forall_elim_list (map #1 insts)
+ in (instantiate ([],insts) fth, thaw) end;
+end;
+fun defer_tac i state =
+ let val (state',thaw) = freeze_thaw state
+ val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
+ val hyp::hyps' = drop(i-1,hyps)
+ in implies_intr hyp (implies_elim_list state' (map assume hyps))
+ |> implies_intr_list (take(i-1,hyps) @ hyps')
+ |> thaw
+ |> Sequence.single
+ end
+ handle Bind => Sequence.null;
+
+
+
(*GOALS.ML??*)
fun prlim n = (goals_limit:=n; pr());
@@ -47,42 +77,26 @@
(*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq,
- fresh_newN, fresh_newK];
+AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goal thy "newK evs ~= shrK B";
-by (subgoal_tac "newK evs = shrK B --> \
-\ Key (newK evs) : parts (initState B)" 1);
-by (Fast_tac 1);
-by (agent.induct_tac "B" 1);
-by (auto_tac (!claset addIs [range_eqI], !simpset addsimps [bad_def]));
-qed "newK_neq_shrK";
-
Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
-(*Good for talking about Server's initial state*)
-goal thy "!!H. H <= Key``E ==> parts H = H";
+goal thy "Key (newK evs) ~: parts (initState lost B)";
+by (agent.induct_tac "B" 1);
by (Auto_tac ());
-be parts.induct 1;
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "parts_image_subset";
-
-bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
+qed "newK_notin_initState";
-goal thy "!!H. H <= Key``E ==> analz H = H";
+goal thy "Nonce (newN evs) ~: parts (initState lost B)";
+by (agent.induct_tac "B" 1);
by (Auto_tac ());
-be analz.induct 1;
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "analz_image_subset";
+qed "newN_notin_initState";
-bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
+AddIffs [newK_notin_initState, newN_notin_initState];
-Addsimps [parts_image_Key, analz_image_Key];
-
-goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
+goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
by (agent.induct_tac "C" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
qed "keysFor_parts_initState";
@@ -99,106 +113,105 @@
qed "shrK_notin_image_newK";
Addsimps [shrK_notin_image_newK];
+
+(*** Function "sees" ***)
+
+goal thy
+ "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
+by (list.induct_tac "evs" 1);
+by (agent.induct_tac "A" 1);
+by (event.induct_tac "a" 2);
+by (Auto_tac ());
+qed "sees_mono";
+
(*Agents see their own shared keys!*)
-goal thy "Key (shrK A) : sees A evs";
+goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
by (list.induct_tac "evs" 1);
by (agent.induct_tac "A" 1);
-by (auto_tac (!claset, !simpset addsimps [bad_def]));
-qed "sees_own_shrK";
-
-(*Enemy sees shared keys of bad agents!*)
-goal thy "!!i. A: bad ==> Key (shrK A) : sees Enemy evs";
-by (list.induct_tac "evs" 1);
-by (auto_tac (!claset, !simpset addsimps [bad_def]));
-qed "Enemy_sees_bad";
-
-AddSIs [sees_own_shrK, Enemy_sees_bad];
+by (Auto_tac ());
+qed_spec_mp "sees_own_shrK";
-goal thy "Enemy: bad";
-by (simp_tac (!simpset addsimps [bad_def]) 1);
-qed "Enemy_in_bad";
-
-AddIffs [Enemy_in_bad];
+(*Spy sees shared keys of lost agents!*)
+goal thy "!!i. A: lost ==> Key (shrK A) : sees lost Spy evs";
+by (list.induct_tac "evs" 1);
+by (Auto_tac());
+qed "Spy_sees_bad";
-goal thy "!!A. A ~: bad ==> A ~= Enemy";
-by (Fast_tac 1);
-qed "not_bad_imp_not_Enemy";
+AddSIs [sees_own_shrK, Spy_sees_bad];
+
-AddIffs [Enemy_in_bad];
+(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
-(** Specialized rewrite rules for (sees A (Says...#evs)) **)
-
-goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
+goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)";
by (Simp_tac 1);
qed "sees_own";
goal thy "!!A. Server ~= A ==> \
-\ sees Server (Says A B X # evs) = sees Server evs";
+\ sees lost Server (Says A B X # evs) = sees lost Server evs";
by (Asm_simp_tac 1);
qed "sees_Server";
goal thy "!!A. Friend i ~= A ==> \
-\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
+\ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
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 lost Spy (Says A B X # evs) = insert X (sees lost 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)";
+goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
qed "sees_Says_subset_insert";
-goal thy "sees A evs <= sees A (Says A' B X # evs)";
+goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
qed "sees_subset_sees_Says";
-(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
-goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
-\ parts {Y} Un (UN A. parts (sees A evs))";
+(*Pushing Unions into parts; one of the A's equals B, and thus sees lost Y*)
+goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
+\ parts {Y} Un (UN A. parts (sees lost 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 lost 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";
+goal thy "initState lost C <= Key `` range shrK";
by (agent.induct_tac "C" 1);
by (Auto_tac ());
qed "initState_subset";
-goal thy "X : sees C evs --> \
+goal thy "X : sees lost C evs --> \
\ (EX A B. Says A B X : set_of_list evs) | \
\ (EX A. X = Key (shrK A))";
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])));
by (ALLGOALS Fast_tac);
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 ****)
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();
@@ -229,26 +242,25 @@
(*Analysis of Fake cases and of messages that forward unknown parts
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*)
-fun enemy_analz_tac i =
+fun spy_analz_tac i =
SELECT_GOAL
(EVERY [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac (!simpset setloop split_tac [expand_if]) 1,
- REPEAT (resolve_tac [impI,notI] 1),
- dtac (impOfSubs Fake_analz_insert) 1,
- eresolve_tac [asm_rl, synth.Inj] 1,
- Fast_tac 1,
- Asm_full_simp_tac 1,
- IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
- ]) i;
+ (REPEAT o CHANGED)
+ (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (!simpset setloop split_tac [expand_if]) 1,
+ REPEAT (resolve_tac [impI,notI] 1),
+ dtac (impOfSubs Fake_analz_insert) 1,
+ eresolve_tac [asm_rl, synth.Inj] 1,
+ Fast_tac 1,
+ Asm_full_simp_tac 1,
+ IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
+ ]) i;
-(** Simplifying parts (insert X (sees A evs))
- = parts {X} Un parts (sees A evs) -- since general case loops*)
+(** Simplifying parts (insert X (sees lost A evs))
+ = parts {X} Un parts (sees lost A evs) -- since general case loops*)
val parts_insert_sees =
- parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees A evs")]
+ parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees lost A evs")]
|> standard;
-
--- a/src/HOL/Auth/Shared.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Sep 26 12:50:48 1996 +0200
@@ -12,22 +12,19 @@
consts
shrK :: agent => key (*symmetric keys*)
- leaked :: nat set (*Friendly agents whose keys have leaked to Enemy*)
-
-constdefs (*Enemy and compromised agents*)
- bad :: agent set "bad == insert Enemy (Friend``leaked)"
rules
isSym_shrK "isSymKey (shrK A)"
consts (*Initial states of agents -- parameter of the construction*)
- initState :: agent => msg set
+ initState :: [agent set, agent] => msg set
primrec initState agent
(*Server knows all keys; other agents know only their own*)
- initState_Server "initState Server = Key `` range shrK"
- initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
- initState_Enemy "initState Enemy = Key``shrK``bad"
+ initState_Server "initState lost Server = Key `` range shrK"
+ initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}"
+ initState_Spy "initState lost Spy = Key``shrK``lost"
+
datatype (*Messages, and components of agent stores*)
event = Says agent agent msg
@@ -38,16 +35,16 @@
primrec sees1 event
(*First agent recalls all that it says, but NOT everything
that is sent to it; it must note such things if/when received*)
- sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})"
+ sees1_Says "sees1 A (Says A' B X) = (if A:{A',Spy} then {X} else {})"
(*part of A's internal state*)
consts
- sees :: [agent, event list] => msg set
+ sees :: [agent set, agent, event list] => msg set
primrec sees list
(*Initial knowledge includes all public keys and own private key*)
- sees_Nil "sees A [] = initState A"
- sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
+ sees_Nil "sees lost A [] = initState lost A"
+ sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
(*Agents generate "random" nonces. Different traces always yield
@@ -57,13 +54,12 @@
newK :: "event list => key"
rules
- inj_shrK "inj shrK"
+ inj_shrK "inj shrK"
+
+ inj_newN "inj newN"
- inj_newN "inj newN"
- fresh_newN "Nonce (newN evs) ~: parts (initState B)"
-
- inj_newK "inj newK"
- fresh_newK "Key (newK evs) ~: parts (initState B)"
- isSym_newK "isSymKey (newK evs)"
+ inj_newK "inj newK"
+ newK_neq_shrK "newK evs ~= shrK A"
+ isSym_newK "isSymKey (newK evs)"
end
--- a/src/HOL/Auth/Yahalom.ML Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Yahalom.ML Thu Sep 26 12:50:48 1996 +0200
@@ -20,10 +20,10 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX X NB K. EX evs: yahalom. \
+\ ==> EX X NB K. EX evs: yahalom lost. \
\ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
+by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (ALLGOALS Fast_tac);
result();
@@ -31,19 +31,19 @@
(**** Inductive proofs about yahalom ****)
-(*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 : yahalom ==> \
-\ sees A evs <= initState A Un sees Enemy evs";
-be yahalom.induct 1;
+ "!!evs. evs : yahalom lost ==> \
+\ sees lost A evs <= initState lost A Un sees lost Spy evs";
+by (etac yahalom.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 : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
-be yahalom.induct 1;
+goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
+by (etac yahalom.induct 1);
by (Auto_tac());
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
@@ -54,58 +54,58 @@
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
-\ X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "YM4_analz_sees_Enemy";
+\ X : analz (sees lost Spy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
+qed "YM4_analz_sees_Spy";
goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
\ : set_of_list evs ==> \
-\ K : parts (sees Enemy evs)";
+\ K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-qed "YM4_parts_sees_Enemy";
+ addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
+qed "YM4_parts_sees_Spy";
-(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
+(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
goal thy
- "!!evs. [| evs : yahalom; A ~: bad |] \
-\ ==> Key (shrK A) ~: parts (sees Enemy evs)";
-be yahalom.induct 1;
-bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+ "!!evs. [| evs : yahalom lost; A ~: lost |] \
+\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+by (etac yahalom.induct 1);
+by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
by (ALLGOALS Asm_simp_tac);
by (stac insert_commute 3);
by (Auto_tac());
(*Fake and YM4 are similar*)
by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert])));
-qed "Enemy_not_see_shrK";
+ impOfSubs Fake_parts_insert])));
+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, Enemy_not_analz_shrK];
+Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
(*We go to some trouble to preserve R in the 3rd and 4th subgoals
As usual fast_tac cannot be used because it uses the equalities too soon*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
-\ evs : yahalom; \
-\ A:bad ==> R \
+goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : yahalom lost; \
+\ A:lost ==> 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);
-AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
+AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
(*** Future keys can't be seen or used! ***)
@@ -116,21 +116,21 @@
standard Fake rule.
The length comparison, and Union over C, are essential for the
induction! *)
-goal thy "!!evs. evs : yahalom ==> \
+goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evs' --> \
-\ Key (newK evs') ~: (UN C. parts (sees C evs))";
-be yahalom.induct 1;
-bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+by (etac yahalom.induct 1);
+by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
by (REPEAT_FIRST (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*)
goal thy
- "!!evs. [| evs : yahalom; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees C evs)";
+ "!!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";
Addsimps [new_keys_not_seen];
@@ -139,23 +139,23 @@
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
-\ evs : yahalom \
+\ evs : yahalom lost \
\ |] ==> length evt < length evs";
-br ccontr 1;
-bd leI 1;
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
+by (rtac ccontr 1);
+by (dtac leI 1);
+by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
addIs [impOfSubs parts_mono]) 1);
qed "Says_imp_old_keys";
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : yahalom ==> \
+goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
-be yahalom.induct 1;
-by (forward_tac [YM4_parts_sees_Enemy] 6);
-bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+by (etac yahalom.induct 1);
+by (forward_tac [YM4_parts_sees_Spy] 6);
+by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
by (ALLGOALS Asm_full_simp_tac);
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
@@ -167,22 +167,22 @@
by (ALLGOALS
(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]
- addEs [new_keys_not_seen RSN(2,rev_notE)]
- addss (!simpset))));
+ impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
+ addEs [new_keys_not_seen RSN(2,rev_notE)]
+ addss (!simpset))));
val lemma = result();
goal thy
- "!!evs. [| evs : yahalom; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees C evs))";
+ "!!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";
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];
@@ -193,8 +193,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
- Key K : analz (sees Enemy evs)
+ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -205,17 +205,17 @@
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
- "!!evs. evs : yahalom ==> \
-\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees Enemy evs)";
-be yahalom.induct 1;
-bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+ "!!evs. evs : yahalom lost ==> \
+\ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
+by (etac yahalom.induct 1);
+by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
(*Deals with Faked messages*)
by (EVERY
(map (best_tac (!claset addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]
- addss (!simpset)))
+ addDs [impOfSubs parts_insert_subset_Un]
+ addss (!simpset)))
[3,2]));
(*Base case*)
by (Auto_tac());
@@ -230,8 +230,8 @@
Delsimps [image_Un];
Addsimps [image_Un RS sym];
-goal thy "insert (Key (newK x)) (sees A evs) = \
-\ Key `` (newK``{x}) Un (sees A evs)";
+goal thy "insert (Key (newK x)) (sees lost A evs) = \
+\ Key `` (newK``{x}) Un (sees lost A evs)";
by (Fast_tac 1);
val insert_Key_singleton = result();
@@ -243,10 +243,10 @@
(*This lets us avoid analyzing the new message -- unless we have to!*)
(*NEEDED??*)
-goal thy "synth (analz (sees Enemy evs)) <= \
-\ synth (analz (sees Enemy (Says A B X # evs)))";
+goal thy "synth (analz (sees lost Spy evs)) <= \
+\ synth (analz (sees lost Spy (Says A B X # evs)))";
by (Simp_tac 1);
-br (subset_insertI RS analz_mono RS synth_mono) 1;
+by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
qed "synth_analz_thin";
AddIs [impOfSubs synth_analz_thin];
@@ -265,33 +265,33 @@
goal thy
- "!!evs. evs : yahalom ==> \
-\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
-\ (K : newK``E | Key K : analz (sees Enemy evs))";
-be yahalom.induct 1;
-bd YM4_analz_sees_Enemy 6;
+ "!!evs. evs : yahalom lost ==> \
+\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
+\ (K : newK``E | Key K : analz (sees lost Spy evs))";
+by (etac yahalom.induct 1);
+by (dtac YM4_analz_sees_Spy 6);
by (REPEAT_FIRST (resolve_tac [allI, lemma]));
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ @ pushes)
setloop split_tac [expand_if])));
(*YM4*)
-by (enemy_analz_tac 4);
+by (spy_analz_tac 4);
(*YM3*)
by (Fast_tac 3);
(*Fake case*)
-by (enemy_analz_tac 2);
+by (spy_analz_tac 2);
(*Base case*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
qed_spec_mp "analz_image_newK";
goal thy
- "!!evs. evs : yahalom ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
-\ (K = newK evt | Key K : analz (sees Enemy evs))";
+ "!!evs. evs : yahalom lost ==> \
+\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
+\ (K = newK evt | Key K : analz (sees lost 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";
@@ -301,39 +301,39 @@
"!!evs. [| Says Server A \
\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
-\ evs : yahalom |] \
-\ ==> (EX evt:yahalom. K = Key(newK evt))";
-be rev_mp 1;
-be yahalom.induct 1;
+\ evs : yahalom lost |] \
+\ ==> (EX evt: yahalom lost. K = Key(newK evt))";
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "Says_Server_message_form";
-(** Crucial secrecy property: Enemy does not see the keys sent in msg YM3
+(** Crucial secrecy property: Spy does not see the keys sent in msg YM3
As with Otway-Rees, proof does not need uniqueness of session keys. **)
goal thy
- "!!evs. [| A ~: bad; B ~: bad; evs : yahalom; evt : yahalom |] \
+ "!!evs. [| A ~: lost; B ~: lost; evs : yahalom lost; evt : yahalom lost |] \
\ ==> Says Server A \
\ {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A), \
\ Crypt {|Agent A, Key(newK evt)|} (shrK B)|} \
\ : set_of_list evs --> \
-\ Key(newK evt) ~: analz (sees Enemy evs)";
-be yahalom.induct 1;
-bd YM4_analz_sees_Enemy 6;
+\ Key(newK evt) ~: analz (sees lost Spy evs)";
+by (etac yahalom.induct 1);
+by (dtac YM4_analz_sees_Spy 6);
by (ALLGOALS
(asm_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])));
(*YM4*)
-by (enemy_analz_tac 3);
+by (spy_analz_tac 3);
(*YM3*)
by (fast_tac (!claset addIs [parts_insertI]
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 2);
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset)) 2);
(*Fake*) (** LEVEL 10 **)
-by (enemy_analz_tac 1);
+by (spy_analz_tac 1);
val lemma = result() RS mp RSN(2,rev_notE);
@@ -342,26 +342,26 @@
"!!evs. [| Says Server A \
\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
-\ A ~: bad; B ~: bad; evs : yahalom |] ==> \
-\ K ~: analz (sees Enemy evs)";
+\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
+\ K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (fast_tac (!claset addSEs [lemma]) 1);
-qed "Enemy_not_see_encrypted_key";
+qed "Spy_not_see_encrypted_key";
(** Towards proofs of stronger authenticity properties **)
goal thy
- "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees Enemy evs); \
-\ B ~: bad; evs : yahalom |] \
+ "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
+\ B ~: lost; evs : yahalom lost |] \
\ ==> EX NA NB. Says Server A \
\ {|Crypt {|Agent B, Key K, \
\ Nonce NA, Nonce NB|} (shrK A), \
\ Crypt {|Agent A, Key K|} (shrK B)|} \
\ : set_of_list evs";
-be rev_mp 1;
-be yahalom.induct 1;
-bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
by (ALLGOALS Asm_simp_tac);
(*YM3*)
by (Fast_tac 3);
@@ -371,28 +371,28 @@
by (stac insert_commute 2 THEN Simp_tac 2);
(*Fake and YM4 are similar*)
by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert])));
+ impOfSubs Fake_parts_insert])));
qed "Crypt_imp_Server_msg";
(*What can B deduce from receipt of YM4?
NOT THAT THE NONCES AGREE (in this version). But what does the Nonce
- give us??*)
+ give us??*)
goal thy
"!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \
\ Crypt (Nonce NB) K|} : set_of_list evs; \
-\ B ~: bad; evs : yahalom |] \
+\ B ~: lost; evs : yahalom lost |] \
\ ==> EX NA NB. Says Server A \
\ {|Crypt {|Agent B, Key K, \
\ Nonce NA, Nonce NB|} (shrK A), \
\ Crypt {|Agent A, Key K|} (shrK B)|} \
\ : set_of_list evs";
-be rev_mp 1;
-be yahalom.induct 1;
-by (dresolve_tac [YM4_analz_sees_Enemy] 6);
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (dtac YM4_analz_sees_Spy 6);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS
- Crypt_imp_Server_msg])));
+ Crypt_imp_Server_msg])));
qed "YM4_imp_Says_Server_A";
@@ -400,8 +400,8 @@
goal thy
"!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \
\ Crypt (Nonce NB) K|} : set_of_list evs; \
-\ A ~: bad; B ~: bad; evs : yahalom |] \
-\ ==> Key K ~: analz (sees Enemy evs)";
+\ A ~: lost; B ~: lost; evs : yahalom lost |] \
+\ ==> Key K ~: analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A,
- Enemy_not_see_encrypted_key]) 1);
+ Spy_not_see_encrypted_key]) 1);
qed "B_gets_secure_key";
--- a/src/HOL/Auth/Yahalom.thy Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Yahalom.thy Thu Sep 26 12:50:48 1996 +0200
@@ -12,34 +12,35 @@
Yahalom = Shared +
-consts yahalom :: "event list set"
-inductive yahalom
+consts yahalom :: "agent set => event list set"
+inductive "yahalom lost"
intrs
(*Initial trace is empty*)
- Nil "[]: yahalom"
+ Nil "[]: yahalom lost"
- (*The enemy MAY say anything he CAN say. We do not expect him to
+ (*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: yahalom; B ~= Enemy; X: synth (analz (sees Enemy evs)) |]
- ==> Says Enemy B X # evs : yahalom"
+ Fake "[| evs: yahalom lost; B ~= Spy;
+ X: synth (analz (sees lost Spy evs)) |]
+ ==> Says Spy B X # evs : yahalom lost"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom; A ~= B |]
- ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
+ YM1 "[| evs: yahalom lost; A ~= B |]
+ ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs: yahalom; B ~= Server;
+ YM2 "[| evs: yahalom lost; B ~= Server;
Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
==> Says B Server
{|Agent B,
Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
- # evs : yahalom"
+ # evs : yahalom lost"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs: yahalom; A ~= Server;
+ YM3 "[| evs: yahalom lost; A ~= Server;
Says B' Server
{|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
: set_of_list evs |]
@@ -47,15 +48,15 @@
{|Crypt {|Agent B, Key (newK evs),
Nonce NA, Nonce NB|} (shrK A),
Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
- # evs : yahalom"
+ # evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom; A ~= B;
+ YM4 "[| evs: yahalom lost; A ~= B;
Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
X|}
: set_of_list evs;
Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
- ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
+ ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
end