# HG changeset patch # User paulson # Date 838376386 -7200 # Node ID a18a6dc14f768b2b14bc78d82613af2df4b6009f # Parent 5a1f81da3e12a02409667a6312eb80a16bef8fb9 Auth proofs work up to the XXX... diff -r 5a1f81da3e12 -r a18a6dc14f76 src/HOL/Auth/Event.ML --- a/src/HOL/Auth/Event.ML Fri Jul 26 12:18:50 1996 +0200 +++ b/src/HOL/Auth/Event.ML Fri Jul 26 12:19:46 1996 +0200 @@ -10,11 +10,53 @@ *) +proof_timing:=true; + +Delrules [less_SucE]; (*Perhaps avoid inserting this in Arith.ML????*) + +(*FOR LIST.ML??*) +goal List.thy "x : setOfList (x#xs)"; +by (Simp_tac 1); +qed "setOfList_I1"; + +goal List.thy "!!x. xs = x#xs' ==> x : setOfList xs"; +by (Asm_simp_tac 1); +qed "setOfList_eqI1"; + +(*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*) +goalw Set.thy [Bex_def] "(? x:A. False) = False"; +by (Simp_tac 1); +qed "bex_False"; +Addsimps [bex_False]; +goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A"; +by (Fast_tac 1); +qed "insert_image"; +Addsimps [insert_image]; + + +(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE!!*) +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(); + + open Event; -(*Rewrite using {a} Un A = insert a A *) -Addsimps [insert_is_Un RS sym]; +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 + this means that some terms displayed as (f o g) will be rewritten, and others + will not!*) +Addsimps [o_def]; (*** Basic properties of serverKey and newK ***) @@ -46,19 +88,23 @@ Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym]; (*Good for talking about Server's initial state*) -goal thy "parts (range (Key o f)) = range (Key o f)"; -by (auto_tac (!claset addIs [range_eqI], !simpset)); +goal thy "!!H. H <= Key``E ==> parts H = H"; +by (Auto_tac ()); be parts.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "parts_range_Key"; +qed "parts_image_subset"; -goal thy "analyze (range (Key o f)) = range (Key o f)"; -by (auto_tac (!claset addIs [range_eqI], !simpset)); +bind_thm ("parts_image_Key", subset_refl RS parts_image_subset); + +goal thy "!!H. H <= Key``E ==> analyze H = H"; +by (Auto_tac ()); be analyze.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_range_Key"; +qed "analyze_image_subset"; -Addsimps [parts_range_Key, analyze_range_Key]; +bind_thm ("analyze_image_Key", subset_refl RS analyze_image_subset); + +Addsimps [parts_image_Key, analyze_image_Key]; goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; by (agent.induct_tac "C" 1); @@ -66,6 +112,32 @@ qed "keysFor_parts_initState"; Addsimps [keysFor_parts_initState]; +goalw thy [keysFor_def] "keysFor (Key``E) = {}"; +by (Auto_tac ()); +qed "keysFor_image_Key"; +Addsimps [keysFor_image_Key]; + +goal thy "serverKey A ~: newK``E"; +by (agent.induct_tac "A" 1); +by (Auto_tac ()); +qed "serverKey_notin_image_newK"; +Addsimps [serverKey_notin_image_newK]; + + +(*Agents see their own serverKeys!*) +goal thy "Key (serverKey A) : analyze (sees A evs)"; +by (list.induct_tac "evs" 1); +by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analyze_mono)]) 2); +by (agent.induct_tac "A" 1); +by (auto_tac (!claset addIs [range_eqI], !simpset)); +qed "analyze_own_serverKey"; + +bind_thm ("parts_own_serverKey", + [analyze_subset_parts, analyze_own_serverKey] MRS subsetD); + +Addsimps [analyze_own_serverKey, parts_own_serverKey]; + + (**** Inductive relation "traces" -- basic properties ****) @@ -83,6 +155,11 @@ by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); qed "traces_ConsE"; +goal thy "!!ev evs. [| evs = ev#evs'; evs : traces |] ==> evs' : traces"; +by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); +qed "traces_eq_ConsE"; + + (** Specialized rewrite rules for (sees A (Says...#evs)) **) goal thy "sees A (Says A B X # evs) = insert X (sees A evs)"; @@ -123,6 +200,13 @@ by (ALLGOALS (fast_tac (!claset addss ss))); qed "UN_parts_sees_Says"; +goal thy "Says A B X : setOfList evs --> X : sees Enemy evs"; +by (list.induct_tac "evs" 1); +by (Auto_tac ()); +qed_spec_mp "Says_imp_sees_Enemy"; + +Addsimps [Says_imp_sees_Enemy]; +AddIs [Says_imp_sees_Enemy]; Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy]; Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) @@ -142,6 +226,7 @@ qed "sees_agent_subset_sees_Enemy"; +(*Nobody sends themselves messages*) goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs"; be traces.induct 1; by (Auto_tac()); @@ -168,11 +253,15 @@ bind_thm ("Enemy_not_analyze_serverKey", [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); -Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey]; +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)]; (*No Friend will ever see another agent's server key - (excluding the Enemy, who might transmit his).*) + (excluding the Enemy, who might transmit his). + The Server, of course, knows all server keys.*) goal thy "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ \ Key (serverKey A) ~: parts (sees (Friend j) evs)"; @@ -181,6 +270,20 @@ qed "Friend_not_see_serverKey"; +(*Not for Addsimps -- it can cause goals to blow up!*) +goal thy + "!!evs. evs : traces ==> \ +\ (Key (serverKey A) \ +\ : analyze (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)] + addss (!simpset)) 1); +qed "serverKey_mem_analyze"; + + + + (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. @@ -218,6 +321,8 @@ by (fast_tac (!claset addDs [lemma]) 1); qed "new_keys_not_seen"; +Addsimps [new_keys_not_seen]; + goal thy "!!K. newK evs = invKey K ==> newK evs = K"; br (invKey_eq RS iffD1) 1; by (Simp_tac 1); @@ -265,60 +370,897 @@ \ newK evs' ~: keysFor (parts (sees C evs))"; by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); qed "new_keys_not_used"; -Addsimps [new_keys_not_used]; bind_thm ("new_keys_not_analyzed", [analyze_subset_parts RS keysFor_mono, new_keys_not_used] MRS contra_subsetD); - -(*Maybe too specific to be of much use...*) -goal thy - "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \ -\ (serverKey A)) \ -\ : setOfList evs; \ -\ evs : traces \ -\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))"; -be rev_mp 1; -be traces.induct 1; -be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) -be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*) -by (ALLGOALS Asm_full_simp_tac); -by (Fast_tac 1); (*Proves the NS2 case*) -qed "Says_Server_imp_X_eq_Crypt"; +Addsimps [new_keys_not_used, new_keys_not_analyzed]; -(*Pushes Crypt events in so that others might be pulled out*) -goal thy "insert (Crypt X K) (insert y evs) = \ -\ insert y (insert (Crypt X K) evs)"; -by (Fast_tac 1); -qed "insert_Crypt_delay"; +(** Rewrites to push in Key and Crypt messages, so that other messages can + be pulled out using the analyze_insert rules **) + +fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] + insert_commute; -goal thy "insert (Key K) (insert y evs) = \ -\ insert y (insert (Key K) evs)"; -by (Fast_tac 1); -qed "insert_Key_delay"; +val pushKeys = map (insComm "Key ?K") + ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"]; + +val pushCrypts = map (insComm "Crypt ?X ?K") + ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; + +(*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)"; (** Lemmas concerning the form of items passed in messages **) -(*Describes the form *and age* of K when the following message is sent*) +(*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 : traces \ -\ |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)"; + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \ +\ evs : traces \ +\ |] ==> (EX evs':traces. K = Key(newK evs') & length evs' < length evs & \ +\ X = (Crypt {|K, Agent A|} (serverKey B)))"; be rev_mp 1; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); -qed "Says_Server_imp_Key_newK"; +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); + +(*USELESS for NS3, case 1, as the ind hyp says the same thing! +goal thy + "!!evs. [| evs = Says Server (Friend i) \ +\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ +\ evs : traces; i~=k \ +\ |] ==> \ +\ K ~: analyze (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); +val Enemy_not_see_encrypted_key_lemma = result(); +*) + + +(*Describes the form of X when the following message is sent*) +goal thy + "!!evs. evs : traces ==> \ +\ ALL A NA B K X. \ +\ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ +\ : parts (sees Enemy evs) & A ~= Enemy --> \ +\ (EX evt:traces. K = newK evt & \ +\ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (Step_tac 1); +by (ALLGOALS Asm_full_simp_tac); +(*Remaining cases are Fake, NS2 and NS3*) +by (fast_tac (!claset addSDs [spec]) 2); +(*The NS3 case needs the induction hypothesis twice! + One application is to the X component of the most recent message.*) +by (full_simp_tac (!simpset addsimps [conj_disj_distribR, all_conj_distrib]) 2); +be conjE 2; +by (subgoal_tac "? evs':traces. K = newK evs' & \ +\ X = Crypt {|Key K, Agent (Friend i)|} (serverKey B)" 2); +(*DELETE the second quantified formula for speed*) +by (eres_inst_tac [("V","ALL A NA B K Xa. ?f A NA B K Xa : ?H X & ?P(A) --> \ +\ ?Q K Xa A B")] thin_rl 3); +by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 3); +(*DELETE the first quantified formula: it's now useless*) +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); +by (fast_tac (!claset addss (!simpset)) 2); +(*Now for the Fake case*) +by (subgoal_tac + "Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \ +\ parts (synthesize (analyze (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] + addss (!simpset)) 1); +val encrypted_form = result(); + + +(*For eliminating the A ~= Enemy condition from the previous result*) +goal thy + "!!evs. evs : traces ==> \ +\ ALL S A NA B K X. \ +\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ +\ : setOfList evs --> \ +\ S = Server | S = Enemy"; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (ALLGOALS Asm_full_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 (setOfList_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); +bd (normalize_thm [RSspec,RSmp] encrypted_form) 1; +br (parts.Inj RS conjI) 1; +auto(); +qed_spec_mp "Server_or_Enemy"; + + + +(*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)) \ +\ : setOfList evs; \ +\ evs : traces \ +\ |] ==> (EX evt:traces. K = newK evt & \ +\ X = (Crypt {|Key K, Agent A|} (serverKey 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); +by (forward_tac [normalize_thm [RSspec,RSmp] encrypted_form] 1); +br (parts.Inj RS conjI) 1; +by (Auto_tac()); +qed "Says_S_message_form"; + +goal thy + "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} \ +\ (serverKey A)) # evs'; \ +\ evs : traces \ +\ |] ==> (EX evt:traces. evs' : traces & \ +\ 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 (Auto_tac()); +qed "Says_S_message_form_eq"; + + + + +(**** + The following is to prove theorems of the form + + Key K : analyze (insert (Key (newK evt)) + (insert (Key (serverKey C)) (sees Enemy evs))) ==> + Key K : analyze (insert (Key (serverKey C)) (sees Enemy evs)) + + A more general formula must be proved inductively. + +****) + + +(*Not useful in this form, but it says that session keys are not used + to encrypt messages containing other keys, in the actual protocol. + We require that agents should behave like this subsequently also.*) +goal thy + "!!evs. evs : traces ==> \ +\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ +\ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (hyp_subst_tac 5); (*NS3: apply evsa = Says S A (Crypt ...) # ... *) +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); +(*Case NS3*) +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, + impOfSubs parts_insert_subset_Un] + addss (!simpset)) 1); +result(); + + +(** Specialized rewrites for this proof **) + +Delsimps [image_insert]; +Addsimps [image_insert RS sym]; + +goal thy "insert (Key (newK x)) (sees A evs) = \ +\ Key `` (newK``{x}) Un (sees A evs)"; +by (Fast_tac 1); +val insert_Key_singleton = result(); + +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ +\ Key `` (f `` (insert x E)) Un C"; +by (Fast_tac 1); +val insert_Key_image = result(); + + +goal thy + "!!evs. evs : traces ==> \ +\ ALL K E. (Key K : analyze (insert (Key (serverKey C)) \ +\ (Key``(newK``E) Un (sees Enemy evs)))) = \ +\ (K : newK``E | \ +\ Key K : analyze (insert (Key (serverKey C)) \ +\ (sees Enemy evs)))"; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (dtac Says_S_message_form_eq 5 THEN assume_tac 5); +by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); +by (ALLGOALS + (asm_full_simp_tac + (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] + @ pushes) + setloop split_tac [expand_if]))); +(*Cases NS2 and NS3!! Simple, thanks to auto case splits*) +by (REPEAT (Fast_tac 3)); +(*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 (analyze_mono)]) 2); +by (subgoal_tac + "Key K : analyze \ +\ (synthesize \ +\ (analyze (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 (Asm_full_simp_tac 1); +by (deepen_tac (!claset addIs [impOfSubs analyze_mono]) 0 1); +qed_spec_mp "analyze_image_newK"; + + +goal thy + "!!evs. evs : traces ==> \ +\ Key K : analyze (insert (Key (newK evt)) \ +\ (insert (Key (serverKey C)) \ +\ (sees Enemy evs))) = \ +\ (K = newK evt | \ +\ Key K : analyze (insert (Key (serverKey C)) \ +\ (sees Enemy evs)))"; +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analyze_image_newK, + insert_Key_singleton]) 1); +by (Fast_tac 1); +qed "analyze_insert_Key_newK"; + + + + +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; + + +goal thy + "!!evs. [| evs = Says Server (Friend i) \ +\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ +\ evs : traces; i~=k \ +\ |] ==> \ +\ K = newK evs'"; ???????????????? + + +goals_limit:=2; +goal thy + "!!evs. [| Says S A \ +\ (Crypt {|N, Agent B, Key K, X|} (serverKey A)) : setOfList evs; \ +\ evs : traces \ +\ |] ==> \ +\ ALL A' N' B' X'. \ +\ Says Server A' \ +\ (Crypt {|N', Agent B', Key K, X'|} (serverKey A')) : \ +\ setOfList evs --> X = X'"; +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 (REPEAT_FIRST (resolve_tac [conjI, impI, allI] ORELSE' etac conjE + ORELSE' hyp_subst_tac)); + +by (ALLGOALS (full_simp_tac (!simpset addsimps [not_Cons_self]))); +by (Step_tac 1); +fe Crypt_synthesize; +by (fast_tac (!claset addss (!simpset)) 2); + + + +by (Step_tac 1); +by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1); +val Enemy_not_see_encrypted_key_lemma = result(); + + + + +AddSEs [less_irrefl]; + +(*Crucial security property: Enemy does not see the keys sent in msg NS2 + -- even if another key is compromised*) +goal thy + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent(Friend j), K, X|} K') : setOfList evs; \ +\ evs : traces; Friend i ~= C; Friend j ~= C \ +\ |] ==> \ +\ K ~: analyze (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!*) +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); +(*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)); +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) + setloop split_tac [expand_if]))); + +(*NS2*) +by (Fast_tac 2); +(** LEVEL 9 **) +(*Now for the Fake case*) +br notI 1; +by (subgoal_tac + "Key (newK evs') : \ +\ analyze (synthesize (analyze (insert (Key (serverKey C)) \ +\ (sees Enemy evsa))))" 1); +be (impOfSubs analyze_mono) 2; +by (deepen_tac (!claset addIs [analyze_mono RS synthesize_mono RSN + (2,rev_subsetD), + impOfSubs synthesize_increasing, + impOfSubs analyze_increasing]) 0 2); +(*Proves the Fake goal*) +by (fast_tac (!claset addss (!simpset)) 1); + +(**LEVEL 16**) +(*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 (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); + +(**LEVEL 20, one subgoal left! **) +(*NS3, case 2: that message from the Server was sent earlier*) + +(*simplify the good implication*) +by (Asm_full_simp_tac 1); +by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*delete the bad implication*) +by ((forward_tac [Says_Server_message_form] THEN' assume_tac) 1); +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); +by (Full_simp_tac 1); + +(**LEVEL 25 **) + +by ((forward_tac [setOfList_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 (analyze_insert_Key_newK::pushes)) 1); +by (step_tac (!claset delrules [impCE]) 1); +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); + + +by (Step_tac 1); +by (Fast_tac 1); + +(*May do this once we have proved that the keys coincide*) +by (subgoal_tac "i = ia & N = Nonce NA & Friend j = C & K' = serverKey (Friend ia)" 1); +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); + +(**LEVEL 29 **) + +by (asm_full_simp_tac (!simpset addsimps (pushes)) 1); + + +(*ALL THAT REMAINS IS TO PROVE THE SUBGOAL!*) + + + + + +by (Step_tac 1); +by (Fast_tac 1); + + + + +by (forward_tac [setOfList_I1 RSN (2, Server_or_Enemy)] 1); + + + (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); + + +by (excluded_middle_tac "evs'a=evt" 1); +(*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) +by (subgoal_tac "B = Friend j" 2); +by (REPEAT_FIRST hyp_subst_tac); +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); +(*Keys differ? Then they cannot clash*) + +br notI 1; +bd (impOfSubs analyze_insert_Crypt_subset) 1; + + +????????????????????????????????????????????????????????????????; + +(**LEVEL 35 **) + +(*In this case, the Key in X (newK evs') is younger than + the Key we are worried about (newK evs'a). And nobody has used the + new Key yet, so it can be pulled out of the "analyze".*) +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); +by (Fast_tac 1); +(*In this case, Enemy has seen the (encrypted!) message at hand...*) +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); +by (asm_full_simp_tac (!simpset addsimps ([insert_absorb]@pushes)) 1); + +(**LEVEL 39 **) + +br notI 1; +bd (impOfSubs analyze_insert_Crypt_subset) 1; +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); + + +by (excluded_middle_tac "evs'a=evt" 1); +(*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) +by (subgoal_tac "B = Friend j" 2); +by (REPEAT_FIRST hyp_subst_tac); +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); +(*Keys differ? Then they cannot clash*) + +br notI 1; +bd (impOfSubs analyze_insert_Crypt_subset) 1; + + + + + + + +(**LEVEL 28 OLD VERSION, with extra case split on ia=k **) + +by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1); +by (excluded_middle_tac "ia=k" 1); +(*Case where the key is compromised*) +by (hyp_subst_tac 2); +by (asm_full_simp_tac (!simpset addsimps pushes) 2); +by (full_simp_tac (!simpset addsimps [insert_commute]) 2); + +(**LEVEL 33 **) + +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; +proof_timing:=true; +AddSEs [less_irrefl]; + + +(*Case where the key is secure*) +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); + +(*pretend we have the right lemma!*) +(*EITHER the message was just sent by the Server, OR is a replay from the Enemy + -- in either case it has the right form, only the age differs +*) +by (subgoal_tac "EX evt. K = newK evt & X = (Crypt {|Key K, Agent(Friend ia)|} (serverKey B)) & (evt = evs' | (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) : sees Enemy evs')" 1); +by (REPEAT_FIRST (eresolve_tac [exE, disjE, conjE] ORELSE' hyp_subst_tac)); +by (asm_full_simp_tac (!simpset addsimps pushes) 1); +by (res_inst_tac [("x1","Crypt ?U (?K ia)")] (insert_commute RS ssubst) 1); +br notI 1; + +bd (impOfSubs analyze_insert_Crypt_subset) 1; + +(**LEVEL 40 **) + +(*In this case, the Key in X (newK evs') is younger than + the Key we are worried about (newK evs'a). And nobody has used the + new Key yet, so it can be pulled out of the "analyze".*) +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); +by (Fast_tac 1); +(*In this case, Enemy already knows about the message at hand...*) +by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1); +by (asm_full_simp_tac (!simpset addsimps ([insert_absorb]@pushes)) 1); + +(**LEVEL 44 **) + +by (excluded_middle_tac "evs'a=evt" 1); +(*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) +by (subgoal_tac "B = Friend j" 2); +by (REPEAT_FIRST hyp_subst_tac); +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); +(*Keys differ? Then they cannot clash*) + +br notI 1; +bd (impOfSubs analyze_insert_Crypt_subset) 1; + +by (asm_full_simp_tac + (!simpset addsimps (pushes@[analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); +by (Fast_tac 1); + + + +by (excluded_middle_tac "evs'a=evt" 1); +(*Keys agree? Then should have B = Friend j, so encrypted msg is secure*) +by (subgoal_tac "B = Friend j & ia=i" 2); +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); +by (asm_full_simp_tac + (!simpset addsimps ([analyze_subset_parts RS contra_subsetD])) 2); +(*Keys differ? Then they cannot clash*) + +br notI 1; +bd (impOfSubs analyze_insert_Crypt_subset) 1; + +by (asm_full_simp_tac + (!simpset addsimps (pushes@[analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); +by (Fast_tac 1); + + +Level 51 +!!evs. [| Says Server (Friend i) (Crypt {|N, Agent (Friend j), K, X|} K') : + setOfList evs; + evs : traces; i ~= k; j ~= k |] ==> + K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs)) + 1. !!evs A B K NA S X evsa evs' ia evs'a evt. + [| i ~= k; j ~= k; + Says S (Friend ia) + (Crypt + {|Nonce NA, Agent B, Key (newK evt), + Crypt {|Key (newK evt), Agent (Friend ia)|} (serverKey B)|} + (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'; + evs' : traces; length evs'a < length evs'; ia ~= k; + Crypt + {|Nonce NA, Agent B, Key (newK evt), + Crypt {|Key (newK evt), Agent (Friend ia)|} (serverKey B)|} + (serverKey (Friend ia)) : + sees Enemy evs'; + Key (newK evs'a) ~: + analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')); + evs'a ~= evt; + Key (newK evs'a) : + analyze + (insert (Key (newK evt)) + (insert (Key (serverKey (Friend k))) (sees Enemy evs'))) |] ==> + False + + + + +YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; + + +push_proof(); +goal thy + "!!evs. [| evs = Says S (Friend i) \ +\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ +\ evs : traces; i~=k \ +\ |] ==> \ +\ K ~: analyze (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); +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); + +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"; + + +goal thy + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ evs : traces; i~=j \ +\ |] ==> K ~: analyze (sees (Friend j) evs)"; +br (sees_agent_subset_sees_Enemy RS analyze_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; \ +\ A ~: {Friend i, Server}; \ +\ evs : traces \ +\ |] ==> K ~: analyze (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; +(* hyp_subst_tac would deletes the equality assumption... *) +by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac)); +qed "Agent_not_see_encrypted_key"; + + +(*Neatly packaged, perhaps in a useless form*) +goalw thy [knownBy_def] + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ evs : traces \ +\ |] ==> knownBy evs K <= {Friend i, Server}"; + +by (Step_tac 1); +br ccontr 1; +by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); +qed "knownBy_encrypted_key"; + + + + XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; ZZZZZZZZZZZZZZZZ; @@ -520,101 +1462,6 @@ WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW; -Addsimps [new_keys_not_seen]; - -(*Crucial security property: Enemy does not see the keys sent in msg NS2 - -- even if another friend's key is compromised*) -goal thy - "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \ -\ evs : traces; i~=j |] ==> \ -\ \ -\ K ~: analyze (insert (Key (serverKey (Friend j))) (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); -(*The two simplifications cannot be combined -- they loop!*) -by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay]))); -(*Next 3 steps infer that K has the form "Key (newK evs'" ... *) -br conjI 3; -by (REPEAT_FIRST (resolve_tac [impI])); -by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac)); -(*NS1, subgoal concerns "(Says A Server - {|Agent A, Agent B, Nonce (newN evsa)|}"*) -(*... thus it cannot equal any components of A's message above.*) -by (fast_tac (!claset addss (!simpset)) 2); -(*NS2, the subcase where that message was the most recently sent; - it holds because here K' = serverKey(Friend i), which Enemies can't see, - AND because nobody can know about a brand new key*) -by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2); -(*NS2, other subcase. K is an old key, and thus not in the latest message.*) -by (fast_tac - (!claset addSEs [less_irrefl] - addDs [impOfSubs analyze_insert_Crypt_subset] - addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2); -(*Now for the Fake case*) -be exE 1; -br notI 1; -by (REPEAT (etac conjE 1)); -by (REPEAT (hyp_subst_tac 1)); -by (subgoal_tac - "Key (newK evs') : \ -\ analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \ -\ (sees Enemy evsa))))" 1); -be (impOfSubs analyze_mono) 2; -by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN - (2,rev_subsetD), - impOfSubs synthesize_increasing, - impOfSubs analyze_increasing]) 2); -(*Proves the Fake goal*) -by (Auto_tac()); -qed "Enemy_not_see_encrypted_key"; - - -goal thy - "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ -\ evs : traces; i~=j \ -\ |] ==> K ~: analyze (sees (Friend j) evs)"; -br (sees_agent_subset_sees_Enemy RS analyze_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; \ -\ A ~: {Friend i, Server}; \ -\ evs : traces \ -\ |] ==> K ~: analyze (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; -(* hyp_subst_tac would deletes the equality assumption... *) -by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac)); -qed "Agent_not_see_encrypted_key"; - - -(*Neatly packaged, perhaps in a useless form*) -goalw thy [knownBy_def] - "!!evs. [| Says Server (Friend i) \ -\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ -\ evs : traces \ -\ |] ==> knownBy evs K <= {Friend i, Server}"; - -by (Step_tac 1); -br ccontr 1; -by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); -qed "knownBy_encrypted_key"; - - - - -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; - @@ -651,10 +1498,6 @@ -goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \ -\ insert {|X,Y|} (insert (Crypt x) evs)"; -by (Fast_tac 1); -qed "insert_Crypt_MPair_delay"; diff -r 5a1f81da3e12 -r a18a6dc14f76 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Fri Jul 26 12:18:50 1996 +0200 +++ b/src/HOL/Auth/Event.thy Fri Jul 26 12:19:46 1996 +0200 @@ -26,7 +26,7 @@ primrec initState agent (*Server knows all keys; other agents know only their own*) - initState_Server "initState Server = range (Key o serverKey)" + initState_Server "initState Server = Key `` range serverKey" initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}" initState_Enemy "initState Enemy = {Key (serverKey Enemy)}" @@ -111,7 +111,7 @@ (serverKey A))) # evs : traces" (*We can't assume S=Server. Agent A "remembers" her nonce. - May assume WLOG that she is NOT the Enemy, as the Fake rule. + May assume WLOG that she is NOT the Enemy: the Fake rule covers this case. Can inductively show A ~= Server*) NS3 "[| evs: traces; A ~= B; evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} diff -r 5a1f81da3e12 -r a18a6dc14f76 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Fri Jul 26 12:18:50 1996 +0200 +++ b/src/HOL/Auth/Message.ML Fri Jul 26 12:19:46 1996 +0200 @@ -268,6 +268,8 @@ AddSEs [MPair_analyze]; AddDs [analyze.Decrypt]; +Addsimps [analyze.Inj]; + goal thy "H <= analyze(H)"; by (Fast_tac 1); qed "analyze_increasing"; @@ -289,6 +291,13 @@ qed "parts_analyze"; Addsimps [parts_analyze]; +goal thy "analyze (parts H) = parts H"; +by (Auto_tac()); +be analyze.induct 1; +by (Auto_tac()); +qed "analyze_parts"; +Addsimps [analyze_parts]; + (*Monotonicity; Lemma 1 of Lowe*) goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)"; by (rtac lfp_mono 1); @@ -342,6 +351,17 @@ by (ALLGOALS (fast_tac (!claset addss (!simpset)))); qed "analyze_insert_Key"; +goal thy "analyze (insert {|X,Y|} H) = \ +\ insert {|X,Y|} (analyze (insert X (insert Y H)))"; +br equalityI 1; +br subsetI 1; +be analyze.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"; + +(*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)"; @@ -375,70 +395,31 @@ by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); qed "analyze_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"; + Addsimps [analyze_insert_Agent, analyze_insert_Nonce, - analyze_insert_Key, analyze_insert_Crypt, - analyze_insert_Decrypt]; - + analyze_insert_Key, analyze_insert_MPair, + analyze_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))"; +\ insert (Crypt X K) (analyze (insert X H))"; br subsetI 1; be analyze.induct 1; by (Auto_tac()); qed "analyze_insert_Crypt_subset"; -(** Rewrite rules for pulling out atomic parts of messages **) - -goal thy "analyze (insert X H) <= analyze (insert {|X,Y|} H)"; -br subsetI 1; -be analyze.induct 1; -by (ALLGOALS (best_tac (!claset addIs [analyze.Fst]))); -qed "analyze_insert_subset_MPair1"; - -goal thy "analyze (insert Y H) <= analyze (insert {|X,Y|} H)"; -br subsetI 1; -be analyze.induct 1; -by (ALLGOALS (best_tac (!claset addIs [analyze.Snd]))); -qed "analyze_insert_subset_MPair2"; - -goal thy "analyze (insert {|Agent agt,Y|} H) = \ -\ insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))"; -by (rtac equalityI 1); -by (best_tac (!claset addIs [analyze.Fst, - impOfSubs analyze_insert_subset_MPair2]) 2); -br subsetI 1; -be analyze.induct 1; -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Agent_MPair"; - -goal thy "analyze (insert {|Nonce N,Y|} H) = \ -\ insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))"; -by (rtac equalityI 1); -by (best_tac (!claset addIs [analyze.Fst, - impOfSubs analyze_insert_subset_MPair2]) 2); -br subsetI 1; -be analyze.induct 1; -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Nonce_MPair"; - -(*Can only pull out Keys if they are not needed to decrypt the rest*) -goalw thy [keysFor_def] - "!!K. K ~: keysFor (analyze (insert Y H)) ==> \ -\ analyze (insert {|Key K, Y|} H) = \ -\ insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))"; -by (rtac equalityI 1); -by (best_tac (!claset addIs [analyze.Fst, - impOfSubs analyze_insert_subset_MPair2]) 2); -br subsetI 1; -be analyze.induct 1; -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "analyze_insert_Key_MPair"; - -Addsimps [analyze_insert_Agent_MPair, analyze_insert_Nonce_MPair, - analyze_insert_Key_MPair]; - (** Idempotence and transitivity **) goal thy "!!H. X: analyze (analyze H) ==> X: analyze H"; @@ -467,6 +448,29 @@ "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H" *) + +(** A congruence rule for "analyze" **) + +goal thy "!!H. [| analyze G <= analyze G'; analyze H <= analyze H' \ +\ |] ==> analyze (G Un H) <= analyze (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"; + +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] + ORELSE' etac equalityE)); +qed "analyze_cong"; + + +goal thy "!!H. analyze H = analyze H' ==> \ +\ analyze (insert X H) = analyze (insert X H')"; +by (asm_simp_tac (!simpset addsimps [insert_def] + setloop (rtac analyze_cong)) 1); +qed "analyze_insert_cong"; + (*If there are no pairs or encryptions then analyze does nothing*) goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt X K ~: H |] ==> \ \ analyze H = H"; @@ -510,6 +514,10 @@ by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1)); qed "synthesize_Un"; +goal thy "insert X (synthesize H) <= synthesize(insert X H)"; +by (fast_tac (!claset addEs [impOfSubs synthesize_mono]) 1); +qed "synthesize_insert"; + (** Idempotence and transitivity **) goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H"; @@ -539,6 +547,7 @@ but can synthesize a pair or encryption from its components...*) val mk_cases = synthesize.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"; @@ -566,14 +575,6 @@ (*** Combinations of parts, analyze and synthesize ***) -(*Not that useful, in view of the following one...*) -goal thy "parts (synthesize H) <= synthesize (parts H)"; -by (Step_tac 1); -be parts.induct 1; -be (parts_increasing RS synthesize_mono RS subsetD) 1; -by (ALLGOALS Fast_tac); -qed "parts_synthesize_subset"; - goal thy "parts (synthesize H) = parts H Un synthesize H"; br equalityI 1; br subsetI 1;