# HG changeset patch # User paulson # Date 841767882 -7200 # Node ID 20574dca5a3eb3c0b7191c0235403e35cb1ad40d # Parent 6c9c1a42a869db2e648708e0df7a98bf0607540a Renaming and simplification diff -r 6c9c1a42a869 -r 20574dca5a3e src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Tue Sep 03 17:54:39 1996 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Tue Sep 03 18:24:42 1996 +0200 @@ -12,6 +12,8 @@ open NS_Shared; +proof_timing:=true; + (**** Inductive proofs about ns_shared ****) (*The Enemy can see more than anybody else, except for their initial state*) @@ -40,7 +42,7 @@ AddSEs [not_Notes RSN (2, rev_notE)]; -(*For reasoning about message NS3*) +(*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)"; by (fast_tac (!claset addSEs partsEs @@ -48,68 +50,68 @@ qed "NS3_msg_in_parts_sees_Enemy"; -(*** Server keys are not betrayed ***) +(*** Shared keys are not betrayed ***) -(*Enemy never sees another agent's server key!*) +(*Enemy never sees another agent's shared key!*) goal thy "!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \ -\ Key (serverKey A) ~: parts (sees Enemy evs)"; +\ Key (shrK A) ~: parts (sees Enemy evs)"; be ns_shared.induct 1; bd NS3_msg_in_parts_sees_Enemy 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_serverKey"; + impOfSubs Fake_parts_insert]) 1); +qed "Enemy_not_see_shrK"; -bind_thm ("Enemy_not_analz_serverKey", - [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); +bind_thm ("Enemy_not_analz_shrK", + [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD); -Addsimps [Enemy_not_see_serverKey, - not_sym RSN (2, Enemy_not_see_serverKey), - Enemy_not_analz_serverKey, - not_sym RSN (2, Enemy_not_analz_serverKey)]; +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)]; (*We go to some trouble to preserve R in the 3rd subgoal*) val major::prems = -goal thy "[| Key (serverKey A) : parts (sees Enemy evs); \ +goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ \ evs : ns_shared; \ \ A=Enemy ==> R \ \ |] ==> R"; br ccontr 1; -br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1; +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; by (swap_res_tac prems 2); by (ALLGOALS (fast_tac (!claset addIs prems))); -qed "Enemy_see_serverKey_E"; +qed "Enemy_see_shrK_E"; -bind_thm ("Enemy_analz_serverKey_E", - analz_subset_parts RS subsetD RS Enemy_see_serverKey_E); +bind_thm ("Enemy_analz_shrK_E", + analz_subset_parts RS subsetD RS Enemy_see_shrK_E); (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) -AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E]; +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; -(*No Friend will ever see another agent's server key +(*No Friend will ever see another agent's shared key (excluding the Enemy, who might transmit his). - The Server, of course, knows all server keys.*) + The Server, of course, knows all shared keys.*) goal thy "!!evs. [| evs : ns_shared; A ~= Enemy; A ~= Friend j |] ==> \ -\ Key (serverKey A) ~: parts (sees (Friend j) evs)"; +\ Key (shrK A) ~: parts (sees (Friend j) evs)"; br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; by (ALLGOALS Asm_simp_tac); -qed "Friend_not_see_serverKey"; +qed "Friend_not_see_shrK"; (*Not for Addsimps -- it can cause goals to blow up!*) goal thy "!!evs. evs : ns_shared ==> \ -\ (Key (serverKey A) \ -\ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \ +\ (Key (shrK A) \ +\ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ \ (A=B | A=Enemy)"; by (best_tac (!claset addDs [impOfSubs analz_subset_parts] addIs [impOfSubs (subset_insertI RS analz_mono)] addss (!simpset)) 1); -qed "serverKey_mem_analz"; +qed "shrK_mem_analz"; (*** Future keys can't be seen or used! ***) @@ -200,8 +202,8 @@ \ evs : ns_shared \ \ |] ==> (EX evt:ns_shared. \ \ K = Key(newK evt) & \ -\ X = (Crypt {|K, Agent A|} (serverKey B)) & \ -\ K' = serverKey A & \ +\ X = (Crypt {|K, Agent A|} (shrK B)) & \ +\ K' = shrK A & \ \ length evt < length evs)"; be rev_mp 1; be ns_shared.induct 1; @@ -209,14 +211,15 @@ qed "Says_Server_message_form"; -(*Describes the form of X when the following message is sent*) +(*Describes the form of X when the following message is sent. The use of + "parts" strengthens the induction hyp for proving the Fake case*) goal thy "!!evs. evs : ns_shared ==> \ \ ALL A NA B K X. \ -\ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ +\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ \ : parts (sees Enemy evs) & A ~= Enemy --> \ \ (EX evt:ns_shared. K = newK evt & \ -\ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; +\ X = (Crypt {|Key K, Agent A|} (shrK B)))"; be ns_shared.induct 1; bd NS3_msg_in_parts_sees_Enemy 5; by (Step_tac 1); @@ -225,7 +228,7 @@ 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] + impOfSubs Fake_parts_insert] addss (!simpset)) 1); qed_spec_mp "encrypted_form"; @@ -234,7 +237,7 @@ goal thy "!!evs. evs : ns_shared ==> \ \ ALL S A NA B K X. \ -\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ +\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ \ : set_of_list evs --> \ \ S = Server | S = Enemy"; be ns_shared.induct 1; @@ -247,7 +250,7 @@ bd 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); +by (thin_tac "ALL x. ?P(x)" 1); bd encrypted_form 1; br (parts.Inj RS conjI) 1; auto(); @@ -257,11 +260,11 @@ (*Describes the form of X when the following message is sent; use Says_Server_message_form if applicable*) goal thy - "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ -\ : set_of_list evs; \ -\ evs : ns_shared \ -\ |] ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \ -\ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; + "!!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 & \ +\ X = (Crypt {|Key K, Agent A|} (shrK B)))"; by (forward_tac [Server_or_Enemy] 1); ba 1; by (Step_tac 1); @@ -277,8 +280,8 @@ The following is to prove theorems of the form Key K : analz (insert (Key (newK evt)) - (insert (Key (serverKey C)) (sees Enemy evs))) ==> - Key K : analz (insert (Key (serverKey C)) (sees Enemy evs)) + (insert (Key (shrK C)) (sees Enemy evs))) ==> + Key K : analz (insert (Key (shrK C)) (sees Enemy evs)) A more general formula must be proved inductively. @@ -323,52 +326,56 @@ (** Session keys are not used to encrypt other session keys **) +(*Lemma for the trivial direction of the if-and-only-if*) +goal thy + "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \ +\ (K : nE | Key K : analz (insert KsC sEe)) ==> \ +\ (Key K : analz (insert KsC (Key``nE Un sEe))) = \ +\ (K : nE | Key K : analz (insert KsC sEe))"; +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); +val lemma = result(); + goal thy "!!evs. evs : ns_shared ==> \ -\ ALL K E. (Key K : analz (insert (Key (serverKey C)) \ +\ ALL K E. (Key K : analz (insert (Key (shrK C)) \ \ (Key``(newK``E) Un (sees Enemy evs)))) = \ \ (K : newK``E | \ -\ Key K : analz (insert (Key (serverKey C)) \ +\ Key K : analz (insert (Key (shrK C)) \ \ (sees Enemy evs)))"; be ns_shared.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 (REPEAT_FIRST (resolve_tac [allI, lemma])); by (ALLGOALS (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); +(** LEVEL 5 **) (*Cases NS2 and NS3!! Simple, thanks to auto case splits*) by (REPEAT (Fast_tac 3)); +(*Fake case*) (** LEVEL 6 **) +by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] + (insert_commute RS ssubst) 2); +(*This is enemy_analz_tac from OtwayRees.ML*) +by (EVERY [rtac impI 2, + dtac (impOfSubs Fake_analz_insert) 2, + eresolve_tac [asm_rl, synth.Inj] 2, + Fast_tac 2, + Asm_full_simp_tac 2, + deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 2]); (*Base case*) by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); -(** LEVEL 7 **) -(*Fake case*) -by (REPEAT (Safe_step_tac 1)); -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2); -by (subgoal_tac - "Key K : analz \ -\ (synth \ -\ (analz (insert (Key (serverKey C)) \ -\ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); -(*First, justify this subgoal*) -(*Discard formulae for better speed*) -by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); -by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); -by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] - addSEs [impOfSubs analz_mono]) 2); -by (Asm_full_simp_tac 1); -by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1); qed_spec_mp "analz_image_newK"; goal thy "!!evs. evs : ns_shared ==> \ \ Key K : analz (insert (Key (newK evt)) \ -\ (insert (Key (serverKey C)) \ +\ (insert (Key (shrK C)) \ \ (sees Enemy evs))) = \ \ (K = newK evt | \ -\ Key K : analz (insert (Key (serverKey C)) \ +\ Key K : analz (insert (Key (shrK C)) \ \ (sees Enemy evs)))"; by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, insert_Key_singleton]) 1); @@ -384,8 +391,7 @@ \ EX X'. ALL C S A Y N B X. \ \ C ~= Enemy --> \ \ Says S A Y : set_of_list evs --> \ -\ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \ -\ (X = X'))"; +\ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> X=X')"; be ns_shared.induct 1; by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); by (ALLGOALS @@ -407,13 +413,13 @@ ba 2; by (Step_tac 1); (** LEVEL 12 **) -by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \ +by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \ \ : parts (sees Enemy evsa)" 1); -by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); +by (thin_tac "ALL S.?P(S)" 2); by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] addDs [impOfSubs parts_insert_subset_Un] addss (!simpset)) 2); -by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1); +by (thin_tac "?aa : parts {X}" 1); bd parts_singleton 1; by (Step_tac 1); bd seesD 1; @@ -426,10 +432,10 @@ (*In messages of this form, the session key uniquely identifies the rest*) goal thy "!!evs. [| Says S A \ -\ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) \ +\ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \ \ : set_of_list evs; \ \ Says S' A' \ -\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \ +\ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ \ : set_of_list evs; \ \ evs : ns_shared; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; bd lemma 1; @@ -447,9 +453,10 @@ \ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ \ evs : ns_shared; Friend i ~= C; Friend j ~= C \ \ |] ==> \ -\ K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))"; +\ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))"; be rev_mp 1; be ns_shared.induct 1; +(*TRY CHANGING NEXT CMD TO by (ALLGOALS Asm_simp_tac);*) 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])); @@ -467,7 +474,7 @@ br notI 1; by (subgoal_tac "Key (newK evt) : \ -\ analz (synth (analz (insert (Key (serverKey C)) \ +\ analz (synth (analz (insert (Key (shrK C)) \ \ (sees Enemy evsa))))" 1); be (impOfSubs analz_mono) 2; by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), @@ -489,7 +496,7 @@ by (REPEAT_FIRST assume_tac); by (ALLGOALS Full_simp_tac); by (Step_tac 1); -by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1); +by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1); qed "Enemy_not_see_encrypted_key"; diff -r 6c9c1a42a869 -r 20574dca5a3e src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Tue Sep 03 17:54:39 1996 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Tue Sep 03 18:24:42 1996 +0200 @@ -22,46 +22,49 @@ 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" + |] ==> Says Enemy B X # evs : ns_shared" (*Alice initiates a protocol run*) NS1 "[| evs: ns_shared; A ~= Server - |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) - # evs : ns_shared" + |] ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs + : ns_shared" (*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; - (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs - |] ==> (Says Server A + 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|} (serverKey B))|} - (serverKey A))) # evs : ns_shared" + (Crypt {|Key (newK evs), Agent A|} (shrK B))|} + (shrK A)) # evs : ns_shared" (*We can't assume S=Server. Agent A "remembers" her nonce. May assume WLOG that she is NOT the Enemy: the Fake rule covers this case. Can inductively show A ~= Server*) NS3 "[| evs: ns_shared; A ~= B; - (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) + Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) : set_of_list evs; A = Friend i; - (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs - |] ==> (Says A B X) # evs : ns_shared" + Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs + |] ==> Says A B X # evs : ns_shared" (*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; - (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) - : set_of_list evs - |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : ns_shared" + 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" - (*Alice responds with (Suc N), if she has seen the key before.*) + (*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 + nonces. Instead we distinguish the messages by sending the + nonce twice.*) NS5 "[| evs: ns_shared; A ~= B; - (Says B' A (Crypt (Nonce N) K)) : set_of_list evs; - (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) + 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 (Suc N)) K)) # evs : ns_shared" + |] ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared" end diff -r 6c9c1a42a869 -r 20574dca5a3e src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Tue Sep 03 17:54:39 1996 +0200 +++ b/src/HOL/Auth/Shared.ML Tue Sep 03 18:24:42 1996 +0200 @@ -12,13 +12,6 @@ Addsimps [parts_cut_eq]; -proof_timing:=true; - -(*IN SET.ML*) -goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; -by (simp_tac (!simpset setloop split_tac [expand_if]) 1); -qed "mem_if"; - (*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; by (fast_tac (!claset addEs [equalityE]) 1); @@ -34,37 +27,37 @@ will not!*) Addsimps [o_def]; -(*** Basic properties of serverKey and newK ***) +(*** Basic properties of shrK and newK ***) -(* invKey (serverKey A) = serverKey A *) -bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey); +(* invKey (shrK A) = shrK A *) +bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK); (* invKey (newK evs) = newK evs *) bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); -Addsimps [invKey_serverKey, invKey_newK]; +Addsimps [invKey_shrK, invKey_newK]; (*New keys and nonces are fresh*) -val serverKey_inject = inj_serverKey RS injD; +val shrK_inject = inj_shrK RS injD; val newN_inject = inj_newN RS injD and newK_inject = inj_newK RS injD; -AddSEs [serverKey_inject, newN_inject, newK_inject, +AddSEs [shrK_inject, newN_inject, newK_inject, fresh_newK RS notE, fresh_newN RS notE]; -Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; +Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; Addsimps [fresh_newN, fresh_newK]; (** Rewrites should not refer to initState(Friend i) -- not in normal form! **) -goal thy "newK evs ~= serverKey B"; -by (subgoal_tac "newK evs = serverKey B --> \ +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)); -qed "newK_neq_serverKey"; +qed "newK_neq_shrK"; -Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym]; +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"; @@ -96,25 +89,25 @@ qed "keysFor_image_Key"; Addsimps [keysFor_image_Key]; -goal thy "serverKey A ~: newK``E"; +goal thy "shrK A ~: newK``E"; by (agent.induct_tac "A" 1); by (Auto_tac ()); -qed "serverKey_notin_image_newK"; -Addsimps [serverKey_notin_image_newK]; +qed "shrK_notin_image_newK"; +Addsimps [shrK_notin_image_newK]; -(*Agents see their own serverKeys!*) -goal thy "Key (serverKey A) : analz (sees A evs)"; +(*Agents see their own shrKs!*) +goal thy "Key (shrK A) : analz (sees A evs)"; by (list.induct_tac "evs" 1); by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2); by (agent.induct_tac "A" 1); by (auto_tac (!claset addIs [range_eqI], !simpset)); -qed "analz_own_serverKey"; +qed "analz_own_shrK"; -bind_thm ("parts_own_serverKey", - [analz_subset_parts, analz_own_serverKey] MRS subsetD); +bind_thm ("parts_own_shrK", + [analz_subset_parts, analz_own_shrK] MRS subsetD); -Addsimps [analz_own_serverKey, parts_own_serverKey]; +Addsimps [analz_own_shrK, parts_own_shrK]; @@ -143,6 +136,11 @@ by (Fast_tac 1); qed "sees_Says_subset_insert"; +goal thy "sees A (Notes A' X # evs) <= insert X (sees A evs)"; +by (simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (Fast_tac 1); +qed "sees_Notes_subset_insert"; + goal thy "sees A evs <= sees A (Says A' B X # evs)"; by (simp_tac (!simpset setloop split_tac [expand_if]) 1); by (Fast_tac 1); @@ -166,7 +164,7 @@ Addsimps [Says_imp_sees_Enemy]; AddIs [Says_imp_sees_Enemy]; -goal thy "initState C <= Key `` range serverKey"; +goal thy "initState C <= Key `` range shrK"; by (agent.induct_tac "C" 1); by (Auto_tac ()); qed "initState_subset"; @@ -174,7 +172,7 @@ goal thy "X : sees C evs --> \ \ (EX A B. Says A B X : set_of_list evs) | \ \ (EX A. Notes A X : set_of_list evs) | \ -\ (EX A. X = Key (serverKey A))"; +\ (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); @@ -211,6 +209,6 @@ (*Cannot be added with Addsimps -- we don't always want to re-order messages*) val pushes = pushKeys@pushCrypts; -val pushKey_newK = insComm "Key (newK ?evs)" "Key (serverKey ?C)"; +val pushKey_newK = insComm "Key (newK ?evs)" "Key (shrK ?C)"; diff -r 6c9c1a42a869 -r 20574dca5a3e src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Tue Sep 03 17:54:39 1996 +0200 +++ b/src/HOL/Auth/Shared.thy Tue Sep 03 18:24:42 1996 +0200 @@ -6,24 +6,26 @@ Theory of Shared Keys (common to all symmetric-key protocols) Server keys; initial states of agents; new nonces and keys; function "sees" + +IS THE Notes constructor needed?? *) Shared = Message + List + consts - serverKey :: agent => key (*symmetric keys*) + shrK :: agent => key (*symmetric keys*) rules - isSym_serverKey "isSymKey (serverKey A)" + isSym_shrK "isSymKey (shrK A)" consts (*Initial states of agents -- parameter of the construction*) initState :: agent => msg set primrec initState agent (*Server knows all keys; other agents know only their own*) - initState_Server "initState Server = Key `` range serverKey" - initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}" - initState_Enemy "initState Enemy = {Key (serverKey Enemy)}" + initState_Server "initState Server = Key `` range shrK" + initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" + initState_Enemy "initState Enemy = {Key (shrK Enemy)}" datatype (*Messages, and components of agent stores*) event = Says agent agent msg @@ -55,7 +57,7 @@ newK :: "event list => key" rules - inj_serverKey "inj serverKey" + inj_shrK "inj shrK" inj_newN "inj newN" fresh_newN "Nonce (newN evs) ~: parts (initState B)"