# HG changeset patch # User paulson # Date 840446395 -7200 # Node ID 2809adb15eb0aefe0a2eaf39084a3b14cb26a950 # Parent 947a34e00d1ea21367abc9d144e759ec51018a26 Renaming of functions, and tidying diff -r 947a34e00d1e -r 2809adb15eb0 src/HOL/Auth/Event.ML --- a/src/HOL/Auth/Event.ML Mon Aug 19 11:19:16 1996 +0200 +++ b/src/HOL/Auth/Event.ML Mon Aug 19 11:19:55 1996 +0200 @@ -15,29 +15,25 @@ Delrules [less_SucE]; (*Perhaps avoid inserting this in Arith.ML????*) (*FOR LIST.ML??*) -goal List.thy "x : setOfList (x#xs)"; +goal List.thy "x : set_of_list (x#xs)"; by (Simp_tac 1); -qed "setOfList_I1"; +qed "set_of_list_I1"; -goal List.thy "!!x. xs = x#xs' ==> x : setOfList xs"; +goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs"; by (Asm_simp_tac 1); -qed "setOfList_eqI1"; +qed "set_of_list_eqI1"; -goal List.thy "setOfList l <= setOfList (x#l)"; +goal List.thy "set_of_list l <= set_of_list (x#l)"; by (Simp_tac 1); by (Fast_tac 1); -qed "setOfList_subset_Cons"; +qed "set_of_list_subset_Cons"; (*Not for Addsimps -- it can cause goals to blow up!*) 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"; -(*DELETE, AS ALREADY IN SET.ML*) -prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; - - -(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE!!*) +(*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); val subset_range_iff = result(); @@ -45,10 +41,6 @@ open Event; -goal Set.thy "A Un (insert a B) = insert a (A Un B)"; -by (Fast_tac 1); -qed "Un_insert_right"; - Addsimps [Un_insert_left, Un_insert_right]; (*By default only o_apply is built-in. But in the presence of eta-expansion @@ -94,15 +86,15 @@ bind_thm ("parts_image_Key", subset_refl RS parts_image_subset); -goal thy "!!H. H <= Key``E ==> analyze H = H"; +goal thy "!!H. H <= Key``E ==> analz H = H"; by (Auto_tac ()); -be analyze.induct 1; +be analz.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_image_subset"; +qed "analz_image_subset"; -bind_thm ("analyze_image_Key", subset_refl RS analyze_image_subset); +bind_thm ("analz_image_Key", subset_refl RS analz_image_subset); -Addsimps [parts_image_Key, analyze_image_Key]; +Addsimps [parts_image_Key, analz_image_Key]; goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; by (agent.induct_tac "C" 1); @@ -123,17 +115,17 @@ (*Agents see their own serverKeys!*) -goal thy "Key (serverKey A) : analyze (sees A evs)"; +goal thy "Key (serverKey A) : analz (sees A evs)"; by (list.induct_tac "evs" 1); -by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analyze_mono)]) 2); +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 "analyze_own_serverKey"; +qed "analz_own_serverKey"; bind_thm ("parts_own_serverKey", - [analyze_subset_parts, analyze_own_serverKey] MRS subsetD); + [analz_subset_parts, analz_own_serverKey] MRS subsetD); -Addsimps [analyze_own_serverKey, parts_own_serverKey]; +Addsimps [analz_own_serverKey, parts_own_serverKey]; @@ -197,7 +189,7 @@ by (ALLGOALS (fast_tac (!claset addss ss))); qed "UN_parts_sees_Says"; -goal thy "Says A B X : setOfList evs --> X : sees Enemy evs"; +goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs"; by (list.induct_tac "evs" 1); by (Auto_tac ()); qed_spec_mp "Says_imp_sees_Enemy"; @@ -211,8 +203,8 @@ qed "initState_subset"; goal thy "X : sees C evs --> \ -\ (EX A B. Says A B X : setOfList evs) | \ -\ (EX A. Notes A X : setOfList 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))"; by (list.induct_tac "evs" 1); by (ALLGOALS Asm_simp_tac); @@ -244,14 +236,14 @@ (*Nobody sends themselves messages*) -goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs"; +goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs"; be 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 ~: setOfList evs"; +goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs"; be traces.induct 1; by (Auto_tac()); qed "not_Notes"; @@ -269,18 +261,18 @@ be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) by (auto_tac(!claset, !simpset addsimps [parts_insert2])); (*Deals with Faked messages*) -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts, +by (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un] addss (!simpset)) 1); qed "Enemy_not_see_serverKey"; -bind_thm ("Enemy_not_analyze_serverKey", - [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); +bind_thm ("Enemy_not_analz_serverKey", + [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); Addsimps [Enemy_not_see_serverKey, not_sym RSN (2, Enemy_not_see_serverKey), - Enemy_not_analyze_serverKey, - not_sym RSN (2, Enemy_not_analyze_serverKey)]; + Enemy_not_analz_serverKey, + not_sym RSN (2, Enemy_not_analz_serverKey)]; (*We go to some trouble to preserve R in the 3rd subgoal*) val major::prems = @@ -294,11 +286,11 @@ by (ALLGOALS (fast_tac (!claset addIs prems))); qed "Enemy_see_serverKey_E"; -bind_thm ("Enemy_analyze_serverKey_E", - analyze_subset_parts RS subsetD RS Enemy_see_serverKey_E); +bind_thm ("Enemy_analz_serverKey_E", + analz_subset_parts RS subsetD RS Enemy_see_serverKey_E); (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) -AddSEs [Enemy_see_serverKey_E, Enemy_analyze_serverKey_E]; +AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E]; (*No Friend will ever see another agent's server key @@ -316,12 +308,12 @@ goal thy "!!evs. evs : traces ==> \ \ (Key (serverKey A) \ -\ : analyze (insert (Key (serverKey B)) (sees Enemy evs))) = \ +\ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \ \ (A=B | A=Enemy)"; -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts] - addIs [impOfSubs (subset_insertI RS analyze_mono)] +by (best_tac (!claset addDs [impOfSubs analz_subset_parts] + addIs [impOfSubs (subset_insertI RS analz_mono)] addss (!simpset)) 1); -qed "serverKey_mem_analyze"; +qed "serverKey_mem_analz"; @@ -349,7 +341,7 @@ (*Rule NS3 in protocol*) by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2); (*Rule Fake: where an Enemy agent can say practically anything*) -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts, +by (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, less_imp_le] addss (!simpset)) 1); @@ -365,7 +357,7 @@ (*Another variant: old messages must contain old keys!*) goal thy - "!!evs. [| Says A B X : setOfList evs; \ + "!!evs. [| Says A B X : set_of_list evs; \ \ Key (newK evt) : parts {X}; \ \ evs : traces \ \ |] ==> length evt < length evs"; @@ -398,10 +390,10 @@ (*Rule Fake: where an Enemy agent can say practically anything*) by (best_tac (!claset addSDs [newK_invKey] - addDs [impOfSubs (analyze_subset_parts RS keysFor_mono), + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), impOfSubs (parts_insert_subset_Un RS keysFor_mono), less_imp_le] - addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)] + addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)] addss (!simpset)) 1); (*Rule NS3: quite messy...*) by (hyp_subst_tac 1); @@ -422,15 +414,15 @@ by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); qed "new_keys_not_used"; -bind_thm ("new_keys_not_analyzed", - [analyze_subset_parts RS keysFor_mono, +bind_thm ("new_keys_not_analzd", + [analz_subset_parts RS keysFor_mono, new_keys_not_used] MRS contra_subsetD); -Addsimps [new_keys_not_used, new_keys_not_analyzed]; +Addsimps [new_keys_not_used, new_keys_not_analzd]; (** Rewrites to push in Key and Crypt messages, so that other messages can - be pulled out using the analyze_insert rules **) + be pulled out using the analz_insert rules **) fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] insert_commute; @@ -452,7 +444,7 @@ (*Describes the form *and age* of K, and the form of X, when the following message is sent*) goal thy - "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \ + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ \ evs : traces \ \ |] ==> (EX evt:traces. \ \ K = Key(newK evt) & \ @@ -465,9 +457,9 @@ by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); qed "Says_Server_message_form"; -(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *) -bind_thm ("not_parts_not_keysFor_analyze", - analyze_subset_parts RS keysFor_mono RS contra_subsetD); +(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *) +bind_thm ("not_parts_not_keysFor_analz", + analz_subset_parts RS keysFor_mono RS contra_subsetD); @@ -477,13 +469,13 @@ \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ \ evs : traces; i~=k \ \ |] ==> \ -\ K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; +\ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; be rev_mp 1; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); by (Step_tac 1); -by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1); +by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); val Enemy_not_see_encrypted_key_lemma = result(); *) @@ -519,9 +511,9 @@ (*Now for the Fake case*) by (subgoal_tac "Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \ -\ parts (synthesize (analyze (sees Enemy evsa)) Un (sees Enemy evsa))" 1); +\ parts (synth (analz (sees Enemy evsa)) Un (sees Enemy evsa))" 1); by (fast_tac (!claset addSEs [impOfSubs parts_mono]) 2); -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts] +by (best_tac (!claset addDs [impOfSubs analz_subset_parts] addss (!simpset)) 1); val encrypted_form = result(); @@ -531,7 +523,7 @@ "!!evs. evs : traces ==> \ \ ALL S A NA B K X. \ \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ -\ : setOfList evs --> \ +\ : set_of_list evs --> \ \ S = Server | S = Enemy"; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) @@ -541,7 +533,7 @@ (*First justify this assumption!*) by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); by (Step_tac 1); -bd (setOfList_I1 RS Says_Server_message_form) 1; +bd (set_of_list_I1 RS 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); @@ -555,7 +547,7 @@ use Says_Server_message_form if applicable*) goal thy "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ -\ : setOfList evs; \ +\ : set_of_list evs; \ \ evs : traces \ \ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; @@ -576,7 +568,7 @@ \ K = newK evt & \ \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; by (forward_tac [traces_eq_ConsE] 1); -by (dtac (setOfList_eqI1 RS Says_S_message_form) 2); +by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2); by (Auto_tac()); qed "Says_S_message_form_eq"; @@ -586,9 +578,9 @@ (**** The following is to prove theorems of the form - Key K : analyze (insert (Key (newK evt)) + Key K : analz (insert (Key (newK evt)) (insert (Key (serverKey C)) (sees Enemy evs))) ==> - Key K : analyze (insert (Key (serverKey C)) (sees Enemy evs)) + Key K : analz (insert (Key (serverKey C)) (sees Enemy evs)) A more general formula must be proved inductively. @@ -610,7 +602,7 @@ by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2); by (Asm_full_simp_tac 2); (*Deals with Faked messages*) -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts, +by (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un] addss (!simpset)) 1); result(); @@ -636,10 +628,10 @@ goal thy "!!evs. evs : traces ==> \ -\ ALL K E. (Key K : analyze (insert (Key (serverKey C)) \ +\ ALL K E. (Key K : analz (insert (Key (serverKey C)) \ \ (Key``(newK``E) Un (sees Enemy evs)))) = \ \ (K : newK``E | \ -\ Key K : analyze (insert (Key (serverKey C)) \ +\ Key K : analz (insert (Key (serverKey C)) \ \ (sees Enemy evs)))"; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) @@ -657,35 +649,35 @@ (** LEVEL 7 **) (*Fake case*) by (REPEAT (Safe_step_tac 1)); -by (fast_tac (!claset addSEs [impOfSubs (analyze_mono)]) 2); +by (fast_tac (!claset addSEs [impOfSubs (analz_mono)]) 2); by (subgoal_tac - "Key K : analyze \ -\ (synthesize \ -\ (analyze (insert (Key (serverKey C)) \ + "Key K : analz \ +\ (synth \ +\ (analz (insert (Key (serverKey C)) \ \ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); (*First, justify this subgoal*) (*Discard the quantified formula 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 (analyze_mono RS synthesize_mono)] - addSEs [impOfSubs analyze_mono]) 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 analyze_mono]) 0 1); -qed_spec_mp "analyze_image_newK"; +by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1); +qed_spec_mp "analz_image_newK"; goal thy "!!evs. evs : traces ==> \ -\ Key K : analyze (insert (Key (newK evt)) \ +\ Key K : analz (insert (Key (newK evt)) \ \ (insert (Key (serverKey C)) \ \ (sees Enemy evs))) = \ \ (K = newK evt | \ -\ Key K : analyze (insert (Key (serverKey C)) \ +\ Key K : analz (insert (Key (serverKey C)) \ \ (sees Enemy evs)))"; -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analyze_image_newK, +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, insert_Key_singleton]) 1); by (Fast_tac 1); -qed "analyze_insert_Key_newK"; +qed "analz_insert_Key_newK"; @@ -694,7 +686,7 @@ "!!evs. evs : traces ==> \ \ EX X'. ALL C S A Y N B X. \ \ C ~= Enemy --> \ -\ Says S A Y : setOfList evs --> \ +\ Says S A Y : set_of_list evs --> \ \ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \ \ (X = X'))"; be traces.induct 1; @@ -721,7 +713,7 @@ by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \ \ : parts (sees Enemy evsa)" 1); by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); -by (best_tac (!claset addSEs [impOfSubs analyze_subset_parts] +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); @@ -737,9 +729,9 @@ (*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)) : setOfList evs; \ +\ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : set_of_list evs; \ \ Says S' A' \ -\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : setOfList evs; \ +\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : set_of_list evs; \ \ \ \ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; bd lemma 1; @@ -754,10 +746,10 @@ -- even if another key is compromised*) goal thy "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent(Friend j), K, X|} K') : setOfList evs; \ +\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ \ evs : traces; Friend i ~= C; Friend j ~= C \ \ |] ==> \ -\ K ~: analyze (insert (Key (serverKey C)) (sees Enemy evs))"; +\ K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))"; be rev_mp 1; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) @@ -768,8 +760,8 @@ by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); by (ALLGOALS (asm_full_simp_tac - (!simpset addsimps ([analyze_subset_parts RS contra_subsetD, - analyze_insert_Key_newK] @ pushes) + (!simpset addsimps ([analz_subset_parts RS contra_subsetD, + analz_insert_Key_newK] @ pushes) setloop split_tac [expand_if]))); (*NS2*) by (fast_tac (!claset addSEs [less_irrefl]) 2); @@ -778,13 +770,13 @@ br notI 1; by (subgoal_tac "Key (newK evt) : \ -\ analyze (synthesize (analyze (insert (Key (serverKey C)) \ +\ analz (synth (analz (insert (Key (serverKey C)) \ \ (sees Enemy evsa))))" 1); -be (impOfSubs analyze_mono) 2; -by (deepen_tac (!claset addIs [analyze_mono RS synthesize_mono RSN +be (impOfSubs analz_mono) 2; +by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), - impOfSubs synthesize_increasing, - impOfSubs analyze_increasing]) 0 2); + impOfSubs synth_increasing, + impOfSubs analz_increasing]) 0 2); (*Proves the Fake goal*) by (fast_tac (!claset addss (!simpset)) 1); @@ -792,14 +784,14 @@ (*Now for NS3*) (*NS3, case 1: that message from the Server was just sent*) by (ALLGOALS (forward_tac [traces_ConsE])); -by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1); +by (forward_tac [set_of_list_I1 RS Says_Server_message_form] 1); by (Full_simp_tac 1); by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); (*Can simplify the Crypt messages: their key is secure*) by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); by (asm_full_simp_tac - (!simpset addsimps (pushes @ [analyze_insert_Crypt, - analyze_subset_parts RS contra_subsetD])) 1); + (!simpset addsimps (pushes @ [analz_insert_Crypt, + analz_subset_parts RS contra_subsetD])) 1); (**LEVEL 20, one subgoal left! **) (*NS3, case 2: that message from the Server was sent earlier*) @@ -813,18 +805,18 @@ (**LEVEL 24 **) -by ((forward_tac [setOfList_I1 RS Says_S_message_form]) 1); +by ((forward_tac [set_of_list_I1 RS Says_S_message_form]) 1); by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); by (asm_full_simp_tac - (!simpset addsimps (mem_if::analyze_insert_Key_newK::pushes)) 1); + (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1); by (step_tac (!claset delrules [impCE]) 1); (**LEVEL 28 **) -bd ([impOfSubs setOfList_subset_Cons, setOfList_I1] MRS unique_session_keys) 1; +bd ([impOfSubs set_of_list_subset_Cons, set_of_list_I1] MRS unique_session_keys) 1; ba 1; by (ALLGOALS Full_simp_tac); by (REPEAT_FIRST (eresolve_tac [conjE] ORELSE' hyp_subst_tac)); -by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analyze]) 1); +by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1); qed "Enemy_not_see_encrypted_key"; @@ -839,25 +831,25 @@ goal thy "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ \ evs : traces; i~=j \ -\ |] ==> K ~: analyze (sees (Friend j) evs)"; -br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1; +\ |] ==> 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]))); qed "Friend_not_see_encrypted_key"; goal thy "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ \ A ~: {Friend i, Server}; \ \ evs : traces \ -\ |] ==> K ~: analyze (sees A evs)"; +\ |] ==> K ~: analz (sees A evs)"; by (eres_inst_tac [("P", "A~:?X")] rev_mp 1); 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 ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1; +br ([analz_mono, Enemy_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"; @@ -866,7 +858,7 @@ (*Neatly packaged, perhaps in a useless form*) goalw thy [knownBy_def] "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ \ evs : traces \ \ |] ==> knownBy evs K <= {Friend i, Server}"; @@ -887,269 +879,38 @@ \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ \ evs : traces; i~=k \ \ |] ==> \ -\ K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; +\ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; be rev_mp 1; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); by (Step_tac 1); -by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1); +by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); val Enemy_not_see_encrypted_key_lemma = result(); -by (asm_full_simp_tac - (!simpset addsimps (pushes @ - [analyze_subset_parts RS contra_subsetD, - traces_ConsE RS Enemy_not_see_serverKey])) 1); - -by (asm_full_simp_tac - (!simpset addsimps [analyze_subset_parts RS keysFor_mono RS contra_subsetD, - traces_ConsE RS new_keys_not_used]) 1); -by (Fast_tac 1); - - - - -(*Precisely formulated as needed below. Perhaps redundant, as simplification - with the aid of analyze_subset_parts RS contra_subsetD might do the - same thing.*) -goal thy - "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ -\ Key (serverKey A) ~: \ -\ analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))"; -br (analyze_subset_parts RS contra_subsetD) 1; -by (Asm_simp_tac 1); -qed "insert_not_analyze_serverKey"; - - - - -by (asm_full_simp_tac - (!simpset addsimps (pushes @ - [insert_not_analyze_serverKey, - traces_ConsE RS insert_not_analyze_serverKey])) 1); - - -by (stac analyze_insert_Crypt 1); - - - - - - - - - -(*NS3, case 1: that message from the Server was just sent*) -by (asm_full_simp_tac (!simpset addsimps pushes) 1); - -(*NS3, case 2: that message from the Server was sent earlier*) -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); -by (mp_tac 1); -by (asm_full_simp_tac (!simpset addsimps pushes) 1); - -by (Step_tac 1); -by (asm_full_simp_tac - (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1); - - - -(*pretend we have the right lemma!*) -by (subgoal_tac "(EX evt. X = (Crypt {|Key(newK evt), Agent(Friend ia)|} (serverKey B)))" 1); -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); -by (asm_full_simp_tac (!simpset addsimps pushes) 1); +(*Precisely formulated as needed below. Perhaps redundant, as simplification + 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 |] ==> \ +\ Key (serverKey A) ~: \ +\ analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))"; +br (analz_subset_parts RS contra_subsetD) 1; +by (Asm_simp_tac 1); +qed "insert_not_analz_serverKey"; -by (excluded_middle_tac "ia=k" 1); -(*Case where the key is compromised*) -by (hyp_subst_tac 2); -by (stac insert_commute 2); (*Pushes in the "insert X" for simplification*) -by (Asm_full_simp_tac 2); - - - -by (asm_full_simp_tac (!simpset addsimps pushes) 1); - -by (REPEAT_FIRST Safe_step_tac); -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); - - -by (REPEAT (Safe_step_tac 1)); - - - -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); - -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); - -by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*deletes the bad implication*) -by ((forward_tac [Says_Server_message_form] THEN' - fast_tac (!claset addSEs [traces_ConsE])) 1); -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; proof_timing:=true; -(*Case where the key is secure*) -by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); -by (asm_full_simp_tac - (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1); - - - -by (full_simp_tac (!simpset addsimps [insert_Key_Agent_delay, - insert_Key_Crypt_delay]) 1); - -by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1); -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac)); - - -by (asm_full_simp_tac - (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1); - - -by (stac insert_commute 1); (*Pushes in the "insert X" for simplification*) -by (stac analyze_insert_Crypt 1); - -by (asm_full_simp_tac - (!simpset addsimps [insert_not_analyze_serverKey, - traces_ConsE RS insert_not_analyze_serverKey]) 1); - - - 1. !!evs A B K NA S X evsa evs' ia evs'a. - [| i ~= k; j ~= k; - Says S (Friend ia) - (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) # - evs' : - traces; - Friend ia ~= B; - Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} : - setOfList evs'; - Says Server (Friend i) - (Crypt - {|N, Agent (Friend j), Key (newK evs'a), - Crypt {|Key (newK evs'a), Agent (Friend i)|} - (serverKey (Friend j))|} - K') : - setOfList evs'; - Key (newK evs'a) ~: - analyze - (insert - (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) - (insert (Key (serverKey (Friend k))) (sees Enemy evs'))); - length evs'a < length evs' |] ==> - Key (newK evs'a) ~: - analyze - (insert X - (insert - (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) - (insert (Key (serverKey (Friend k))) (sees Enemy evs')))) - - -by (Asm_full_simp_tac 1); - - -by (Simp_tac 2); - - -by (Simp_tac 2); - -by (simp_tac (HOL_ss addsimps [insert_commute]) 2); - - -by (simp_tac (HOL_ss addsimps [analyze_insert_insert]) 2); -by (Asm_full_simp_tac 2); -by (simp_tac (!simpset addsimps [insert_absorb]) 2); - - -by (stac analyze_insert_Decrypt 2); - - -goal thy "analyze (insert X (insert Y H)) = analyze (insert X (analyze (insert Y H)))"; -br analyze_insert_cong 1; -by (Simp_tac 1); -qed "analyze_insert_insert"; - - - - - - - - 1. !!evs A B K NA S X evsa evs' ia evs'a. - [| i ~= k; j ~= k; - Says S (Friend ia) - (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) # - evs' : - traces; - Friend ia ~= B; - Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} : - setOfList evs'; - Says Server (Friend i) - (Crypt - {|N, Agent (Friend j), Key (newK evs'a), - Crypt {|Key (newK evs'a), Agent (Friend i)|} - (serverKey (Friend j))|} - K') : - setOfList evs'; - length evs'a < length evs'; ia ~= k; - Key (newK evs'a) ~: - analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')) |] ==> - Key (newK evs'a) ~: - analyze - (insert X - (insert - (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) - (insert (Key (serverKey (Friend k))) (sees Enemy evs')))) - - -by (ALLGOALS Asm_full_simp_tac); - -by (Asm_full_simp_tac 1); - -by (asm_simp_tac (!simpset addsimps [insert_not_analyze_serverKey]) 1); -fr insert_not_analyze_serverKey; -by (fast_tac (!claset addSEs [traces_ConsE]) 1); - -by (forward_tac [traces_ConsE] 1); - - - -by (asm_full_simp_tac (!simpset addsimps [analyze_subset_parts RS contra_subsetD]) 1); - - - -auto(); - -by (REPEAT_FIRST (resolve_tac [conjI, impI] (*DELETE NEXT TWO LINES??*) - ORELSE' eresolve_tac [conjE] - ORELSE' hyp_subst_tac)); - -by (forward_tac [Says_Server_message_form] 2); - -bd Says_Server_message_form 2; -by (fast_tac (!claset addSEs [traces_ConsE]) 2); -auto(); -by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay]))); - -(*SUBGOAL 1: use analyze_insert_Crypt to pull out - Crypt{|...|} (serverKey (Friend i)) - SUBGOAL 2: cannot do this, as we don't seem to have ia~=j -*) - - - -qed "Enemy_not_see_encrypted_key"; - -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; - - YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; @@ -1161,9 +922,9 @@ goal thy "!!evs. evs : traces ==> \ \ ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \ -\ : setOfList evs --> \ -\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \ -\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)"; +\ : set_of_list evs --> \ +\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \ +\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)"; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) by (Step_tac 1); @@ -1200,10 +961,10 @@ by (Best_tac 2); by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); -be Crypt_synthesize 1; -be Key_synthesize 2; +be Crypt_synth 1; +be Key_synth 2; -(*Split up the possibilities of that message being synthesized...*) +(*Split up the possibilities of that message being synthd...*) by (Step_tac 1); by (Best_tac 6); diff -r 947a34e00d1e -r 2809adb15eb0 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Mon Aug 19 11:19:16 1996 +0200 +++ b/src/HOL/Auth/Event.thy Mon Aug 19 11:19:55 1996 +0200 @@ -60,7 +60,7 @@ constdefs knownBy :: [event list, msg] => agent set - "knownBy evs X == {A. X: analyze (sees A evs)}" + "knownBy evs X == {A. X: analz (sees A evs)}" (*Agents generate "random" nonces. Different traces always yield @@ -95,7 +95,7 @@ (*The enemy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1.*) Fake "[| evs: traces; B ~= Enemy; - X: synthesize(analyze(sees Enemy evs)) + X: synth(analz(sees Enemy evs)) |] ==> (Says Enemy B X) # evs : traces" NS1 "[| evs: traces; A ~= Server @@ -118,15 +118,15 @@ (serverKey A))) # evs'; A = Friend i; - (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs' + (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs' |] ==> (Says A B X) # evs : traces" (*Initial version of NS2 had {|Agent A, Agent B, Key (newK evs), Nonce NA|} - for the encrypted part; the version above is LESS transparent, hence - maybe HARDER to prove. Also it is precisely as in the BAN paper. + for the encrypted part; the version above is LESS explicit, hence + HARDER to prove. Also it is precisely as in the BAN paper. *) end diff -r 947a34e00d1e -r 2809adb15eb0 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Mon Aug 19 11:19:16 1996 +0200 +++ b/src/HOL/Auth/Message.ML Mon Aug 19 11:19:55 1996 +0200 @@ -4,30 +4,12 @@ Copyright 1996 University of Cambridge Datatypes of agents and messages; -Inductive relations "parts", "analyze" and "synthesize" +Inductive relations "parts", "analz" and "synth" *) open Message; -(**************** INSTALL CENTRALLY SOMEWHERE? ****************) - -(*Maybe swap the safe_tac and simp_tac lines?**) -fun auto_tac (cs,ss) = - TRY (safe_tac cs) THEN - ALLGOALS (asm_full_simp_tac ss) THEN - REPEAT (FIRSTGOAL (best_tac (cs addss ss))); - -fun Auto_tac() = auto_tac (!claset, !simpset); - -fun auto() = by (Auto_tac()); - -fun impOfSubs th = th RSN (2, rev_subsetD); - -(**************** INSTALL CENTRALLY SOMEWHERE? ****************) - - - (** Inverse of keys **) goal thy "!!K K'. (invKey K = invKey K') = (K=K')"; @@ -172,7 +154,7 @@ by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1); qed "parts_UN1"; -(*Added to simplify arguments to parts, analyze and synthesize*) +(*Added to simplify arguments to parts, analz and synth*) Addsimps [parts_Un, parts_UN, parts_UN1]; goal thy "insert X (parts H) <= parts(insert X H)"; @@ -259,362 +241,360 @@ parts_insert_Key, parts_insert_Crypt, parts_insert_MPair]; -(**** Inductive relation "analyze" ****) +(**** Inductive relation "analz" ****) val major::prems = -goal thy "[| {|X,Y|} : analyze H; \ -\ [| X : analyze H; Y : analyze H |] ==> P \ +goal thy "[| {|X,Y|} : analz H; \ +\ [| X : analz H; Y : analz H |] ==> P \ \ |] ==> P"; by (cut_facts_tac [major] 1); brs prems 1; -by (REPEAT (eresolve_tac [asm_rl, analyze.Fst, analyze.Snd] 1)); -qed "MPair_analyze"; +by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); +qed "MPair_analz"; -AddIs [analyze.Inj]; -AddSEs [MPair_analyze]; -AddDs [analyze.Decrypt]; +AddIs [analz.Inj]; +AddSEs [MPair_analz]; +AddDs [analz.Decrypt]; -Addsimps [analyze.Inj]; +Addsimps [analz.Inj]; -goal thy "H <= analyze(H)"; +goal thy "H <= analz(H)"; by (Fast_tac 1); -qed "analyze_increasing"; +qed "analz_increasing"; -goal thy "analyze H <= parts H"; +goal thy "analz H <= parts H"; by (rtac subsetI 1); -be analyze.induct 1; +be analz.induct 1; by (ALLGOALS Fast_tac); -qed "analyze_subset_parts"; +qed "analz_subset_parts"; -bind_thm ("not_parts_not_analyze", analyze_subset_parts RS contra_subsetD); +bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); -goal thy "parts (analyze H) = parts H"; +goal thy "parts (analz H) = parts H"; br equalityI 1; -br (analyze_subset_parts RS parts_mono RS subset_trans) 1; +br (analz_subset_parts RS parts_mono RS subset_trans) 1; by (Simp_tac 1); -by (fast_tac (!claset addDs [analyze_increasing RS parts_mono RS subsetD]) 1); -qed "parts_analyze"; -Addsimps [parts_analyze]; +by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); +qed "parts_analz"; +Addsimps [parts_analz]; -goal thy "analyze (parts H) = parts H"; +goal thy "analz (parts H) = parts H"; by (Auto_tac()); -be analyze.induct 1; +be analz.induct 1; by (Auto_tac()); -qed "analyze_parts"; -Addsimps [analyze_parts]; +qed "analz_parts"; +Addsimps [analz_parts]; (*Monotonicity; Lemma 1 of Lowe*) -goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)"; +goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); -qed "analyze_mono"; +qed "analz_mono"; (** General equational properties **) -goal thy "analyze{} = {}"; +goal thy "analz{} = {}"; by (Step_tac 1); -be analyze.induct 1; +be analz.induct 1; by (ALLGOALS Fast_tac); -qed "analyze_empty"; -Addsimps [analyze_empty]; +qed "analz_empty"; +Addsimps [analz_empty]; -(*Converse fails: we can analyze more from the union than from the +(*Converse fails: we can analz more from the union than from the separate parts, as a key in one might decrypt a message in the other*) -goal thy "analyze(G) Un analyze(H) <= analyze(G Un H)"; -by (REPEAT (ares_tac [Un_least, analyze_mono, Un_upper1, Un_upper2] 1)); -qed "analyze_Un"; +goal thy "analz(G) Un analz(H) <= analz(G Un H)"; +by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); +qed "analz_Un"; -goal thy "insert X (analyze H) <= analyze(insert X H)"; -by (fast_tac (!claset addEs [impOfSubs analyze_mono]) 1); -qed "analyze_insert"; +goal thy "insert X (analz H) <= analz(insert X H)"; +by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1); +qed "analz_insert"; (** Rewrite rules for pulling out atomic messages **) -goal thy "analyze (insert (Agent agt) H) = insert (Agent agt) (analyze H)"; -by (rtac (analyze_insert RSN (2, equalityI)) 1); +goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; +by (rtac (analz_insert RSN (2, equalityI)) 1); br subsetI 1; -be analyze.induct 1; +be analz.induct 1; (*Simplification breaks up equalities between messages; how to make it work for fast_tac??*) by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Agent"; +qed "analz_insert_Agent"; -goal thy "analyze (insert (Nonce N) H) = insert (Nonce N) (analyze H)"; -by (rtac (analyze_insert RSN (2, equalityI)) 1); +goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; +by (rtac (analz_insert RSN (2, equalityI)) 1); br subsetI 1; -be analyze.induct 1; +be analz.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Nonce"; +qed "analz_insert_Nonce"; (*Can only pull out Keys if they are not needed to decrypt the rest*) goalw thy [keysFor_def] - "!!K. K ~: keysFor (analyze H) ==> \ -\ analyze (insert (Key K) H) = insert (Key K) (analyze H)"; -by (rtac (analyze_insert RSN (2, equalityI)) 1); + "!!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 analyze.induct 1; +be analz.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Key"; +qed "analz_insert_Key"; -goal thy "analyze (insert {|X,Y|} H) = \ -\ insert {|X,Y|} (analyze (insert X (insert Y H)))"; +goal thy "analz (insert {|X,Y|} H) = \ +\ insert {|X,Y|} (analz (insert X (insert Y H)))"; br equalityI 1; br subsetI 1; -be analyze.induct 1; +be analz.induct 1; by (Auto_tac()); -be analyze.induct 1; -by (ALLGOALS (deepen_tac (!claset addIs [analyze.Fst, analyze.Snd, analyze.Decrypt]) 0)); -qed "analyze_insert_MPair"; +be analz.induct 1; +by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); +qed "analz_insert_MPair"; (*Can pull out enCrypted message if the Key is not known*) -goal thy "!!H. Key (invKey K) ~: analyze H ==> \ -\ analyze (insert (Crypt X K) H) = \ -\ insert (Crypt X K) (analyze H)"; -by (rtac (analyze_insert RSN (2, equalityI)) 1); +goal thy "!!H. Key (invKey K) ~: analz H ==> \ +\ analz (insert (Crypt X K) H) = \ +\ insert (Crypt X K) (analz H)"; +by (rtac (analz_insert RSN (2, equalityI)) 1); br subsetI 1; -be analyze.induct 1; +be analz.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Crypt"; +qed "analz_insert_Crypt"; -goal thy "!!H. Key (invKey K) : analyze H ==> \ -\ analyze (insert (Crypt X K) H) <= \ -\ insert (Crypt X K) (analyze (insert X H))"; +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 (eres_inst_tac [("za","x")] analyze.induct 1); +by (eres_inst_tac [("za","x")] analz.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); val lemma1 = result(); -goal thy "!!H. Key (invKey K) : analyze H ==> \ -\ insert (Crypt X K) (analyze (insert X H)) <= \ -\ analyze (insert (Crypt X K) H)"; +goal thy "!!H. Key (invKey K) : analz H ==> \ +\ insert (Crypt X K) (analz (insert X H)) <= \ +\ analz (insert (Crypt X K) H)"; by (Auto_tac()); -by (eres_inst_tac [("za","x")] analyze.induct 1); +by (eres_inst_tac [("za","x")] analz.induct 1); by (Auto_tac()); -by (best_tac (!claset addIs [subset_insertI RS analyze_mono RS subsetD, - analyze.Decrypt]) 1); +by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, + analz.Decrypt]) 1); val lemma2 = result(); -goal thy "!!H. Key (invKey K) : analyze H ==> \ -\ analyze (insert (Crypt X K) H) = \ -\ insert (Crypt X K) (analyze (insert X H))"; +goal thy "!!H. Key (invKey K) : analz H ==> \ +\ analz (insert (Crypt X K) H) = \ +\ insert (Crypt X K) (analz (insert X H))"; by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); -qed "analyze_insert_Decrypt"; +qed "analz_insert_Decrypt"; (*Case analysis: either the message is secure, or it is not! Use with expand_if; apparently split_tac does not cope with patterns - such as "analyze (insert (Crypt X' K) H)" *) -goal thy "analyze (insert (Crypt X' K) H) = \ -\ (if (Key (invKey K) : analyze H) then \ -\ insert (Crypt X' K) (analyze (insert X' H)) \ -\ else insert (Crypt X' K) (analyze H))"; -by (excluded_middle_tac "Key (invKey K) : analyze H " 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [analyze_insert_Crypt, - analyze_insert_Decrypt]))); -qed "analyze_Crypt_if"; + such as "analz (insert (Crypt X' K) H)" *) +goal thy "analz (insert (Crypt X' K) H) = \ +\ (if (Key (invKey K) : analz H) then \ +\ insert (Crypt X' K) (analz (insert X' H)) \ +\ 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]))); +qed "analz_Crypt_if"; -Addsimps [analyze_insert_Agent, analyze_insert_Nonce, - analyze_insert_Key, analyze_insert_MPair, - analyze_Crypt_if]; +Addsimps [analz_insert_Agent, analz_insert_Nonce, + analz_insert_Key, analz_insert_MPair, + analz_Crypt_if]; (*This rule supposes "for the sake of argument" that we have the key.*) -goal thy "analyze (insert (Crypt X K) H) <= \ -\ insert (Crypt X K) (analyze (insert X H))"; +goal thy "analz (insert (Crypt X K) H) <= \ +\ insert (Crypt X K) (analz (insert X H))"; br subsetI 1; -be analyze.induct 1; +be analz.induct 1; by (Auto_tac()); -qed "analyze_insert_Crypt_subset"; +qed "analz_insert_Crypt_subset"; (** Idempotence and transitivity **) -goal thy "!!H. X: analyze (analyze H) ==> X: analyze H"; -be analyze.induct 1; +goal thy "!!H. X: analz (analz H) ==> X: analz H"; +be analz.induct 1; by (ALLGOALS Fast_tac); -qed "analyze_analyzeE"; -AddSEs [analyze_analyzeE]; +qed "analz_analzE"; +AddSEs [analz_analzE]; -goal thy "analyze (analyze H) = analyze H"; +goal thy "analz (analz H) = analz H"; by (Fast_tac 1); -qed "analyze_idem"; -Addsimps [analyze_idem]; +qed "analz_idem"; +Addsimps [analz_idem]; -goal thy "!!H. [| X: analyze G; G <= analyze H |] ==> X: analyze H"; -by (dtac analyze_mono 1); +goal thy "!!H. [| X: analz G; G <= analz H |] ==> X: analz H"; +by (dtac analz_mono 1); by (Fast_tac 1); -qed "analyze_trans"; +qed "analz_trans"; (*Cut; Lemma 2 of Lowe*) -goal thy "!!H. [| X: analyze H; Y: analyze (insert X H) |] ==> Y: analyze H"; -be analyze_trans 1; +goal thy "!!H. [| X: analz H; Y: analz (insert X H) |] ==> Y: analz H"; +be analz_trans 1; by (Fast_tac 1); -qed "analyze_cut"; +qed "analz_cut"; (*Cut can be proved easily by induction on - "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H" + "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H" *) -(** A congruence rule for "analyze" **) +(** A congruence rule for "analz" **) -goal thy "!!H. [| analyze G <= analyze G'; analyze H <= analyze H' \ -\ |] ==> analyze (G Un H) <= analyze (G' Un H')"; +goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \ +\ |] ==> analz (G Un H) <= analz (G' Un H')"; by (Step_tac 1); -be analyze.induct 1; -by (ALLGOALS (best_tac (!claset addIs [analyze_mono RS subsetD]))); -qed "analyze_subset_cong"; +be analz.induct 1; +by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); +qed "analz_subset_cong"; -goal thy "!!H. [| analyze G = analyze G'; analyze H = analyze H' \ -\ |] ==> analyze (G Un H) = analyze (G' Un H')"; -by (REPEAT_FIRST (ares_tac [equalityI, analyze_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)); -qed "analyze_cong"; +qed "analz_cong"; -goal thy "!!H. analyze H = analyze H' ==> \ -\ analyze (insert X H) = analyze (insert X H')"; +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 analyze_cong)) 1); -qed "analyze_insert_cong"; + setloop (rtac analz_cong)) 1); +qed "analz_insert_cong"; -(*If there are no pairs or encryptions then analyze does nothing*) +(*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 |] ==> \ -\ analyze H = H"; +\ analz H = H"; by (Step_tac 1); -be analyze.induct 1; +be analz.induct 1; by (ALLGOALS Fast_tac); -qed "analyze_trivial"; +qed "analz_trivial"; (*Helps to prove Fake cases*) -goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)"; -be analyze.induct 1; -by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analyze_mono]))); +goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; +be analz.induct 1; +by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono]))); val lemma = result(); -goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)"; +goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; by (fast_tac (!claset addIs [lemma] - addEs [impOfSubs analyze_mono]) 1); -qed "analyze_UN_analyze"; -Addsimps [analyze_UN_analyze]; + addEs [impOfSubs analz_mono]) 1); +qed "analz_UN_analz"; +Addsimps [analz_UN_analz]; -(**** Inductive relation "synthesize" ****) +(**** Inductive relation "synth" ****) -AddIs synthesize.intrs; +AddIs synth.intrs; -goal thy "H <= synthesize(H)"; +goal thy "H <= synth(H)"; by (Fast_tac 1); -qed "synthesize_increasing"; +qed "synth_increasing"; (*Monotonicity*) -goalw thy synthesize.defs "!!G H. G<=H ==> synthesize(G) <= synthesize(H)"; +goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)"; by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); -qed "synthesize_mono"; +qed "synth_mono"; (** Unions **) -(*Converse fails: we can synthesize more from the union than from the +(*Converse fails: we can synth more from the union than from the separate parts, building a compound message using elements of each.*) -goal thy "synthesize(G) Un synthesize(H) <= synthesize(G Un H)"; -by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1)); -qed "synthesize_Un"; +goal thy "synth(G) Un synth(H) <= synth(G Un H)"; +by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); +qed "synth_Un"; -goal thy "insert X (synthesize H) <= synthesize(insert X H)"; -by (fast_tac (!claset addEs [impOfSubs synthesize_mono]) 1); -qed "synthesize_insert"; +goal thy "insert X (synth H) <= synth(insert X H)"; +by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1); +qed "synth_insert"; (** Idempotence and transitivity **) -goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H"; -be synthesize.induct 1; +goal thy "!!H. X: synth (synth H) ==> X: synth H"; +be synth.induct 1; by (ALLGOALS Fast_tac); -qed "synthesize_synthesizeE"; -AddSEs [synthesize_synthesizeE]; +qed "synth_synthE"; +AddSEs [synth_synthE]; -goal thy "synthesize (synthesize H) = synthesize H"; +goal thy "synth (synth H) = synth H"; by (Fast_tac 1); -qed "synthesize_idem"; +qed "synth_idem"; -goal thy "!!H. [| X: synthesize G; G <= synthesize H |] ==> X: synthesize H"; -by (dtac synthesize_mono 1); +goal thy "!!H. [| X: synth G; G <= synth H |] ==> X: synth H"; +by (dtac synth_mono 1); by (Fast_tac 1); -qed "synthesize_trans"; +qed "synth_trans"; (*Cut; Lemma 2 of Lowe*) -goal thy "!!H. [| X: synthesize H; Y: synthesize (insert X H) \ -\ |] ==> Y: synthesize H"; -be synthesize_trans 1; +goal thy "!!H. [| X: synth H; Y: synth (insert X H) |] ==> Y: synth H"; +be synth_trans 1; by (Fast_tac 1); -qed "synthesize_cut"; +qed "synth_cut"; (*Can only produce a nonce or key if it is already known, - but can synthesize a pair or encryption from its components...*) -val mk_cases = synthesize.mk_cases msg.simps; + but can synth a pair or encryption from its components...*) +val mk_cases = synth.mk_cases msg.simps; -(*NO Agent_synthesize, as any Agent name can be synthesized*) -val Nonce_synthesize = mk_cases "Nonce n : synthesize H"; -val Key_synthesize = mk_cases "Key K : synthesize H"; -val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H"; -val Crypt_synthesize = mk_cases "Crypt X K : synthesize H"; +(*NO Agent_synth, as any Agent name can be synthd*) +val Nonce_synth = mk_cases "Nonce n : synth H"; +val Key_synth = mk_cases "Key K : synth H"; +val MPair_synth = mk_cases "{|X,Y|} : synth H"; +val Crypt_synth = mk_cases "Crypt X K : synth H"; -AddSEs [Nonce_synthesize, Key_synthesize, MPair_synthesize, Crypt_synthesize]; +AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth]; -goal thy "(Nonce N : synthesize H) = (Nonce N : H)"; +goal thy "(Nonce N : synth H) = (Nonce N : H)"; by (Fast_tac 1); -qed "Nonce_synthesize_eq"; +qed "Nonce_synth_eq"; -goal thy "(Key K : synthesize H) = (Key K : H)"; +goal thy "(Key K : synth H) = (Key K : H)"; by (Fast_tac 1); -qed "Key_synthesize_eq"; +qed "Key_synth_eq"; -Addsimps [Nonce_synthesize_eq, Key_synthesize_eq]; +Addsimps [Nonce_synth_eq, Key_synth_eq]; goalw thy [keysFor_def] - "keysFor (synthesize H) = keysFor H Un invKey``{K. Key K : H}"; + "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; by (Fast_tac 1); -qed "keysFor_synthesize"; -Addsimps [keysFor_synthesize]; +qed "keysFor_synth"; +Addsimps [keysFor_synth]; -(*** Combinations of parts, analyze and synthesize ***) +(*** Combinations of parts, analz and synth ***) -goal thy "parts (synthesize H) = parts H Un synthesize H"; +goal thy "parts (synth H) = parts H Un synth H"; br equalityI 1; br subsetI 1; be parts.induct 1; by (ALLGOALS - (best_tac (!claset addIs ((synthesize_increasing RS parts_mono RS subsetD) + (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) ::parts.intrs)))); -qed "parts_synthesize"; -Addsimps [parts_synthesize]; +qed "parts_synth"; +Addsimps [parts_synth]; -goal thy "analyze (synthesize H) = analyze H Un synthesize H"; +goal thy "analz (synth H) = analz H Un synth H"; br equalityI 1; br subsetI 1; -be analyze.induct 1; +be analz.induct 1; by (best_tac - (!claset addIs [synthesize_increasing RS analyze_mono RS subsetD]) 5); + (!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5); (*Strange that best_tac just can't hack this one...*) -by (ALLGOALS (deepen_tac (!claset addIs analyze.intrs) 0)); -qed "analyze_synthesize"; -Addsimps [analyze_synthesize]; +by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); +qed "analz_synth"; +Addsimps [analz_synth]; (*Hard to prove; still needed now that there's only one Enemy?*) -goal thy "analyze (UN i. synthesize (H i)) = \ -\ analyze (UN i. H i) Un (UN i. synthesize (H i))"; +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 analyze.induct 1; +be analz.induct 1; by (best_tac - (!claset addEs [impOfSubs synthesize_increasing, - impOfSubs analyze_mono]) 5); + (!claset addEs [impOfSubs synth_increasing, + impOfSubs analz_mono]) 5); by (Best_tac 1); -by (deepen_tac (!claset addIs [analyze.Fst]) 0 1); -by (deepen_tac (!claset addIs [analyze.Snd]) 0 1); -by (deepen_tac (!claset addSEs [analyze.Decrypt] - addIs [analyze.Decrypt]) 0 1); -qed "analyze_UN1_synthesize"; -Addsimps [analyze_UN1_synthesize]; +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); +qed "analz_UN1_synth"; +Addsimps [analz_UN1_synth]; diff -r 947a34e00d1e -r 2809adb15eb0 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Mon Aug 19 11:19:16 1996 +0200 +++ b/src/HOL/Auth/Message.thy Mon Aug 19 11:19:55 1996 +0200 @@ -4,7 +4,7 @@ Copyright 1996 University of Cambridge Datatypes of agents and messages; -Inductive relations "parts", "analyze" and "synthesize" +Inductive relations "parts", "analz" and "synth" *) Message = Arith + @@ -77,38 +77,29 @@ Body "Crypt X K : parts H ==> X : parts H" -(** Inductive definition of "analyze" -- what can be broken down from a set of +(** Inductive definition of "analz" -- what can be broken down from a set of messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys. **) -consts analyze :: msg set => msg set -inductive "analyze H" +consts analz :: msg set => msg set +inductive "analz H" intrs - Inj "X: H ==> X: analyze H" - - Fst "{|X,Y|} : analyze H ==> X : analyze H" - - Snd "{|X,Y|} : analyze H ==> Y : analyze H" - - Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H - |] ==> X : analyze H" + Inj "X: H ==> X: analz H" + Fst "{|X,Y|} : analz H ==> X : analz H" + Snd "{|X,Y|} : analz H ==> Y : analz H" + Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H" -(** Inductive definition of "synthesize" -- what can be built up from a set of +(** Inductive definition of "synth" -- what can be built up from a set of messages. A form of upward closure. Pairs can be built, messages encrypted with known keys. Agent names may be quoted. **) -consts synthesize :: msg set => msg set -inductive "synthesize H" +consts synth :: msg set => msg set +inductive "synth H" intrs - Inj "X: H ==> X: synthesize H" - - Agent "Agent agt : synthesize H" - - MPair "[| X: synthesize H; Y: synthesize H - |] ==> {|X,Y|} : synthesize H" - - Crypt "[| X: synthesize H; Key(K): synthesize H - |] ==> Crypt X K : synthesize H" + Inj "X: H ==> X: synth H" + Agent "Agent agt : synth H" + MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" + Crypt "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H" end