# HG changeset patch # User paulson # Date 842288282 -7200 # Node ID 0ff58b41c037cf2280b8c325b52d8fb5d71318e6 # Parent 9e626f86e3352fa5c6b073d11ef3391eeacffe6b "bad" set simplifies statements of many theorems diff -r 9e626f86e335 -r 0ff58b41c037 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Mon Sep 09 18:53:41 1996 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Mon Sep 09 18:58:02 1996 +0200 @@ -54,7 +54,7 @@ (*Enemy never sees another agent's shared key!*) goal thy - "!!evs. [| evs : ns_shared; A ~= Enemy; A ~: Friend``leaked |] ==> \ + "!!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; @@ -67,45 +67,37 @@ bind_thm ("Enemy_not_analz_shrK", [analz_subset_parts, Enemy_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 [Enemy_not_see_shrK, Enemy_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 - REDO USING 'BAD' SET TO AVOID CASE SPLIT!*) + 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=Enemy ==> R; \ -\ !!i. [| A = Friend i; i: leaked |] ==> R \ +\ A:bad ==> R \ \ |] ==> R"; br ccontr 1; br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; -br notI 3; -be imageE 3; by (swap_res_tac prems 2); -by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems))); +by (ALLGOALS (fast_tac (!claset addIs prems))); qed "Enemy_see_shrK_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_shrK_E, Enemy_analz_shrK_E]; -(*Not for Addsimps -- it can cause goals to blow up!*) goal thy "!!evs. evs : ns_shared ==> \ -\ (Key (shrK A) : analz (sees Enemy evs)) = \ -\ (A=Enemy | A : Friend``leaked)"; +\ (Key (shrK A) : analz (sees Enemy evs)) = (A : bad)"; by (best_tac (!claset addDs [impOfSubs analz_subset_parts] addIs [impOfSubs (subset_insertI RS analz_mono)] addss (!simpset)) 1); qed "shrK_mem_analz"; +Addsimps [shrK_mem_analz]; + (*** Future keys can't be seen or used! ***) @@ -210,9 +202,9 @@ goal thy "!!evs. evs : ns_shared ==> \ \ ALL A NA B K X. \ -\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ +\ Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A) \ \ : parts (sees Enemy evs) & \ -\ A ~= Enemy & A ~: Friend``leaked --> \ +\ A ~: bad --> \ \ (EX evt:ns_shared. K = newK evt & \ \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; be ns_shared.induct 1; @@ -223,18 +215,17 @@ (*Remaining cases are Fake and NS2*) by (fast_tac (!claset addSDs [spec]) 2); (*Now for the Fake case*) -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); +by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); qed_spec_mp "encrypted_form"; (*If such a message is sent with a bad key then the Enemy sees it (even if he didn't send it in the first place).*) goal thy - "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ -\ : set_of_list evs; \ -\ A = Enemy | A : Friend``leaked |] \ + "!!evs. [| Says S A (Crypt {|N, B, K, X|} (shrK A)) : set_of_list evs; \ +\ A : bad |] \ \ ==> X : analz (sees Enemy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj] addss (!simpset)) 1); @@ -251,7 +242,7 @@ \ ==> (EX evt:ns_shared. 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 = Enemy | A : Friend``leaked" 1); +by (excluded_middle_tac "A : bad" 1); by (fast_tac (!claset addIs [bad_encrypted_form]) 2); by (forward_tac [encrypted_form] 1); br (parts.Inj RS conjI) 1; @@ -373,7 +364,7 @@ goal thy "!!evs. [| X : synth (analz (sees Enemy evs)); \ \ Crypt X' (shrK C) : parts{X}; \ -\ C ~= Enemy; C ~: Friend``leaked; evs : ns_shared |] \ +\ C ~: bad; evs : ns_shared |] \ \ ==> Crypt X' (shrK C) : parts (sees Enemy evs)"; by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] addDs [impOfSubs parts_insert_subset_Un] @@ -394,8 +385,8 @@ But if Enemy knows C's key then he could send all sorts of nonsense.*) goal thy "!!evs. evs : ns_shared ==> \ -\ EX X'. ALL C. \ -\ C ~= Enemy & C ~: Friend``leaked --> \ +\ EX X'. ALL C. \ +\ C ~: bad --> \ \ (ALL S A Y. Says S A Y : set_of_list evs --> \ \ (ALL N B X. Crypt {|N, Agent B, Key K, X|} (shrK C) : parts{Y} --> \ \ X=X'))"; @@ -433,7 +424,7 @@ \ Says S' A' \ \ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ \ : set_of_list evs; \ -\ evs : ns_shared; C ~= Enemy; C ~: Friend``leaked; C' ~= Enemy; C' ~: Friend``leaked |] ==> X = X'"; +\ evs : ns_shared; C ~= Enemy; C ~: bad; C' ~: bad |] ==> X = X'"; bd lemma 1; be exE 1; (*Duplicate the assumption*) @@ -448,9 +439,9 @@ (*Crucial secrecy property: Enemy does not see the keys sent in msg NS2*) goal thy - "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ -\ i ~: leaked; j ~: leaked; evs : ns_shared \ + "!!evs. [| Says Server A \ +\ (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ +\ A ~: bad; B ~: bad; evs : ns_shared \ \ |] ==> \ \ K ~: analz (sees Enemy evs)"; be rev_mp 1; @@ -472,23 +463,21 @@ (*NS3: that message from the Server was sent earlier*) by (mp_tac 1); by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1); -by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac)); +by (Step_tac 1); by (enemy_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); ****************) -by (step_tac HOL_cs 1); +by (Step_tac 1); (**LEVEL 15 **) -by (excluded_middle_tac "ia : leaked" 1); +by (excluded_middle_tac "Friend i : bad" 1); +(*But this contradicts Key (newK evta) ~: analz (sees Enemy evsa) *) bd (Says_imp_sees_Enemy RS analz.Inj) 2; bd analz.Decrypt 2; -by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 2); +by (Asm_full_simp_tac 2); by (Fast_tac 2); -(*So now we know that Friend ia is a good agent*) +(*So now we know that (Friend i) is a good agent*) bd unique_session_keys 1; by (REPEAT_FIRST assume_tac); -by (ALLGOALS Full_simp_tac); -by (Step_tac 1); -by (auto_tac (!claset, !simpset addsimps [shrK_mem_analz])); +by (Auto_tac ()); qed "Enemy_not_see_encrypted_key"; diff -r 9e626f86e335 -r 0ff58b41c037 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Sep 09 18:53:41 1996 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Mon Sep 09 18:58:02 1996 +0200 @@ -75,7 +75,7 @@ (*Enemy never sees another agent's shared key! (unless it is leaked at start)*) goal thy - "!!evs. [| evs : otway; A ~= Enemy; A ~: Friend``leaked |] ==> \ + "!!evs. [| evs : otway; A ~: bad |] ==> \ \ Key (shrK A) ~: parts (sees Enemy evs)"; be otway.induct 1; by OR2_OR4_tac; @@ -88,31 +88,24 @@ bind_thm ("Enemy_not_analz_shrK", [analz_subset_parts, Enemy_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 [Enemy_not_see_shrK, Enemy_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=Enemy ==> R; \ -\ !!i. [| A = Friend i; i: leaked |] ==> R \ +\ A:bad ==> R \ \ |] ==> R"; br ccontr 1; br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; -br notI 3; -be imageE 3; by (swap_res_tac prems 2); -by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems))); +by (ALLGOALS (fast_tac (!claset addIs prems))); qed "Enemy_see_shrK_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_shrK_E, Enemy_analz_shrK_E]; @@ -348,10 +341,10 @@ (*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*) goal thy - "!!evs. [| Says Server (Friend j) \ -\ {|Ni, Crypt {|Ni, K|} (shrK (Friend i)), \ -\ Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs; \ -\ i ~: leaked; j ~: leaked; evs : otway |] ==> \ + "!!evs. [| Says Server A \ +\ {|NA, Crypt {|NA, K|} (shrK B), \ +\ Crypt {|NB, K|} (shrK A)|} : set_of_list evs; \ +\ A ~: bad; B ~: bad; evs : otway |] ==> \ \ K ~: analz (sees Enemy evs)"; be rev_mp 1; be otway.induct 1; @@ -392,7 +385,7 @@ goal thy "!!evs. [| X : synth (analz (sees Enemy evs)); \ \ Crypt X' (shrK C) : parts{X}; \ -\ C ~= Enemy; C ~: Friend``leaked; evs : otway |] \ +\ C ~: bad; evs : otway |] \ \ ==> Crypt X' (shrK C) : parts (sees Enemy evs)"; by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] addDs [impOfSubs parts_insert_subset_Un] @@ -414,7 +407,7 @@ goal thy "!!evs. evs : otway ==> \ \ EX A B. ALL C. \ -\ C ~= Enemy & C ~: Friend``leaked --> \ +\ C ~: bad --> \ \ (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); diff -r 9e626f86e335 -r 0ff58b41c037 src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Mon Sep 09 18:53:41 1996 +0200 +++ b/src/HOL/Auth/Shared.ML Mon Sep 09 18:58:02 1996 +0200 @@ -60,7 +60,7 @@ \ 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)); +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]; @@ -101,21 +101,20 @@ qed "shrK_notin_image_newK"; Addsimps [shrK_notin_image_newK]; - (*Agents see their own shared keys!*) goal thy "Key (shrK A) : sees A evs"; by (list.induct_tac "evs" 1); by (agent.induct_tac "A" 1); -by (Auto_tac ()); +by (auto_tac (!claset, !simpset addsimps [bad_def])); qed "sees_own_shrK"; -(*Enemy sees leaked shrKs!*) -goal thy "!!i. i: leaked ==> Key (shrK (Friend i)) : sees Enemy evs"; +(*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 ()); -qed "Enemy_sees_leaked"; +by (auto_tac (!claset, !simpset addsimps [bad_def])); +qed "Enemy_sees_bad"; -AddSIs [sees_own_shrK, Enemy_sees_leaked]; +AddSIs [sees_own_shrK, Enemy_sees_bad]; (** Specialized rewrite rules for (sees A (Says...#evs)) **) diff -r 9e626f86e335 -r 0ff58b41c037 src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Mon Sep 09 18:53:41 1996 +0200 +++ b/src/HOL/Auth/Shared.thy Mon Sep 09 18:58:02 1996 +0200 @@ -16,6 +16,9 @@ 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)" @@ -26,8 +29,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 = insert (Key (shrK Enemy)) (Key``shrK``Friend``leaked)" + initState_Enemy "initState Enemy = Key``shrK``bad" datatype (*Messages, and components of agent stores*) event = Says agent agent msg