# HG changeset patch # User paulson # Date 842283860 -7200 # Node ID 789c12ea0b30366d64677f4b79c43fed2b2cde8c # Parent d551e68b7a36b98a7daeacc24385c8472378bc2a Stronger proofs; work for Otway-Rees diff -r d551e68b7a36 -r 789c12ea0b30 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Mon Sep 09 17:34:24 1996 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Mon Sep 09 17:44:20 1996 +0200 @@ -54,7 +54,7 @@ (*Enemy never sees another agent's shared key!*) goal thy - "!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \ + "!!evs. [| evs : ns_shared; A ~= Enemy; A ~: Friend``leaked |] ==> \ \ Key (shrK A) ~: parts (sees Enemy evs)"; be ns_shared.induct 1; bd NS3_msg_in_parts_sees_Enemy 5; @@ -72,16 +72,21 @@ Enemy_not_analz_shrK, not_sym RSN (2, Enemy_not_analz_shrK)]; -(*We go to some trouble to preserve R in the 3rd subgoal*) +(*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!*) val major::prems = -goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ -\ evs : ns_shared; \ -\ A=Enemy ==> R \ +goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ +\ evs : ns_shared; \ +\ A=Enemy ==> R; \ +\ !!i. [| A = Friend i; i: leaked |] ==> 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 (ALLGOALS (fast_tac (!claset addIs prems))); +by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems))); qed "Enemy_see_shrK_E"; bind_thm ("Enemy_analz_shrK_E", @@ -91,23 +96,11 @@ AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; -(*No Friend will ever see another agent's shared key - (excluding the Enemy, who might transmit his). - The Server, of course, knows all shared keys.*) -goal thy - "!!evs. [| evs : ns_shared; A ~= Enemy; 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 (ALLGOALS Asm_simp_tac); -qed "Friend_not_see_shrK"; - - (*Not for Addsimps -- it can cause goals to blow up!*) goal thy - "!!evs. evs : ns_shared ==> \ -\ (Key (shrK A) \ -\ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ -\ (A=B | A=Enemy)"; + "!!evs. evs : ns_shared ==> \ +\ (Key (shrK A) : analz (sees Enemy evs)) = \ +\ (A=Enemy | A : Friend``leaked)"; by (best_tac (!claset addDs [impOfSubs analz_subset_parts] addIs [impOfSubs (subset_insertI RS analz_mono)] addss (!simpset)) 1); @@ -212,63 +205,54 @@ (*Describes the form of X when the following message is sent. The use of - "parts" strengthens the induction hyp for proving the Fake case*) + "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 ==> \ -\ ALL A NA B K X. \ -\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ -\ : parts (sees Enemy evs) & A ~= Enemy --> \ + "!!evs. evs : ns_shared ==> \ +\ ALL A NA B K X. \ +\ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ +\ : parts (sees Enemy evs) & \ +\ A ~= Enemy & A ~: Friend``leaked --> \ \ (EX evt:ns_shared. 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 (Step_tac 1); by (ALLGOALS Asm_full_simp_tac); +by (fast_tac (!claset addss (!simpset)) 1); (*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 Fake_parts_insert] +by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] addss (!simpset)) 1); qed_spec_mp "encrypted_form"; -(*For eliminating the A ~= Enemy condition from the previous result*) -goal thy - "!!evs. evs : ns_shared ==> \ -\ 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 ns_shared.induct 1; -by (ALLGOALS Asm_simp_tac); -(*We are left with NS3*) -by (subgoal_tac "S = Server | S = Enemy" 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 (ALLGOALS Full_simp_tac); -(*Final case. Clear out needless quantifiers to speed the following step*) -by (thin_tac "ALL x. ?P(x)" 1); -bd encrypted_form 1; -br (parts.Inj RS conjI) 1; -auto(); -qed_spec_mp "Server_or_Enemy"; +(*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 |] \ +\ ==> X : analz (sees Enemy evs)"; +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj] + addss (!simpset)) 1); +qed_spec_mp "bad_encrypted_form"; -(*Describes the form of X when the following message is sent; - use Says_Server_message_form if applicable*) + +(*EITHER describes the form of X when the following message is sent, + OR reduces it to the Fake case. + 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 |] \ +\ : 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); -by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); +\ X = (Crypt {|Key K, Agent A|} (shrK B))) | \ +\ X : analz (sees Enemy evs)"; +by (excluded_middle_tac "A = Enemy | A : Friend``leaked" 1); +by (fast_tac (!claset addIs [bad_encrypted_form]) 2); by (forward_tac [encrypted_form] 1); br (parts.Inj RS conjI) 1; by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); @@ -279,9 +263,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)) + Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==> + Key K : analz (sees Enemy evs) A more general formula must be proved inductively. @@ -302,8 +285,8 @@ by (best_tac (!claset addSEs partsEs addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un] - addss (!simpset)) 1); -(*NS4 and NS5*) + addss (!simpset)) 2); +(*Base, NS4 and NS5*) by (ALLGOALS (fast_tac (!claset addss (!simpset)))); result(); @@ -313,6 +296,9 @@ Delsimps [image_insert]; Addsimps [image_insert RS sym]; +Delsimps [image_Un]; +Addsimps [image_Un RS sym]; + goal thy "insert (Key (newK x)) (sees A evs) = \ \ Key `` (newK``{x}) Un (sees A evs)"; by (Fast_tac 1); @@ -328,23 +314,30 @@ (*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))"; + "!!evs. (Key K : analz (Key``nE Un sEe)) --> \ +\ (K : nE | Key K : analz sEe) ==> \ +\ (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)"; by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); val lemma = result(); +(*Copied from OtwayRees.ML*) +val enemy_analz_tac = + SELECT_GOAL + (EVERY [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) + ]); + goal thy "!!evs. evs : ns_shared ==> \ -\ 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 (shrK C)) \ -\ (sees Enemy evs)))"; +\ 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); -by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_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 @@ -352,18 +345,14 @@ @ pushes) setloop split_tac [expand_if]))); (** LEVEL 5 **) +(*NS3, Fake subcase*) +by (enemy_analz_tac 5); (*Cases NS2 and NS3!! Simple, thanks to auto case splits*) by (REPEAT (Fast_tac 3)); -(*Fake case*) (** LEVEL 6 **) +(*Fake case*) (** LEVEL 7 **) 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]); +by (enemy_analz_tac 2); (*Base case*) by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); qed_spec_mp "analz_image_newK"; @@ -371,61 +360,68 @@ goal thy "!!evs. evs : ns_shared ==> \ -\ Key K : analz (insert (Key (newK evt)) \ -\ (insert (Key (shrK C)) \ -\ (sees Enemy evs))) = \ -\ (K = newK evt | \ -\ Key K : analz (insert (Key (shrK C)) \ -\ (sees Enemy evs)))"; +\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \ +\ (K = newK evt | Key K : analz (sees Enemy evs))"; by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, insert_Key_singleton]) 1); by (Fast_tac 1); qed "analz_insert_Key_newK"; +(** First, two lemmas for the Fake and NS3 cases **) + +goal thy + "!!evs. [| X : synth (analz (sees Enemy evs)); \ +\ Crypt X' (shrK C) : parts{X}; \ +\ C ~= Enemy; C ~: Friend``leaked; 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] + addss (!simpset)) 1); +qed "Crypt_Fake_parts"; + +goal thy + "!!evs. [| Crypt X' K : parts (sees A evs); evs : ns_shared |] \ +\ ==> EX S S' Y. Says S S' Y : set_of_list evs & \ +\ Crypt X' K : parts {Y}"; +bd parts_singleton 1; +by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1); +qed "Crypt_parts_singleton"; + +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); (*This says that the Key, K, uniquely identifies the message. - But if C=Enemy then he could send all sorts of nonsense.*) + 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 S A Y N B X. \ -\ C ~= Enemy --> \ -\ Says S A Y : set_of_list evs --> \ -\ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> X=X')"; +\ EX X'. ALL C. \ +\ C ~= Enemy & C ~: Friend``leaked --> \ +\ (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'))"; be 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, imp_conj_distrib]))); +by (REPEAT_FIRST (eresolve_tac [exE,disjE])); +(*NS3: Fake (compromised) case*) +by (ex_strip_tac 4); +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, + Crypt_parts_singleton]) 4); +(*NS3: Good case, no relevant messages*) +by (fast_tac (!claset addSEs [exI] addss (!simpset)) 3); (*NS2: Case split propagates some context to other subgoal...*) by (excluded_middle_tac "K = newK evsa" 2); by (Asm_simp_tac 2); +be exI 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); -(*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 (Step_tac 1); -(** LEVEL 12 **) -by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \ -\ : parts (sees Enemy evsa)" 1); -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 (thin_tac "?aa : parts {X}" 1); -bd parts_singleton 1; -by (Step_tac 1); -bd seesD 1; -by (Step_tac 1); -by (Full_simp_tac 2); -by (fast_tac (!claset addSDs [spec]) 1); +(*Fake*) (** LEVEL 11 **) +by (ex_strip_tac 1); +by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1); val lemma = result(); @@ -433,31 +429,33 @@ goal thy "!!evs. [| Says S A \ \ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \ -\ : set_of_list evs; \ - \ Says S' A' \ +\ : set_of_list evs; \ +\ Says S' A' \ \ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ \ : set_of_list evs; \ -\ evs : ns_shared; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; +\ evs : ns_shared; C ~= Enemy; C ~: Friend``leaked; C' ~= Enemy; C' ~: Friend``leaked |] ==> X = X'"; bd lemma 1; be exE 1; +(*Duplicate the assumption*) by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); -by (Fast_tac 1); +(*Are these instantiations essential?*) +by (dres_inst_tac [("x","C")] spec 1); +by (dres_inst_tac [("x","C'")] spec 1); +by (fast_tac (!claset addSDs [spec]) 1); qed "unique_session_keys"; -(*Crucial secrecy property: Enemy does not see the keys sent in msg NS2 - -- even if another key is compromised*) +(*Crucial secrecy property: Enemy does not see the keys sent in msg NS2*) goal thy - "!!evs. [| Says Server (Friend i) \ + "!!evs. [| Says Server (Friend i) \ \ (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 (shrK C)) (sees Enemy evs))"; +\ i ~: leaked; j ~: leaked; evs : ns_shared \ +\ |] ==> \ +\ K ~: analz (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))); +by (ALLGOALS Asm_simp_tac); (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) by (REPEAT_FIRST (resolve_tac [conjI, impI])); by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); @@ -469,36 +467,28 @@ 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 (subgoal_tac - "Key (newK evt) : \ -\ 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), - impOfSubs synth_increasing, - impOfSubs analz_increasing]) 0 2); -(*Proves the Fake goal*) -by (fast_tac (!claset addss (!simpset)) 1); - -(**LEVEL 13**) +(*Fake case*) (** LEVEL 8 **) +by (enemy_analz_tac 1); (*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] ORELSE' hyp_subst_tac)); +by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac)); +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); -(**LEVEL 18 **) +(**************** by (Step_tac 1); ****************) +by (step_tac HOL_cs 1); +(**LEVEL 15 **) +by (excluded_middle_tac "ia : leaked" 1); +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 (Fast_tac 2); +(*So now we know that Friend ia is a good agent*) bd 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); +by (auto_tac (!claset, !simpset addsimps [shrK_mem_analz])); qed "Enemy_not_see_encrypted_key"; - - - diff -r d551e68b7a36 -r 789c12ea0b30 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Mon Sep 09 17:34:24 1996 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Mon Sep 09 17:44:20 1996 +0200 @@ -24,7 +24,7 @@ Fake "[| evs: ns_shared; B ~= Enemy; X: synth (analz (sees Enemy evs)) |] ==> Says Enemy B X # evs : ns_shared" - (*Alice initiates a protocol run*) + (*Alice initiates a protocol run, requesting to talk to any B*) NS1 "[| evs: ns_shared; A ~= Server |] ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs : ns_shared" diff -r d551e68b7a36 -r 789c12ea0b30 src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Mon Sep 09 17:34:24 1996 +0200 +++ b/src/HOL/Auth/Shared.thy Mon Sep 09 17:44:20 1996 +0200 @@ -14,6 +14,7 @@ consts shrK :: agent => key (*symmetric keys*) + leaked :: nat set (*Friendly agents whose keys have leaked to Enemy*) rules isSym_shrK "isSymKey (shrK A)" @@ -25,7 +26,8 @@ (*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_Enemy + "initState Enemy = insert (Key (shrK Enemy)) (Key``shrK``Friend``leaked)" datatype (*Messages, and components of agent stores*) event = Says agent agent msg