# HG changeset patch # User paulson # Date 843735048 -7200 # Node ID 1bbf1bdcaf56d0d75bfd1d7fc4b79a42f1cefcdd # Parent 03a843f0f4472cbf50faf608bf698c972a2e2c92 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Event.ML --- 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); diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Event.thy --- 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))) diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Message.ML --- 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); diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Message.thy --- 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 diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/NS_Shared.ML --- 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"; diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/NS_Shared.thy --- 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 diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/OtwayRees.ML --- 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"; + + diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/OtwayRees.thy --- 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 diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/OtwayRees_Bad.ML --- 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); diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/OtwayRees_Bad.thy --- 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 diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Shared.ML --- 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; - diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Shared.thy --- 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 diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Yahalom.ML --- 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"; diff -r 03a843f0f447 -r 1bbf1bdcaf56 src/HOL/Auth/Yahalom.thy --- 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