# HG changeset patch # User paulson # Date 838657899 -7200 # Node ID fa58f4a06f21bea50528e745cbc2460da27dd118 # Parent 23765bc3e8e27980a8243e35be4f28f172add54b Works up to main theorem, then XXX...X diff -r 23765bc3e8e2 -r fa58f4a06f21 src/HOL/Auth/Event.ML --- a/src/HOL/Auth/Event.ML Mon Jul 29 18:30:01 1996 +0200 +++ b/src/HOL/Auth/Event.ML Mon Jul 29 18:31:39 1996 +0200 @@ -23,20 +23,18 @@ by (Asm_simp_tac 1); qed "setOfList_eqI1"; +goal List.thy "setOfList l <= setOfList (x#l)"; +by (Simp_tac 1); +by (Fast_tac 1); +qed "setOfList_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*) -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]; +prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; (*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE!!*) @@ -149,7 +147,6 @@ val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces"; val Notes_tracesE = mk_cases "Notes A X # evs: traces"; - (*The tail of a trace is a trace*) goal thy "!!ev evs. ev#evs : traces ==> evs : traces"; by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); @@ -208,6 +205,26 @@ Addsimps [Says_imp_sees_Enemy]; AddIs [Says_imp_sees_Enemy]; +goal thy "initState C <= Key `` range serverKey"; +by (agent.induct_tac "C" 1); +by (Auto_tac ()); +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. X = Key (serverKey A))"; +by (list.induct_tac "evs" 1); +by (ALLGOALS Asm_simp_tac); +by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); +br conjI 1; +by (Fast_tac 2); +by (event.induct_tac "a" 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); +by (ALLGOALS Fast_tac); +qed_spec_mp "seesD"; + + Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy]; Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) @@ -234,6 +251,13 @@ Addsimps [not_Says_to_self]; AddSEs [not_Says_to_self RSN (2, rev_notE)]; +goal thy "!!evs. evs : traces ==> Notes A X ~: setOfList evs"; +be traces.induct 1; +by (Auto_tac()); +qed "not_Notes"; +Addsimps [not_Notes]; +AddSEs [not_Notes RSN (2, rev_notE)]; + (*** Server keys are not betrayed ***) @@ -258,6 +282,24 @@ Enemy_not_analyze_serverKey, not_sym RSN (2, Enemy_not_analyze_serverKey)]; +(*We go to some trouble to preserve R in the 3rd subgoal*) +val major::prems = +goal thy "[| Key (serverKey A) : parts (sees Enemy evs); \ +\ evs : traces; \ +\ A=Enemy ==> R \ +\ |] ==> R"; +br ccontr 1; +br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1; +by (swap_res_tac prems 2); +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); + +(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) +AddSEs [Enemy_see_serverKey_E, Enemy_analyze_serverKey_E]; + (*No Friend will ever see another agent's server key (excluding the Enemy, who might transmit his). @@ -297,8 +339,7 @@ \ Key (newK evs') ~: (UN C. parts (sees C evs))"; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) -by (ALLGOALS (asm_full_simp_tac - (!simpset addsimps [de_Morgan_disj,Suc_le_eq]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Suc_le_eq]))); (*Initial state? New keys cannot clash*) by (Fast_tac 1); (*Rule NS1 in protocol*) @@ -320,8 +361,19 @@ \ Key (newK evs') ~: parts (sees C evs)"; by (fast_tac (!claset addDs [lemma]) 1); qed "new_keys_not_seen"; +Addsimps [new_keys_not_seen]; -Addsimps [new_keys_not_seen]; +(*Another variant: old messages must contain old keys!*) +goal thy + "!!evs. [| Says A B X : setOfList evs; \ +\ Key (newK evt) : parts {X}; \ +\ evs : traces \ +\ |] ==> length evt < length evs"; +br ccontr 1; +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy] + addIs [impOfSubs parts_mono, leI]) 1); +qed "Says_imp_old_keys"; + goal thy "!!K. newK evs = invKey K ==> newK evs = K"; br (invKey_eq RS iffD1) 1; @@ -338,8 +390,7 @@ \ newK evs' ~: keysFor (UN C. parts (sees C evs))"; be traces.induct 1; be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) -by (ALLGOALS (asm_full_simp_tac - (!simpset addsimps [de_Morgan_disj,Suc_le_eq]))); +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [Suc_le_eq]))); (*Rule NS1 in protocol*) by (fast_tac (!claset addDs [less_imp_le]) 2); (*Rule NS2 in protocol*) @@ -403,11 +454,14 @@ goal thy "!!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)))"; +\ |] ==> (EX evt:traces. \ +\ K = Key(newK evt) & \ +\ X = (Crypt {|K, Agent A|} (serverKey B)) & \ +\ K' = serverKey A & \ +\ length evt < length evs)"; be rev_mp 1; be traces.induct 1; -be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +be subst 4; (*NS2: discard evsa = Says A Server...#evs' as irrelevant!*) by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); qed "Says_Server_message_form"; @@ -450,7 +504,8 @@ 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); +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); @@ -480,7 +535,7 @@ \ 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); +by (ALLGOALS Asm_simp_tac); (*We are left with NS3*) by (subgoal_tac "S = Server | S = Enemy" 1); (*First justify this assumption!*) @@ -496,14 +551,13 @@ 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 & \ +\ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; by (forward_tac [Server_or_Enemy] 1); ba 1; @@ -511,14 +565,14 @@ 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()); +by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); 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 & \ +\ |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \ \ K = newK evt & \ \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; by (forward_tac [traces_eq_ConsE] 1); @@ -551,7 +605,7 @@ 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))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); (*Case NS3*) by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2); by (Asm_full_simp_tac 2); @@ -562,7 +616,7 @@ result(); -(** Specialized rewrites for this proof **) +(** Specialized rewriting for this proof **) Delsimps [image_insert]; Addsimps [image_insert RS sym]; @@ -578,6 +632,8 @@ val insert_Key_image = result(); +(** Session keys are not used to encrypt other session keys **) + goal thy "!!evs. evs : traces ==> \ \ ALL K E. (Key K : analyze (insert (Key (serverKey C)) \ @@ -590,7 +646,7 @@ 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 + (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); @@ -633,51 +689,67 @@ - -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; +(*If C=Enemy then of course he could make up all sorts of nonsense.*) +goal thy + "!!evs. evs : traces ==> \ +\ EX X'. ALL C S A Y N B X. \ +\ C ~= Enemy --> \ +\ Says S A Y : setOfList evs --> \ +\ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \ +\ (X = X'))"; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) +by (dtac Says_S_message_form_eq 5 THEN assume_tac 5); +by (ALLGOALS + (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); +(*NS2: Case split propagates some context to other subgoal...*) +by (excluded_middle_tac "K = newK evsa" 2); +by (Asm_simp_tac 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)] + 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 13 **) +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] + addDs [impOfSubs parts_insert_subset_Un] + addss (!simpset)) 2); +by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 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); +val lemma = result(); -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; +(*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 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); +\ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : setOfList evs; \ + \ Says S' A' \ +\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : setOfList evs; \ +\ \ +\ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; +bd lemma 1; +be exE 1; +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); +by (Fast_tac 1); +qed "unique_session_keys"; -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 @@ -689,7 +761,7 @@ 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 (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) by (REPEAT_FIRST (resolve_tac [conjI, impI])); by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); @@ -699,14 +771,13 @@ (!simpset addsimps ([analyze_subset_parts RS contra_subsetD, analyze_insert_Key_newK] @ pushes) setloop split_tac [expand_if]))); - (*NS2*) -by (Fast_tac 2); +by (fast_tac (!claset addSEs [less_irrefl]) 2); (** LEVEL 9 **) (*Now for the Fake case*) br notI 1; by (subgoal_tac - "Key (newK evs') : \ + "Key (newK evt) : \ \ analyze (synthesize (analyze (insert (Key (serverKey C)) \ \ (sees Enemy evsa))))" 1); be (impOfSubs analyze_mono) 2; @@ -717,7 +788,7 @@ (*Proves the Fake goal*) by (fast_tac (!claset addss (!simpset)) 1); -(**LEVEL 16**) +(**LEVEL 14**) (*Now for NS3*) (*NS3, case 1: that message from the Server was just sent*) by (ALLGOALS (forward_tac [traces_ConsE])); @@ -735,222 +806,79 @@ (*simplify the good implication*) by (Asm_full_simp_tac 1); -by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); (*delete the bad implication*) +(*delete the bad implication*) +by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1); 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 **) +(**LEVEL 24 **) 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 (asm_full_simp_tac + (!simpset addsimps (mem_if::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); +(**LEVEL 28 **) +bd ([impOfSubs setOfList_subset_Cons, setOfList_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); +qed "Enemy_not_see_encrypted_key"; -by (forward_tac [setOfList_I1 RSN (2, Server_or_Enemy)] 1); - - - (!simpset addsimps ([analyze_subset_parts RS keysFor_mono RS contra_subsetD])) 1); +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; -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*) +goals_limit:=4; -br notI 1; -bd (impOfSubs analyze_insert_Crypt_subset) 1; -????????????????????????????????????????????????????????????????; - -(**LEVEL 35 **) +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"; -(*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); +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"; -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*) +(*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}"; -br notI 1; -bd (impOfSubs analyze_insert_Crypt_subset) 1; - - +by (Step_tac 1); +br ccontr 1; +by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); +qed "knownBy_encrypted_key"; -(**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(); @@ -1219,170 +1147,14 @@ 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; - - -(*Fake case below may need something like this...*) -goal thy - "!!evs. evs : traces ==> \ -\ ALL B X. Crypt X (serverKey B) : analyze (sees Enemy evs) --> \ -\ (EX A A'. Says A A' (Crypt X (serverKey B)) : setOfList evs"; - -goal thy - "!!evs. evs : traces ==> \ -\ ALL NA B K X. Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B) : - analyze (sees Enemy evs) --> \ -\ (EX A A'. Says A A' (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B)) : setOfList evs"; - - -(*Describes the form of X when the following message is sent*) -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 --> \ -\ (EX evs'. X = (Crypt {|Key(newK evs'), 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 2); (*Solves the NS2 case*) -(*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 [all_conj_distrib]) 2); -be conjE 2; -by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent (Friend i)|} (serverKey B)" 2); -by (eres_inst_tac [("V","?P|?Q")] thin_rl 3); (*speeds the following step*) -by (Fast_tac 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*) -be disjE 1; -(*The subcase of Fake, where the message in question is NOT the most recent*) -by (Best_tac 2); -(*The subcase of Fake proved because server keys are kept secret*) -by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); -be Crypt_synthesize 1; -be Key_synthesize 2; -by (Asm_full_simp_tac 2); - - - - 1. !!evs B X evsa S A NA Ba K Xa. - [| evsa : traces; - ! S A NA B K X. - Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) : - setOfList evsa --> - (? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)); - B ~= Enemy; - Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey B) : - analyze (sees Enemy evsa) |] ==> - ? evs'. Xa = Crypt {|Key (newK evs'), Agent B|} (serverKey Ba) - - -(*Split up the possibilities of that message being synthesized...*) -by (Step_tac 1); -by (Best_tac 6); - - - - -by (Safe_step_tac 1); -by (Safe_step_tac 2); -by (ALLGOALS Asm_full_simp_tac); -by (REPEAT_FIRST (etac disjE)); -by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); - - -by (hyp_subst_tac 5); - - - - - -by (REPEAT (dtac spec 3)); -fe conjE; -fe mp ; -by (REPEAT (resolve_tac [refl, conjI] 3)); -by (REPEAT_FIRST (etac conjE)); -by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); - - -by (subgoal_tac "? evs'. Xa = Crypt {|Key (newK evs'), Agent Aa|} (serverKey Ba)" 2); -by (Fast_tac 3); - - - -be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*) - - -auto(); -by (ALLGOALS - (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,de_Morgan_conj]))); -by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); - -by (REPEAT (Safe_step_tac 1)); - -qed "Says_Crypt_Nonce_imp_msg_Crypt"; - -goal thy - "!!evs. [| Says S 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)))"; YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; -WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW; (*If a message is sent, encrypted with a Friend's server key, then either that Friend or the Server originally sent it.*) @@ -1439,44 +1211,6 @@ - (*The NS3 case needs the induction hypothesis twice! - One application is to the X component of the most recent message.*) - -???????????????????????????????????????????????????????????????? -by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 1); -by (Fast_tac 2); - -by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1); - -be conjE 1; -(*DELETE the first quantified formula: it's now useless*) -by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 1); -by (fast_tac (!claset addss (!simpset)) 1); - - -(*Now for the Fake case*) -be disjE 1; -(*The subcase of Fake, where the message in question is NOT the most recent*) -by (Best_tac 2); - -WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW; - - - - - - -goal thy - "!!evs. evs : traces ==> \ -\ Says Server A \ -\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \ -\ --> (EX evs'. N = Nonce (newN evs'))"; -be traces.induct 1; -by (ALLGOALS Asm_simp_tac); -by (Fast_tac 1); -val Says_Server_lemma = result(); - - (*NEEDED??*) goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)"; diff -r 23765bc3e8e2 -r fa58f4a06f21 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Mon Jul 29 18:30:01 1996 +0200 +++ b/src/HOL/Auth/Event.thy Mon Jul 29 18:31:39 1996 +0200 @@ -102,9 +102,9 @@ |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) # evs : traces" - (*We can't trust the sender field: change that A to A'? *) - NS2 "[| evs: traces; A ~= B; - evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs' + (*We can't trust the sender field, hence the A' in it *) + NS2 "[| evs: traces; A ~= B; A ~= Server; + evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs' |] ==> (Says Server A (Crypt {|Nonce NA, Agent B, Key (newK evs), (Crypt {|Key (newK evs), Agent A|} (serverKey B))|} diff -r 23765bc3e8e2 -r fa58f4a06f21 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Mon Jul 29 18:30:01 1996 +0200 +++ b/src/HOL/Auth/Message.ML Mon Jul 29 18:31:39 1996 +0200 @@ -124,6 +124,12 @@ qed "parts_emptyE"; AddSEs [parts_emptyE]; +(*WARNING: loops if H = {Y}, therefore must not be repeated!*) +goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}"; +be parts.induct 1; +by (ALLGOALS Fast_tac); +qed "parts_singleton"; + (** Unions **)