# HG changeset patch # User paulson # Date 853501771 -3600 # Node ID 4d68fbe6378b5c451788ab31951305ac5f0d41b0 # Parent 6ff9bd353121690e84ece8c28f858ebbe0492389 Now with Andy Gordon's treatment of freshness to replace newN/K diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Message.ML Fri Jan 17 12:49:31 1997 +0100 @@ -18,16 +18,6 @@ Simp_tac i; - -(*GOALS.ML??*) -fun prlim n = (goals_limit:=n; pr()); - -(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) -goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; -by (fast_tac (!claset addEs [equalityE]) 1); -val subset_range_iff = result(); - - open Message; AddIffs (msg.inject); @@ -44,49 +34,6 @@ Addsimps [invKey, invKey_eq]; -(**** Freeness laws for HPair ****) - -goalw thy [HPair_def] "Agent A ~= HPair X Y"; -by (Simp_tac 1); -qed "Agent_neq_HPair"; - -goalw thy [HPair_def] "Nonce N ~= HPair X Y"; -by (Simp_tac 1); -qed "Nonce_neq_HPair"; - -goalw thy [HPair_def] "Key K ~= HPair X Y"; -by (Simp_tac 1); -qed "Key_neq_HPair"; - -goalw thy [HPair_def] "Hash Z ~= HPair X Y"; -by (Simp_tac 1); -qed "Hash_neq_HPair"; - -goalw thy [HPair_def] "Crypt K X' ~= HPair X Y"; -by (Simp_tac 1); -qed "Crypt_neq_HPair"; - -val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, - Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; - -AddIffs HPair_neqs; -AddIffs (HPair_neqs RL [not_sym]); - -goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)"; -by (Simp_tac 1); -qed "HPair_eq"; - -goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)"; -by (Simp_tac 1); -qed "MPair_eq_HPair"; - -goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; -by (Auto_tac()); -qed "HPair_eq_MPair"; - -AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; - - (**** keysFor operator ****) goalw thy [keysFor_def] "keysFor {} = {}"; @@ -133,7 +80,7 @@ Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, - keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; + keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; by (Fast_tac 1); @@ -282,8 +229,8 @@ fun parts_tac i = EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, - etac parts.induct i, - REPEAT (fast_tac (!claset addss (!simpset)) i)]; + etac parts.induct i, + REPEAT (fast_tac (!claset addss (!simpset)) i)]; goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; by (parts_tac 1); @@ -410,8 +357,8 @@ fun analz_tac i = EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, - etac analz.induct i, - REPEAT (fast_tac (!claset addss (!simpset)) i)]; + etac analz.induct i, + REPEAT (fast_tac (!claset addss (!simpset)) i)]; goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; by (analz_tac 1); @@ -488,7 +435,7 @@ qed "analz_Crypt_if"; Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, - analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; + analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; (*This rule supposes "for the sake of argument" that we have the key.*) goal thy "analz (insert (Crypt K X) H) <= \ @@ -587,7 +534,7 @@ but can synth a pair or encryption from its components...*) val mk_cases = synth.mk_cases msg.simps; -(*NO Agent_synth, as any Agent name can be synthd*) +(*NO Agent_synth, as any Agent name can be synthesized*) val Nonce_synth = mk_cases "Nonce n : synth H"; val Key_synth = mk_cases "Key K : synth H"; val Hash_synth = mk_cases "Hash X : synth H"; @@ -752,17 +699,6 @@ by (Fast_tac 1); qed "Fake_analz_insert"; -(*Needed????????????????*) -goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \ -\ analz (insert X H) <= synth (analz H) Un analz H"; -by (rtac subsetI 1); -by (subgoal_tac "x : analz (synth (analz H))" 1); -by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] - addSEs [impOfSubs analz_mono]) 2); -by (Full_simp_tac 1); -by (Fast_tac 1); -qed "Fake_analz_insert_old"; - goal thy "(X: analz H & X: parts H) = (X: analz H)"; by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); val analz_conj_parts = result(); @@ -788,8 +724,8 @@ qed "Crypt_synth_analz"; -goal thy "!!K. Key K ~: analz H \ -\ ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)"; +goal thy "!!K. X ~: synth (analz H) \ +\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)"; by (Fast_tac 1); qed "Hash_synth_analz"; Addsimps [Hash_synth_analz]; @@ -799,41 +735,41 @@ (*** Freeness ***) -goalw thy [HPair_def] "Agent A ~= HPair X Y"; +goalw thy [HPair_def] "Agent A ~= Hash[X] Y"; by (Simp_tac 1); qed "Agent_neq_HPair"; -goalw thy [HPair_def] "Nonce N ~= HPair X Y"; +goalw thy [HPair_def] "Nonce N ~= Hash[X] Y"; by (Simp_tac 1); qed "Nonce_neq_HPair"; -goalw thy [HPair_def] "Key K ~= HPair X Y"; +goalw thy [HPair_def] "Key K ~= Hash[X] Y"; by (Simp_tac 1); qed "Key_neq_HPair"; -goalw thy [HPair_def] "Hash Z ~= HPair X Y"; +goalw thy [HPair_def] "Hash Z ~= Hash[X] Y"; by (Simp_tac 1); qed "Hash_neq_HPair"; -goalw thy [HPair_def] "Crypt K X' ~= HPair X Y"; +goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y"; by (Simp_tac 1); qed "Crypt_neq_HPair"; val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, - Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; + Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; AddIffs HPair_neqs; AddIffs (HPair_neqs RL [not_sym]); -goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)"; +goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; by (Simp_tac 1); qed "HPair_eq"; -goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)"; +goalw thy [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"; by (Simp_tac 1); qed "MPair_eq_HPair"; -goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; +goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; by (Auto_tac()); qed "HPair_eq_MPair"; @@ -842,31 +778,31 @@ (*** Specialized laws, proved in terms of those for Hash and MPair ***) -goalw thy [HPair_def] "keysFor (insert (HPair X Y) H) = keysFor H"; +goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; by (Simp_tac 1); qed "keysFor_insert_HPair"; goalw thy [HPair_def] - "parts (insert (HPair X Y) H) = \ -\ insert (HPair X Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"; + "parts (insert (Hash[X] Y) H) = \ +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"; by (Simp_tac 1); qed "parts_insert_HPair"; goalw thy [HPair_def] - "analz (insert (HPair X Y) H) = \ -\ insert (HPair X Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"; + "analz (insert (Hash[X] Y) H) = \ +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"; by (Simp_tac 1); qed "analz_insert_HPair"; goalw thy [HPair_def] "!!H. X ~: synth (analz H) \ -\ ==> (HPair X Y : synth (analz H)) = \ +\ ==> (Hash[X] Y : synth (analz H)) = \ \ (Hash {|X, Y|} : analz H & Y : synth (analz H))"; by (Simp_tac 1); by (Fast_tac 1); qed "HPair_synth_analz"; Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, - HPair_synth_analz, HPair_synth_analz]; + HPair_synth_analz, HPair_synth_analz]; (*We do NOT want Crypt... messages broken up in protocols!!*) @@ -881,7 +817,7 @@ val pushKeys = map (insComm thy "Key ?K") ["Agent ?C", "Nonce ?N", "Hash ?X", - "MPair ?X ?Y", "Crypt ?X ?K'"]; + "MPair ?X ?Y", "Crypt ?X ?K'"]; val pushCrypts = map (insComm thy "Crypt ?X ?K") ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"]; @@ -898,7 +834,7 @@ val Fake_insert_tac = dresolve_tac [impOfSubs Fake_analz_insert, - impOfSubs Fake_parts_insert] THEN' + impOfSubs Fake_parts_insert] THEN' eresolve_tac [asm_rl, synth.Inj]; (*Analysis of Fake cases and of messages that forward unknown parts. @@ -916,9 +852,9 @@ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])), DEPTH_SOLVE (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1 - THEN - IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono, - impOfSubs analz_subset_parts]) 2 1)) + THEN + IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono, + impOfSubs analz_subset_parts]) 2 1)) ]) i); (** Useful in many uniqueness proofs **) @@ -929,10 +865,10 @@ their standard form*) fun prove_unique_tac lemma = EVERY' [dtac lemma, - REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]), - (*Duplicate the assumption*) - forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl, - fast_tac (!claset addSDs [spec])]; + REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]), + (*Duplicate the assumption*) + forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl, + fast_tac (!claset addSDs [spec])]; (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Message.thy Fri Jan 17 12:49:31 1997 +0100 @@ -41,7 +41,7 @@ (*Allows messages of the form {|A,B,NA|}, etc...*) syntax - "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") + "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") translations "{|x, y, z|}" == "{|x, {|y, z|}|}" @@ -50,8 +50,8 @@ constdefs (*Message Y, paired with a MAC computed with the help of X*) - HPair :: "[msg,msg]=>msg" - "HPair X Y == {| Hash{|X,Y|}, Y|}" + HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000]) + "Hash[X] Y == {| Hash{|X,Y|}, Y|}" (*Keys useful to decrypt elements of a message set*) keysFor :: msg set => key set diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/NS_Public.ML Fri Jan 17 12:49:31 1997 +0100 @@ -11,7 +11,6 @@ proof_timing:=true; HOL_quantifiers := false; -Pretty.setdepth 20; AddIffs [Spy_in_lost]; @@ -26,10 +25,7 @@ \ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE] - addss (!simpset setsolver safe_solver)))); +by possibility_tac; result(); @@ -84,9 +80,9 @@ fun analz_induct_tac i = - etac ns_public.induct i THEN + etac ns_public.induct i THEN ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz] + (!simpset addsimps [not_parts_not_analz] setloop split_tac [expand_if])); (**** Authenticity properties obtained from NS2 ****) @@ -105,9 +101,9 @@ by (fast_tac (!claset addSEs partsEs) 3); (*Fake*) by (best_tac (!claset addIs [analz_insertI] - addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2); + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); (*Base*) by (fast_tac (!claset addss (!simpset)) 1); bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); @@ -132,8 +128,8 @@ by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); by (best_tac (!claset delrules [conjI] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] addss (!simpset)) 1); val lemma = result(); @@ -158,7 +154,7 @@ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); (*NS1*) by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy' RS parts.Inj] + addSDs [Says_imp_sees_Spy' RS parts.Inj] addIs [impOfSubs analz_subset_parts]) 2); (*Fake*) by (spy_analz_tac 1); @@ -191,9 +187,9 @@ by (fast_tac (!claset addss (!simpset)) 1); by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); qed_spec_mp "NA_decrypt_imp_B_msg"; (*Corollary: if A receives B's message NS2 and the nonce NA agrees @@ -219,10 +215,10 @@ by (analz_induct_tac 1); (*Fake*) by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addIs [analz_insertI] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 2); + addSDs [impOfSubs Fake_parts_insert] + addIs [analz_insertI] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 2); (*Base*) by (fast_tac (!claset addss (!simpset)) 1); qed_spec_mp "B_trusts_NS1"; @@ -252,9 +248,9 @@ by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); by (best_tac (!claset delrules [conjI] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); val lemma = result(); goal thy @@ -317,14 +313,14 @@ by (fast_tac (!claset addss (!simpset)) 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); (*NS3*) by (Step_tac 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] - addDs [unique_NB]) 1); + addDs [unique_NB]) 1); qed_spec_mp "NB_decrypt_imp_A_msg"; (*Corollary: if B receives message NS3 and the nonce NB agrees, @@ -363,14 +359,14 @@ by (fast_tac (!claset addss (!simpset)) 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (best_tac (!claset addSIs [disjI2] - addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 1); + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); (*NS3*) by (Step_tac 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] - addDs [unique_NB]) 1); + addDs [unique_NB]) 1); val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp); goal thy diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/NS_Public.thy --- a/src/HOL/Auth/NS_Public.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/NS_Public.thy Fri Jan 17 12:49:31 1997 +0100 @@ -37,9 +37,9 @@ (*Alice proves her existence by sending NB back to Bob.*) NS3 "[| evs: ns_public; A ~= B; - Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) + Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; - Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) + Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) : set_of_list evs |] ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public" diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/NS_Public_Bad.ML --- a/src/HOL/Auth/NS_Public_Bad.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Jan 17 12:49:31 1997 +0100 @@ -15,7 +15,6 @@ proof_timing:=true; HOL_quantifiers := false; -Pretty.setdepth 20; AddIffs [Spy_in_lost]; @@ -30,10 +29,7 @@ \ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE] - addss (!simpset setsolver safe_solver)))); +by possibility_tac; result(); @@ -88,9 +84,9 @@ fun analz_induct_tac i = - etac ns_public.induct i THEN + etac ns_public.induct i THEN ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz] + (!simpset addsimps [not_parts_not_analz] setloop split_tac [expand_if])); @@ -110,9 +106,9 @@ by (fast_tac (!claset addSEs partsEs) 3); (*Fake*) by (best_tac (!claset addIs [analz_insertI] - addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2); + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); (*Base*) by (fast_tac (!claset addss (!simpset)) 1); bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); @@ -137,8 +133,8 @@ by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); by (best_tac (!claset delrules [conjI] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] addss (!simpset)) 1); val lemma = result(); @@ -163,7 +159,7 @@ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); (*NS1*) by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy' RS parts.Inj] + addSDs [Says_imp_sees_Spy' RS parts.Inj] addIs [impOfSubs analz_subset_parts]) 2); (*Fake*) by (spy_analz_tac 1); @@ -193,9 +189,9 @@ by (fast_tac (!claset addss (!simpset)) 1); by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); (*NS2*) by (Step_tac 1); by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); @@ -225,10 +221,10 @@ by (analz_induct_tac 1); (*Fake*) by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addIs [analz_insertI] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 2); + addSDs [impOfSubs Fake_parts_insert] + addIs [analz_insertI] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 2); (*Base*) by (fast_tac (!claset addss (!simpset)) 1); qed_spec_mp "B_trusts_NS1"; @@ -257,9 +253,9 @@ by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); by (best_tac (!claset delrules [conjI] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); val lemma = result(); goal thy @@ -316,18 +312,18 @@ (*Fake*) by (REPEAT_FIRST (resolve_tac [impI, conjI])); by (fast_tac (!claset addss (!simpset)) 1); -br (ccontr RS disjI2) 1; +by (rtac (ccontr RS disjI2) 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); by (Fast_tac 1); by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); (*NS3*) by (Step_tac 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1)); by (Fast_tac 1); by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addDs [unique_NB]) 1); + addDs [unique_NB]) 1); qed_spec_mp "NB_decrypt_imp_A_msg"; diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Jan 17 12:49:31 1997 +0100 @@ -41,9 +41,9 @@ (*Alice proves her existence by sending NB back to Bob.*) NS3 "[| evs: ns_public; A ~= B; - Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) + Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; - Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) + Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs |] ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public" diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Fri Jan 17 12:49:31 1997 +0100 @@ -22,10 +22,9 @@ \ ==> EX N K. EX evs: ns_shared lost. \ \ Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS + ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); +by possibility_tac; result(); @@ -52,15 +51,13 @@ (*For reasoning about the encrypted portion of message NS3*) goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \ \ ==> X : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "NS3_msg_in_parts_sees_Spy"; goal thy "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \ \ ==> K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "Oops_parts_sees_Spy"; val parts_Fake_tac = @@ -107,72 +104,18 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) - -(*Nobody can have SEEN keys that will be generated in the future. *) +(*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : ns_shared lost ==> \ -\ length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -by (ALLGOALS (fast_tac (!claset addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK i) : parts {X}; \ -\ evs : ns_shared lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - - -(*** Future nonces can't be seen or used! ***) - -goal thy "!!evs. evs : ns_shared lost ==> \ -\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)"; +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (REPEAT_FIRST - (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_nonces_not_seen"; -Addsimps [new_nonces_not_seen]; - - -(*Nobody can have USED keys that will be generated in the future. - ...very like new_keys_not_seen*) -goal thy "!!evs. evs : ns_shared lost ==> \ -\ length evs <= i --> \ -\ newK i ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); -(*NS1 and NS2*) -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2])); -(*Fake and NS3*) -by (EVERY - (map - (best_tac - (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] - addss (!simpset))) - [2,1])); -(*NS4 and NS5: nonce exchange*) -by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys] - addIs [less_SucI, impOfSubs keysFor_mono] - addss (!simpset addsimps [le_def])) 1)); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); +(*NS2, NS4, NS5*) +by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1)); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -186,14 +129,15 @@ (*Describes the form of K, X and K' when the Server sends this message.*) goal thy - "!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \ -\ evs : ns_shared lost |] \ -\ ==> (EX i. K = Key(newK i) & \ -\ X = (Crypt (shrK B) {|K, Agent A|}) & \ -\ K' = shrK A)"; + "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \ +\ : set_of_list evs; \ +\ evs : ns_shared lost |] \ +\ ==> K ~: range shrK & \ +\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \ +\ K' = shrK A"; by (etac rev_mp 1); by (etac ns_shared.induct 1); -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +by (Auto_tac()); qed "Says_Server_message_form"; @@ -219,16 +163,14 @@ goal thy "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \ \ : set_of_list evs; evs : ns_shared lost |] \ -\ ==> (EX i. K = newK i & i < length evs & \ -\ X = (Crypt (shrK B) {|Key K, Agent A|})) \ -\ | X : analz (sees lost Spy evs)"; +\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \ +\ | X : analz (sees lost Spy evs)"; by (case_tac "A : lost" 1); by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] addss (!simpset)) 1); by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1); by (fast_tac (!claset addEs partsEs addSDs [A_trusts_NS2, Says_Server_message_form] - addIs [Says_imp_old_keys] addss (!simpset)) 1); qed "Says_S_message_form"; @@ -237,14 +179,13 @@ val analz_Fake_tac = forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN - Full_simp_tac 7 THEN - REPEAT_FIRST (eresolve_tac [asm_rl, exE, disjE] ORELSE' hyp_subst_tac); + REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -256,8 +197,8 @@ to encrypt messages containing other keys, in the actual protocol. We require that agents should behave like this subsequently also.*) goal thy - "!!evs. evs : ns_shared lost ==> \ -\ (Crypt (newK i) X) : parts (sees lost Spy evs) & \ + "!!evs. [| evs : ns_shared lost; Kab ~: range shrK |] ==> \ +\ (Crypt KAB X) : parts (sees lost Spy evs) & \ \ Key K : parts {X} --> Key K : parts (sees lost Spy evs)"; by (etac ns_shared.induct 1); by parts_Fake_tac; @@ -276,31 +217,28 @@ (*The equality makes the induction hypothesis easier to apply*) goal thy "!!evs. evs : ns_shared lost ==> \ -\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ -\ (K : newK``E | Key K : analz (sees lost Spy evs))"; +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac ns_shared.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 18 secs*) - (asm_simp_tac - (!simpset addsimps [Un_assoc RS sym, - insert_Key_singleton, insert_Key_image, pushKey_newK] - setloop split_tac [expand_if]))); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +(*Takes 24 secs*) +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*NS4, Fake*) -by (EVERY (map spy_analz_tac [5,2])); -(*NS3, NS2, Base*) -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -qed_spec_mp "analz_image_newK"; +by (EVERY (map spy_analz_tac [3,2])); +(*Base*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. evs : ns_shared lost ==> \ -\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \ -\ (K = newK i | Key K : analz (sees lost Spy 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"; + "!!evs. [| evs : ns_shared lost; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; (** The session key K uniquely identifies the message, if encrypted @@ -320,8 +258,8 @@ (*NS2: it can't be a new key*) by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] - delrules [conjI] (*prevent split-up into 4 subgoals*) +by (fast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*) + addSEs sees_Spy_partsEs addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); @@ -352,15 +290,14 @@ by analz_Fake_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps ([not_parts_not_analz, - analz_insert_Key_newK] @ pushes) + (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes) setloop split_tac [expand_if]))); +(*NS4, Fake*) +by (EVERY (map spy_analz_tac [4,1])); (*NS2*) -by (fast_tac (!claset addIs [parts_insertI] - addEs [Says_imp_old_keys RS less_irrefl] - addss (!simpset)) 2); -(*NS4, Fake*) -by (EVERY (map spy_analz_tac [3,1])); +by (fast_tac (!claset addSEs sees_Spy_partsEs + addIs [parts_insertI, impOfSubs analz_subset_parts] + addss (!simpset)) 1); (*NS3 and Oops subcases*) (**LEVEL 5 **) by (step_tac (!claset delrules [impCE]) 1); by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); @@ -382,10 +319,10 @@ (*Final version: Server's message in the most abstract form*) goal thy "!!evs. [| Says Server A \ -\ (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs; \ -\ (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs); \ +\ (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs; \ +\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs); \ \ A ~: lost; B ~: lost; evs : ns_shared lost \ -\ |] ==> K ~: analz (sees lost Spy evs)"; +\ |] ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -394,10 +331,10 @@ goal thy "!!evs. [| C ~: {A,B,Server}; \ \ Says Server A \ -\ (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs; \ -\ (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs); \ +\ (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs; \ +\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs); \ \ A ~: lost; B ~: lost; evs : ns_shared lost |] \ -\ ==> K ~: analz (sees lost C evs)"; +\ ==> Key K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); @@ -449,8 +386,8 @@ addDs [impOfSubs analz_subset_parts]) 1); by (Fast_tac 2); by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); -(*Contradiction from the assumption - Crypt (newK(length evsa)) (Nonce NB) : parts (sees lost Spy evsa) *) +(*Subgoal 1: contradiction from the assumptions + Key K ~: used evsa and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *) by (dtac Crypt_imp_invKey_keysFor 1); (**LEVEL 10**) by (Asm_full_simp_tac 1); @@ -460,7 +397,7 @@ by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1); by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN REPEAT (assume_tac 1)); -by (fast_tac (!claset addDs [unique_session_keys]) 1); +by (best_tac (!claset addDs [unique_session_keys]) 1); val lemma = result(); goal thy diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/NS_Shared.thy Fri Jan 17 12:49:31 1997 +0100 @@ -26,20 +26,20 @@ ==> Says Spy B X # evs : ns_shared lost" (*Alice initiates a protocol run, requesting to talk to any B*) - NS1 "[| evs: ns_shared lost; A ~= Server |] - ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|} - # evs : ns_shared lost" + NS1 "[| evs: ns_shared lost; A ~= Server; Nonce NA ~: used evs |] + ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs + : ns_shared lost" (*Server's response to Alice's message. !! It may respond more than once to A's request !! Server doesn't know who the true sender is, hence the A' in the sender field.*) - NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; + NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; Key KAB ~: used evs; Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] ==> Says Server A (Crypt (shrK A) - {|Nonce NA, Agent B, Key (newK(length evs)), - (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) + {|Nonce NA, Agent B, Key KAB, + (Crypt (shrK B) {|Key KAB, Agent A|})|}) # evs : ns_shared lost" (*We can't assume S=Server. Agent A "remembers" her nonce. @@ -52,9 +52,9 @@ (*Bob's nonce exchange. He does not know who the message came from, but responds to A because she is mentioned inside.*) - NS4 "[| evs: ns_shared lost; A ~= B; + NS4 "[| evs: ns_shared lost; A ~= B; Nonce NB ~: used evs; Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |] - ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs + ==> Says B A (Crypt K (Nonce NB)) # evs : ns_shared lost" (*Alice responds with Nonce NB if she has seen the key before. diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Fri Jan 17 12:49:31 1997 +0100 @@ -26,9 +26,7 @@ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +by possibility_tac; result(); @@ -59,15 +57,14 @@ by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR2_analz_sees_Spy"; -goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs \ +goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \ \ ==> X : analz (sees lost Spy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR4_analz_sees_Spy"; goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ \ ==> K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "Oops_parts_sees_Spy"; (*OR2_analz... and OR4_analz... let us treat those cases using the same @@ -84,9 +81,9 @@ harder to complete, since simplification does less for us.*) val parts_Fake_tac = let val tac = forw_inst_tac [("lost","lost")] - in tac OR2_parts_sees_Spy 4 THEN - tac OR4_parts_sees_Spy 6 THEN - tac Oops_parts_sees_Spy 7 + in tac OR2_parts_sees_Spy 4 THEN + tac OR4_parts_sees_Spy 6 THEN + tac Oops_parts_sees_Spy 7 end; (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) @@ -128,77 +125,18 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) - -(*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!i. evs : otway lost ==> \ -\ length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK i) : parts {X}; \ -\ evs : otway lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - -(*** Future nonces can't be seen or used! ***) - -goal thy "!!evs. evs : otway lost ==> \ -\ length evs <= i --> \ -\ Nonce (newN i) ~: parts (sees lost Spy evs)"; +(*Nobody can have used non-existent keys!*) +goal thy "!!evs. evs : otway lost ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (REPEAT_FIRST (fast_tac (!claset - addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_nonces_not_seen"; -Addsimps [new_nonces_not_seen]; - -(*Variant: old messages must contain old nonces!*) -goal thy "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN i) : parts {X}; \ -\ evs : otway lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_nonces"; - - -(*Nobody can have USED keys that will be generated in the future. - ...very like new_keys_not_seen*) -goal thy "!!i. evs : otway lost ==> \ -\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))"; -by (parts_induct_tac 1); -(*OR1 and OR3*) -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); -(*Fake, OR2, OR4: these messages send unknown (X) components*) -by (REPEAT - (best_tac - (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] - addss (!simpset)) 1)); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); +(*OR1-3*) +by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -214,11 +152,10 @@ (*Describes the form of K and NA when the Server sends this message. Also for Oops case.*) goal thy - "!!evs. [| Says Server B \ -\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ + "!!evs. [| Says Server B \ +\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ \ evs : otway lost |] \ -\ ==> (EX n. K = Key(newK n)) & \ -\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; +\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -230,14 +167,14 @@ dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN - assume_tac 7 THEN Full_simp_tac 7 THEN + assume_tac 7 THEN REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -248,32 +185,28 @@ (*The equality makes the induction hypothesis easier to apply*) goal thy - "!!evs. evs : otway lost ==> \ -\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ -\ (K : newK``E | Key K : analz (sees lost Spy evs))"; + "!!evs. evs : otway lost ==> \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 11 secs*) - (asm_simp_tac - (!simpset addsimps [Un_assoc RS sym, - insert_Key_singleton, insert_Key_image, pushKey_newK] - setloop split_tac [expand_if]))); -(*OR4, OR2, Fake*) -by (EVERY (map spy_analz_tac [5,3,2])); -(*Oops, OR3, Base*) -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -qed_spec_mp "analz_image_newK"; +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); +(*Base*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +(*Fake, OR2, OR4*) +by (REPEAT (spy_analz_tac 1)); +qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. evs : otway lost ==> \ -\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \ -\ (K = newK i | Key K : analz (sees lost Spy 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"; + "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; (*** The Key K uniquely identifies the Server's message. **) @@ -291,8 +224,8 @@ by (Fast_tac 2); by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -(*...we assume X is a very new message, and handle this case by contradiction*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +(*...we assume X is a recent message, and handle this case by contradiction*) +by (fast_tac (!claset addSEs sees_Spy_partsEs delrules [conjI] (*prevent split-up into 4 subgoals*) addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); @@ -333,8 +266,7 @@ by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*OR1: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NA = ?y" 1); -by (best_tac (!claset addSEs partsEs - addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); +by (best_tac (!claset addSEs sees_Spy_partsEs) 1); val lemma = result(); goal thy @@ -346,8 +278,6 @@ qed "unique_NA"; -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); - (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because OR2 encrypts Nonce NB. It prevents the attack that can occur in the over-simplified version of this protocol: see OtwayRees_Bad.*) @@ -358,7 +288,7 @@ \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ \ ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); -by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now]) +by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addSDs [impOfSubs parts_insert_subset_Un] addss (!simpset)) 1)); qed_spec_mp"no_nonce_OR1_OR2"; @@ -380,16 +310,14 @@ by (parts_induct_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (fast_tac (!claset addSIs [parts_insertI] - addSEs partsEs - addEs [Says_imp_old_nonces RS less_irrefl] + addSEs sees_Spy_partsEs addss (!simpset)) 1); (*OR3 and OR4*) (*OR4*) by (REPEAT (Safe_step_tac 2)); by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); by (fast_tac (!claset addSIs [Crypt_imp_OR1] - addEs partsEs - addDs [Says_imp_sees_Spy RS parts.Inj]) 2); + addEs sees_Spy_partsEs) 2); (*OR3*) (** LEVEL 5 **) by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); by (step_tac (!claset delrules [disjCI, impCE]) 1); @@ -420,8 +348,7 @@ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set_of_list evs"; by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] - addEs partsEs - addDs [Says_imp_sees_Spy RS parts.Inj]) 1); + addEs sees_Spy_partsEs) 1); qed "A_trusts_OR4"; @@ -439,11 +366,13 @@ by (etac otway.induct 1); by analz_Fake_tac; by (ALLGOALS - (asm_simp_tac (!simpset addsimps [not_parts_not_analz, - analz_insert_Key_newK] - setloop split_tac [expand_if]))); + (asm_simp_tac (!simpset addcongs [conj_cong] + addsimps [not_parts_not_analz, analz_insert_freshK] + setloop split_tac [expand_if]))); (*OR3*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +by (fast_tac (!claset delrules [impCE] + addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts] addss (!simpset addsimps [parts_insert2])) 3); (*OR4, OR2, Fake*) by (REPEAT_FIRST spy_analz_tac); @@ -453,12 +382,12 @@ val lemma = result() RS mp RS mp RSN(2,rev_notE); goal thy - "!!evs. [| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, K|}, \ -\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ -\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ + "!!evs. [| Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : otway lost |] \ -\ ==> K ~: analz (sees lost Spy evs)"; +\ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -467,11 +396,11 @@ goal thy "!!evs. [| C ~: {A,B,Server}; \ \ Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, K|}, \ -\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ -\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : otway lost |] \ -\ ==> K ~: analz (sees lost C evs)"; +\ ==> Key K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); @@ -507,7 +436,7 @@ by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*OR2: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NB = ?y" 1); -by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1); +by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1); val lemma = result(); goal thy @@ -537,8 +466,7 @@ by (parts_induct_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (fast_tac (!claset addSIs [parts_insertI] - addSEs partsEs - addEs [Says_imp_old_nonces RS less_irrefl] + addSEs sees_Spy_partsEs addss (!simpset)) 1); (*OR4*) by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); @@ -570,8 +498,7 @@ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set_of_list evs"; by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] - addEs partsEs - addDs [Says_imp_sees_Spy RS parts.Inj]) 1); + addEs sees_Spy_partsEs) 1); qed "B_trusts_OR3"; diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/OtwayRees.thy Fri Jan 17 12:49:31 1997 +0100 @@ -28,27 +28,26 @@ ==> Says Spy B X # evs : otway lost" (*Alice initiates a protocol run*) - OR1 "[| evs: otway lost; A ~= B; B ~= Server |] - ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, - Crypt (shrK A) - {|Nonce (newN(length evs)), Agent A, Agent B|} |} + OR1 "[| evs: otway lost; A ~= B; B ~= Server; Nonce NA ~: used evs |] + ==> Says A B {|Nonce NA, Agent A, Agent B, + Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} # evs : otway lost" (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field. Note that NB is encrypted.*) - OR2 "[| evs: otway lost; B ~= Server; + OR2 "[| evs: otway lost; B ~= Server; Nonce NB ~: used evs; Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] ==> Says B Server {|Nonce NA, Agent A, Agent B, X, Crypt (shrK B) - {|Nonce NA, Nonce(newN(length evs)), Agent A, Agent B|}|} + {|Nonce NA, Nonce NB, Agent A, Agent B|}|} # evs : otway lost" (*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3 "[| evs: otway lost; B ~= Server; + OR3 "[| evs: otway lost; B ~= Server; Key KAB ~: used evs; Says B' Server {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, @@ -56,18 +55,18 @@ : set_of_list evs |] ==> Says Server B {|Nonce NA, - Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|}, - Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|} + Crypt (shrK A) {|Nonce NA, Key KAB|}, + Crypt (shrK B) {|Nonce NB, Key KAB|}|} # evs : otway lost" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server.*) OR4 "[| evs: otway lost; A ~= B; - Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} - : set_of_list evs; Says B Server {|Nonce NA, Agent A, Agent B, X', Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} + : set_of_list evs; + Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} : set_of_list evs |] ==> Says B A {|Nonce NA, X|} # evs : otway lost" diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 17 12:49:31 1997 +0100 @@ -26,9 +26,7 @@ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +by possibility_tac; result(); @@ -54,15 +52,14 @@ (** For reasoning about the encrypted portion of messages **) -goal thy "!!evs. Says S B {|X, X'|} : set_of_list evs ==> \ +goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \ \ X : analz (sees lost Spy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR4_analz_sees_Spy"; goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ \ : set_of_list evs ==> K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "Oops_parts_sees_Spy"; (*OR4_analz_sees_Spy lets us treat those cases using the same @@ -81,9 +78,9 @@ (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] addss (!simpset)) 2)) THEN (*Base case*) fast_tac (!claset addss (!simpset)) 1 THEN @@ -117,49 +114,18 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) - -(*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!i. evs : otway lost ==> \ -\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)"; +(*Nobody can have used non-existent keys!*) +goal thy "!!evs. evs : otway lost ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK i) : parts {X}; \ -\ evs : otway lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - -(*Nobody can have USED keys that will be generated in the future. - ...very like new_keys_not_seen*) -goal thy "!!i. evs : otway lost ==> \ -\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); -(*Fake, OR4: these messages send unknown (X) components*) -by (EVERY - (map - (best_tac - (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] - addss (!simpset))) [5,1])); -(*Remaining subgoals*) -by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1)); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); +(*OR3*) +by (fast_tac (!claset addss (!simpset)) 1); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -174,12 +140,12 @@ (*Describes the form of K and NA when the Server sends this message.*) goal thy - "!!evs. [| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \ -\ evs : otway lost |] \ -\ ==> (EX n. K = Key(newK n)) & \ -\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; + "!!evs. [| Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set_of_list evs; \ +\ evs : otway lost |] \ +\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -190,18 +156,17 @@ val analz_Fake_tac = dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN - assume_tac 7 THEN Full_simp_tac 7 THEN + assume_tac 7 THEN REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. - ****) @@ -210,31 +175,28 @@ (*The equality makes the induction hypothesis easier to apply*) goal thy "!!evs. evs : otway lost ==> \ -\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ -\ (K : newK``E | Key K : analz (sees lost Spy evs))"; +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 18 secs*) - (asm_simp_tac - (!simpset addsimps [Un_assoc RS sym, - insert_Key_singleton, insert_Key_image, pushKey_newK] - setloop split_tac [expand_if]))); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +(*14 seconds*) +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*OR4, Fake*) -by (EVERY (map spy_analz_tac [4,2])); -(*Oops, OR3, Base*) -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -qed_spec_mp "analz_image_newK"; +by (EVERY (map spy_analz_tac [3,2])); +(*Base*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. evs : otway lost ==> \ -\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \ -\ (K = newK i | Key K : analz (sees lost Spy 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"; + "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; (*** The Key K uniquely identifies the Server's message. **) @@ -254,8 +216,8 @@ by (Fast_tac 2); by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -(*...we assume X is a very new message, and handle this case by contradiction*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +(*...we assume X is a recent message and handle this case by contradiction*) +by (fast_tac (!claset addSEs sees_Spy_partsEs delrules [conjI] (*prevent split-up into 4 subgoals*) addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); @@ -306,8 +268,7 @@ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set_of_list evs"; by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] - addEs partsEs - addDs [Says_imp_sees_Spy RS parts.Inj]) 1); + addEs sees_Spy_partsEs) 1); qed "A_trusts_OR4"; @@ -326,38 +287,43 @@ by (etac otway.induct 1); by analz_Fake_tac; by (ALLGOALS - (asm_simp_tac (!simpset addsimps [not_parts_not_analz, - analz_insert_Key_newK] - setloop split_tac [expand_if]))); + (asm_simp_tac (!simpset addcongs [conj_cong] + addsimps [not_parts_not_analz, + analz_insert_freshK] + setloop split_tac [expand_if]))); (*OR3*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +by (fast_tac (!claset delrules [impCE] + addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts] addss (!simpset addsimps [parts_insert2])) 2); +(*Oops*) +by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3); (*OR4, Fake*) by (REPEAT_FIRST spy_analz_tac); -(*Oops*) -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); goal thy - "!!evs. [| Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\ -\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ -\ A ~: lost; B ~: lost; evs : otway lost |] \ -\ ==> K ~: analz (sees lost Spy evs)"; + "!!evs. [| Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set_of_list evs; \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : otway lost |] \ +\ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; goal thy - "!!evs. [| C ~: {A,B,Server}; \ -\ Says Server B \ -\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \ -\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\ -\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ -\ A ~: lost; B ~: lost; evs : otway lost |] \ -\ ==> K ~: analz (sees lost C evs)"; + "!!evs. [| C ~: {A,B,Server}; \ +\ Says Server B \ +\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ +\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +\ : set_of_list evs; \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : otway lost |] \ +\ ==> Key K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); @@ -394,6 +360,5 @@ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set_of_list evs"; by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] - addEs partsEs - addDs [Says_imp_sees_Spy RS parts.Inj]) 1); + addEs sees_Spy_partsEs) 1); qed "B_trusts_OR3"; diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Jan 17 12:49:31 1997 +0100 @@ -7,6 +7,11 @@ Simplified version with minimal encryption but explicit messages +Note that the formalization does not even assume that nonces are fresh. +This is because the protocol does not rely on uniqueness of nonces for +security, only for freshness, and the proof script does not prove freshness +properties. + From page 11 of Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. IEEE Trans. SE 22 (1), 1996 @@ -29,36 +34,31 @@ (*Alice initiates a protocol run*) OR1 "[| evs: otway lost; A ~= B; B ~= Server |] - ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|} - # evs : otway lost" + ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost" (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field.*) OR2 "[| evs: otway lost; B ~= Server; Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] - ==> Says B Server {|Agent A, Agent B, Nonce NA, - Nonce (newN(length evs))|} + ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs : otway lost" (*The Server receives Bob's message. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3 "[| evs: otway lost; B ~= Server; A ~= B; + OR3 "[| evs: otway lost; B ~= Server; A ~= B; Key KAB ~: used evs; Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set_of_list evs |] ==> Says Server B - {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, - Key(newK(length evs))|}, - Crypt (shrK B) {|Nonce NB, Agent A, Agent B, - Key(newK(length evs))|}|} + {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|}, + Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} # evs : otway lost" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server.*) OR4 "[| evs: otway lost; A ~= B; - Says S B {|X, - Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|} + Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set_of_list evs; - Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} + Says S B {|X, Crypt(shrK B){|Nonce NB, Agent A, Agent B, Key K|}|} : set_of_list evs |] ==> Says B A X # evs : otway lost" diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 17 12:49:31 1997 +0100 @@ -29,24 +29,12 @@ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +by possibility_tac; result(); (**** Inductive proofs about otway ****) -(*The Spy can see more than anybody else, except for their initial state*) -goal thy - "!!evs. evs : otway ==> \ -\ sees lost A evs <= initState lost A Un sees lost Spy evs"; -by (etac otway.induct 1); -by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] - addss (!simpset)))); -qed "sees_agent_subset_sees_Spy"; - - (*Nobody sends themselves messages*) goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs"; by (etac otway.induct 1); @@ -63,15 +51,14 @@ by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR2_analz_sees_Spy"; -goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \ +goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \ \ X : analz (sees lost Spy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR4_analz_sees_Spy"; goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ \ ==> K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "Oops_parts_sees_Spy"; (*OR2_analz... and OR4_analz... let us treat those cases using the same @@ -92,9 +79,9 @@ (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] addss (!simpset)) 2)) THEN (*Base case*) fast_tac (!claset addss (!simpset)) 1 THEN @@ -129,76 +116,18 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) - -(*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!i. evs : otway ==> \ -\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK i) : parts {X}; \ -\ evs : otway \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - -(*** Future nonces can't be seen or used! ***) - -goal thy "!!i. evs : otway ==> \ -\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)"; +(*Nobody can have used non-existent keys!*) +goal thy "!!evs. evs : otway ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (REPEAT_FIRST - (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_nonces_not_seen"; -Addsimps [new_nonces_not_seen]; - -(*Variant: old messages must contain old nonces!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN i) : parts {X}; \ -\ evs : otway \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_nonces"; - - -(*Nobody can have USED keys that will be generated in the future. - ...very like new_keys_not_seen*) -goal thy "!!i. evs : otway ==> \ -\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); -(*OR1 and OR3*) -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); -(*Fake, OR2, OR4: these messages send unknown (X) components*) -by (REPEAT - (best_tac - (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] - addss (!simpset)) 1)); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); +(*OR1-3*) +by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -214,11 +143,10 @@ (*Describes the form of K and NA when the Server sends this message. Also for Oops case.*) goal thy - "!!evs. [| Says Server B \ -\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ -\ evs : otway |] \ -\ ==> (EX n. K = Key(newK n)) & \ -\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; + "!!evs. [| Says Server B \ +\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ +\ evs : otway |] \ +\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -229,61 +157,46 @@ val analz_Fake_tac = dtac OR2_analz_sees_Spy 4 THEN dtac OR4_analz_sees_Spy 6 THEN - forward_tac [Says_Server_message_form] 7 THEN - assume_tac 7 THEN Full_simp_tac 7 THEN + forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. - ****) (** Session keys are not used to encrypt other session keys **) -(*Lemma for the trivial direction of the if-and-only-if*) -goal thy - "!!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(); - - (*The equality makes the induction hypothesis easier to apply*) goal thy "!!evs. evs : otway ==> \ -\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ -\ (K : newK``E | Key K : analz (sees lost Spy evs))"; +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (ares_tac [allI, lemma])); -by (ALLGOALS (*Takes 18 secs*) - (asm_simp_tac - (!simpset addsimps [Un_assoc RS sym, - insert_Key_singleton, insert_Key_image, pushKey_newK] - setloop split_tac [expand_if]))); -(*OR4, OR2, Fake*) -by (EVERY (map spy_analz_tac [5,3,2])); -(*Oops, OR3, Base*) -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -qed_spec_mp "analz_image_newK"; +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); +(*Base*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +(*Fake, OR2, OR4*) +by (REPEAT (spy_analz_tac 1)); +qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. evs : otway ==> \ -\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \ -\ (K = newK i | Key K : analz (sees lost Spy 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"; + "!!evs. [| evs : otway; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; (*** The Key K uniquely identifies the Server's message. **) @@ -301,8 +214,8 @@ by (Fast_tac 2); by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -(*...we assume X is a very new message, and handle this case by contradiction*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +(*...we assume X is a recent message, and handle this case by contradiction*) +by (fast_tac (!claset addSEs sees_Spy_partsEs delrules [conjI] (*prevent split-up into 4 subgoals*) addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); @@ -328,27 +241,28 @@ by (etac otway.induct 1); by analz_Fake_tac; by (ALLGOALS - (asm_simp_tac (!simpset addsimps [not_parts_not_analz, - analz_insert_Key_newK] - setloop split_tac [expand_if]))); + (asm_simp_tac (!simpset addcongs [conj_cong] + addsimps [not_parts_not_analz, analz_insert_freshK] + setloop split_tac [expand_if]))); (*OR3*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +by (fast_tac (!claset delrules [impCE] + addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts] addss (!simpset addsimps [parts_insert2])) 3); (*OR4, OR2, Fake*) by (REPEAT_FIRST spy_analz_tac); (*Oops*) (** LEVEL 5 **) by (fast_tac (!claset delrules [disjE] - addDs [unique_session_keys] addss (!simpset)) 1); + addDs [unique_session_keys] addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); - goal thy - "!!evs. [| Says Server B \ -\ {|NA, Crypt (shrK A) {|NA, K|}, \ -\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ -\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ + "!!evs. [| Says Server B \ +\ {|NA, Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs; \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : otway |] \ -\ ==> K ~: analz (sees lost Spy evs)"; +\ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -359,9 +273,9 @@ (*Only OR1 can have caused such a part of a message to appear. I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. Perhaps it's because OR2 has two similar-looking encrypted messages in - this version.*) + this version.*) goal thy - "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ + "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ \ : parts (sees lost Spy evs) --> \ \ Says A B {|NA, Agent A, Agent B, \ @@ -390,15 +304,13 @@ by (parts_induct_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (fast_tac (!claset addSIs [parts_insertI] - addSEs partsEs - addEs [Says_imp_old_nonces RS less_irrefl] + addSEs sees_Spy_partsEs addss (!simpset)) 1); (*OR4*) by (REPEAT (Safe_step_tac 2)); by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); by (fast_tac (!claset addSIs [Crypt_imp_OR1] - addEs partsEs - addDs [Says_imp_sees_Spy RS parts.Inj]) 2); + addEs sees_Spy_partsEs) 2); (*OR3*) (** LEVEL 5 **) by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); by (step_tac (!claset delrules [disjCI, impCE]) 1); diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Jan 17 12:49:31 1997 +0100 @@ -27,26 +27,25 @@ ==> Says Spy B X # evs : otway" (*Alice initiates a protocol run*) - OR1 "[| evs: otway; A ~= B; B ~= Server |] - ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, - Crypt (shrK A) - {|Nonce (newN(length evs)), Agent A, Agent B|} |} + OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |] + ==> Says A B {|Nonce NA, Agent A, Agent B, + Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} # evs : otway" (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field. We modify the published protocol by NOT encrypting NB.*) - OR2 "[| evs: otway; B ~= Server; + OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs; Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] ==> Says B Server - {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)), + {|Nonce NA, Agent A, Agent B, X, Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} # evs : otway" (*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3 "[| evs: otway; B ~= Server; + OR3 "[| evs: otway; B ~= Server; Key KAB ~: used evs; Says B' Server {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, @@ -55,16 +54,16 @@ : set_of_list evs |] ==> Says Server B {|Nonce NA, - Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|}, - Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|} + Crypt (shrK A) {|Nonce NA, Key KAB|}, + Crypt (shrK B) {|Nonce NB, Key KAB|}|} # evs : otway" (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server.*) OR4 "[| evs: otway; A ~= B; - Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} + Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} : set_of_list evs; - Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} + Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} : set_of_list evs |] ==> Says B A {|Nonce NA, X|} # evs : otway" diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Public.ML --- a/src/HOL/Auth/Public.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Public.ML Fri Jan 17 12:49:31 1997 +0100 @@ -158,18 +158,20 @@ AddIffs [Nonce_notin_initState]; goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs"; -be (impOfSubs parts_mono) 1; +by (etac (impOfSubs parts_mono) 1); by (Fast_tac 1); qed "usedI"; AddIs [usedI]; -(*Yields a supply of fresh nonces for possibility theorems.*) +(** A supply of fresh nonces for possibility theorems. **) + goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs"; by (list.induct_tac "evs" 1); by (res_inst_tac [("x","0")] exI 1); by (Step_tac 1); by (Full_simp_tac 1); +(*Inductive step*) by (event.induct_tac "a" 1); by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1); by (msg.induct_tac "msg" 1); @@ -184,11 +186,18 @@ val lemma = result(); goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; -br (lemma RS exE) 1; -br selectI 1; +by (rtac (lemma RS exE) 1); +by (rtac selectI 1); by (Fast_tac 1); qed "Nonce_supply"; +(*Tactic for possibility theorems*) +val possibility_tac = + REPEAT + (ALLGOALS (simp_tac (!simpset setsolver safe_solver)) + THEN + REPEAT_FIRST (eq_assume_tac ORELSE' + resolve_tac [refl, conjI, Nonce_supply])); (** Power of the Spy **) diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Recur.ML Fri Jan 17 12:49:31 1997 +0100 @@ -10,29 +10,26 @@ proof_timing:=true; HOL_quantifiers := false; -Pretty.setdepth 25; +Pretty.setdepth 30; (** Possibility properties: traces that reach the end - ONE theorem would be more elegant and faster! - By induction on a list of agents (no repetitions) + ONE theorem would be more elegant and faster! + By induction on a list of agents (no repetitions) **) + (*Simplest case: Alice goes directly to the server*) goal thy "!!A. A ~= Server \ \ ==> EX K NA. EX evs: recur lost. \ -\ Says Server A {|Agent A, \ -\ Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ +\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ \ Agent Server|} \ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (recur.Nil RS recur.RA1 RS - (respond.One RSN (4,recur.RA3))) 2); -by (REPEAT - (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)) - THEN - REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]))); + (respond.One RSN (4,recur.RA3))) 2); +by possibility_tac; result(); @@ -40,44 +37,42 @@ goal thy "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ \ ==> EX K. EX NA. EX evs: recur lost. \ -\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ \ Agent Server|} \ \ : set_of_list evs"; +by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); +by (REPEAT (eresolve_tac [exE, conjE] 1)); by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS - (respond.One RS respond.Cons RSN (4,recur.RA3)) RS - recur.RA4) 2); -bw HPair_def; -by (REPEAT - (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]) - THEN - ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)))); + (respond.One RS respond.Cons RSN (4,recur.RA3)) RS + recur.RA4) 2); +by basic_possibility_tac; +by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, + less_not_refl2 RS not_sym] 1)); result(); -(*Case three: Alice, Bob, Charlie and the server*) +(*Case three: Alice, Bob, Charlie and the server goal thy - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ + "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \ \ ==> EX K. EX NA. EX evs: recur lost. \ -\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ \ Agent Server|} \ \ : set_of_list evs"; +by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); +by (REPEAT (eresolve_tac [exE, conjE] 1)); by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS - (respond.One RS respond.Cons RS respond.Cons RSN - (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); -bw HPair_def; -by (REPEAT (*SLOW: 37 seconds*) - (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]) - THEN - ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)))); -by (ALLGOALS - (SELECT_GOAL (DEPTH_SOLVE - (swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND - etac not_sym 1)))); + (respond.One RS respond.Cons RS respond.Cons RSN + (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); +(*SLOW: 70 seconds*) +by basic_possibility_tac; +by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 + ORELSE + eresolve_tac [asm_rl, less_not_refl2, + less_not_refl2 RS not_sym] 1)); result(); - - +****************) (**** Inductive proofs about recur ****) @@ -99,10 +94,30 @@ AddSEs [not_Says_to_self RSN (2, rev_notE)]; + +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}"; +by (etac respond.induct 1); +by (ALLGOALS Simp_tac); +qed "respond_Key_in_parts"; + +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs"; +by (etac respond.induct 1); +by (REPEAT (assume_tac 1)); +qed "respond_imp_not_used"; + +goal thy + "!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \ +\ ==> Key K ~: used evs"; +by (etac rev_mp 1); +by (etac respond.induct 1); +by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used], + !simpset)); +qed_spec_mp "Key_in_parts_respond"; + (*Simple inductive reasoning about responses*) -goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i"; +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs"; by (etac respond.induct 1); -by (REPEAT (ares_tac responses.intrs 1)); +by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); qed "respond_imp_responses"; @@ -110,7 +125,7 @@ val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard; -goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \ +goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \ \ ==> RA : analz (sees lost Spy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "RA4_analz_sees_Spy"; @@ -131,8 +146,8 @@ let val tac = forw_inst_tac [("lost","lost")] in tac RA2_parts_sees_Spy 4 THEN etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN - forward_tac [respond_imp_responses] 5 THEN - tac RA4_parts_sees_Spy 6 + forward_tac [respond_imp_responses] 5 THEN + tac RA4_parts_sees_Spy 6 end; (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) @@ -153,14 +168,6 @@ (** Spy never sees another agent's long-term key (unless initially lost) **) goal thy - "!!evs. (j,PB,RB) : respond i \ -\ ==> Key K : parts {RB} --> (EX j'. K = newK2(i,j') & j<=j')"; -be respond.induct 1; -by (Auto_tac()); -by (best_tac (!claset addDs [Suc_leD]) 1); -qed_spec_mp "Key_in_parts_respond"; - -goal thy "!!evs. evs : recur lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; by (parts_induct_tac 1); @@ -189,115 +196,30 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) + +(** Nobody can have used non-existent keys! **) -(*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!evs. evs : recur lost ==> \ -\ length evs <= i --> \ -\ Key (newK2(i,j)) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -(*RA2*) -by (best_tac (!claset addSEs partsEs - addSDs [parts_cut] - addDs [Suc_leD] - addss (!simpset)) 3); -(*Fake*) -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)) 1); -(*For RA3*) -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2); -(*RA1-RA4*) -by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD] - addss (!simpset)) 1)); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK2(i,j)) : parts {X}; \ -\ evs : recur lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - -(*** Future nonces can't be seen or used! ***) - -goal thy - "!!evs. (j, PB, RB) : respond i \ -\ ==> Nonce N : parts {RB} --> Nonce N : parts {PB}"; -be respond.induct 1; +goal thy + "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \ +\ ==> K : range shrK"; +by (etac rev_mp 1); +by (etac (respond_imp_responses RS responses.induct) 1); by (Auto_tac()); -qed_spec_mp "Nonce_in_parts_respond"; +qed_spec_mp "Key_in_keysFor_parts"; -goal thy "!!i. evs : recur lost ==> \ -\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -(*For RA3*) -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4); -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] - addDs [Nonce_in_parts_respond, parts_cut, Suc_leD] - addss (!simpset)) 0 4); -(*Fake*) -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)) 1); -(*RA1, RA2, RA4*) -by (REPEAT_FIRST (fast_tac (!claset - addSEs partsEs - addEs [leD RS notE] - addDs [Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_nonces_not_seen"; -Addsimps [new_nonces_not_seen]; - -(*Variant: old messages must contain old nonces!*) -goal thy "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN i) : parts {X}; \ -\ evs : recur lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_nonces"; - - -(** Nobody can have USED keys that will be generated in the future. **) - -goal thy - "!!evs. (j,PB,RB) : respond i \ -\ ==> K : keysFor (parts {RB}) --> (EX A. K = shrK A)"; -be (respond_imp_responses RS responses.induct) 1; -by (Auto_tac()); -qed_spec_mp "Key_in_keysFor_parts_respond"; - - -goal thy "!!i. evs : recur lost ==> \ -\ length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))"; +goal thy "!!evs. evs : recur lost ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); (*RA3*) -by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD] - addss (!simpset addsimps [parts_insert_sees])) 4); -(*RA2*) -by (fast_tac (!claset addSEs partsEs - addDs [Suc_leD] addss (!simpset)) 3); -(*Fake, RA1, RA4*) -by (REPEAT - (best_tac - (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] - addss (!simpset)) 1)); +by (best_tac (!claset addDs [Key_in_keysFor_parts] + addss (!simpset addsimps [parts_insert_sees])) 2); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); qed_spec_mp "new_keys_not_used"; @@ -319,86 +241,82 @@ dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6; -Delsimps [image_insert]; - (** Session keys are not used to encrypt other session keys **) (*Version for "responses" relation. Handles case RA3 in the theorem below. Note that it holds for *any* set H (not just "sees lost Spy evs") satisfying the inductive hypothesis.*) goal thy - "!!evs. [| RB : responses i; \ -\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \ -\ (K : newK``I | Key K : analz H) |] \ -\ ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \ -\ (K : newK``I | Key K : analz (insert RB H))"; -be responses.induct 1; -by (ALLGOALS - (asm_simp_tac - (!simpset addsimps [insert_Key_singleton, insert_Key_image, - Un_assoc RS sym, pushKey_newK] - setloop split_tac [expand_if]))); -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); -qed "resp_analz_image_newK_lemma"; + "!!evs. [| RB : responses evs; \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un H)) = \ +\ (K : KK | Key K : analz H) |] \ +\ ==> ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (insert RB (Key``KK Un H))) = \ +\ (K : KK | Key K : analz (insert RB H))"; +by (etac responses.induct 1); +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); +qed "resp_analz_image_freshK_lemma"; (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) goal thy - "!!evs. evs : recur lost ==> \ -\ ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \ -\ (K : newK``I | Key K : analz (sees lost Spy evs))"; + "!!evs. evs : recur lost ==> \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac recur.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma]))); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +by (ALLGOALS + (asm_simp_tac + (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); (*Base*) by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); (*RA4, RA2, Fake*) by (REPEAT (spy_analz_tac 1)); -val raw_analz_image_newK = result(); -qed_spec_mp "analz_image_newK"; +val raw_analz_image_freshK = result(); +qed_spec_mp "analz_image_freshK"; (*Instance of the lemma with H replaced by (sees lost Spy evs): - [| RB : responses i; evs : recur lost |] - ==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) = - (xa : newK``x | Key xa : analz (insert RB (sees lost Spy evs))) + [| RB : responses evs; evs : recur lost; |] + ==> KK <= Compl (range shrK) --> + Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) = + (K : KK | Key K : analz (insert RB (sees lost Spy evs))) *) -bind_thm ("resp_analz_image_newK", - raw_analz_image_newK RSN - (2, resp_analz_image_newK_lemma) RS spec RS spec); +bind_thm ("resp_analz_image_freshK", + raw_analz_image_freshK RSN + (2, resp_analz_image_freshK_lemma) RS spec RS spec); goal thy - "!!evs. evs : recur lost ==> \ -\ Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \ -\ (K = newK x | Key K : analz (sees lost Spy 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"; + "!!evs. [| evs : recur lost; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; -(*This is more general than proving Hash_new_nonces_not_seen: we don't prove - that "future nonces" can't be hashed, but that everything that's hashed is - already in past traffic. *) +(*Everything that's hashed is already in past traffic. *) goal thy "!!i. [| evs : recur lost; A ~: lost |] ==> \ \ Hash {|Key(shrK A), X|} : parts (sees lost Spy evs) --> \ \ X : parts (sees lost Spy evs)"; -be recur.induct 1; +by (etac recur.induct 1); by parts_Fake_tac; (*RA3 requires a further induction*) -be responses.induct 5; +by (etac responses.induct 5); by (ALLGOALS Asm_simp_tac); (*Fake*) by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset addsimps [parts_insert_sees])) 2); + impOfSubs Fake_parts_insert] + addss (!simpset addsimps [parts_insert_sees])) 2); (*Two others*) by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); bind_thm ("Hash_imp_body", result() RSN (2, rev_mp)); (** The Nonce NA uniquely identifies A's message. - This theorem applies to rounds RA1 and RA2! + This theorem applies to steps RA1 and RA2! Unicity is not used in other proofs but is desirable in its own right. **) @@ -409,29 +327,20 @@ \ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \ \ : parts (sees lost Spy evs) --> B=B' & P=P'"; by (parts_induct_tac 1); -be responses.induct 3; +by (etac responses.induct 3); by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); by (step_tac (!claset addSEs partsEs) 1); -(*RA1: creation of new Nonce. Move assertion into global context*) -by (expand_case_tac "NA = ?y" 1); -by (best_tac (!claset addSIs [exI] - addSDs [Hash_imp_body] - addSEs (new_nonces_not_seen::partsEs) - addss (!simpset)) 1); -by (best_tac (!claset addss (!simpset)) 1); -(*RA2: creation of new Nonce*) -by (expand_case_tac "NA = ?y" 1); -by (best_tac (!claset addSIs [exI] - addSDs [Hash_imp_body] - addSEs (new_nonces_not_seen::partsEs) - addss (!simpset)) 1); -by (best_tac (!claset addss (!simpset)) 1); +(*RA1,2: creation of new Nonce. Move assertion into global context*) +by (ALLGOALS (expand_case_tac "NA = ?y")); +by (REPEAT_FIRST (ares_tac [exI])); +by (REPEAT (best_tac (!claset addSDs [Hash_imp_body] + addSEs sees_Spy_partsEs) 1)); val lemma = result(); goalw thy [HPair_def] - "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|} \ + "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} \ \ : parts (sees lost Spy evs); \ -\ HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \ +\ Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \ \ : parts (sees lost Spy evs); \ \ evs : recur lost; A ~: lost |] \ \ ==> B=B' & P=P'"; @@ -445,39 +354,36 @@ ***) goal thy - "!!evs. [| RB : responses i; evs : recur lost |] \ + "!!evs. [| RB : responses evs; evs : recur lost |] \ \ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)"; -be responses.induct 1; +by (etac responses.induct 1); by (ALLGOALS (asm_simp_tac - (!simpset addsimps [resp_analz_image_newK, insert_Key_singleton] - setloop split_tac [expand_if]))); + (analz_image_freshK_ss addsimps [Spy_analz_shrK, + resp_analz_image_freshK]))); qed "shrK_in_analz_respond"; Addsimps [shrK_in_analz_respond]; goal thy - "!!evs. [| RB : responses i; \ -\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \ -\ (K : newK``I | Key K : analz H) |] \ + "!!evs. [| RB : responses evs; \ +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un H)) = \ +\ (K : KK | Key K : analz H) |] \ \ ==> (Key K : analz (insert RB H)) --> \ -\ (Key K : parts{RB} | Key K : analz H)"; -be responses.induct 1; +\ (Key K : parts{RB} | Key K : analz H)"; +by (etac responses.induct 1); by (ALLGOALS (asm_simp_tac - (!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert, - resp_analz_image_newK_lemma, - insert_Key_singleton, insert_Key_image, - Un_assoc RS sym, pushKey_newK] - setloop split_tac [expand_if]))); -(*The "Message" simpset gives the standard treatment of "image"*) -by (simp_tac (simpset_of "Message") 1); + (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); +(*Simplification using two distinct treatments of "image"*) +by (simp_tac (!simpset addsimps [parts_insert2]) 1); by (fast_tac (!claset delrules [allE]) 1); qed "resp_analz_insert_lemma"; bind_thm ("resp_analz_insert", - raw_analz_image_newK RSN - (2, resp_analz_insert_lemma) RSN(2, rev_mp)); + raw_analz_image_freshK RSN + (2, resp_analz_insert_lemma) RSN(2, rev_mp)); (*The Server does not send such messages. This theorem lets us avoid @@ -487,44 +393,51 @@ \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \ \ ~: set_of_list evs"; by (etac recur.induct 1); -be (respond.induct) 5; +by (etac (respond.induct) 5); by (Auto_tac()); qed_spec_mp "Says_Server_not"; AddSEs [Says_Server_not RSN (2,rev_notE)]; +(*The last key returned by respond indeed appears in a certificate*) goal thy - "!!i. (j,PB,RB) : respond i \ -\ ==> EX A' B'. ALL A B N. \ + "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \ +\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}"; +by (etac respond.elim 1); +by (ALLGOALS Asm_full_simp_tac); +qed "respond_certificate"; + + +goal thy + "!!K'. (PB,RB,KXY) : respond evs \ +\ ==> EX A' B'. ALL A B N. \ \ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \ \ --> (A'=A & B'=B) | (A'=B & B'=A)"; -be respond.induct 1; +by (etac respond.induct 1); by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); (*Base case*) by (Fast_tac 1); by (Step_tac 1); +(*Case analysis on K=KBC*) by (expand_case_tac "K = ?y" 1); +by (dtac respond_Key_in_parts 1); by (best_tac (!claset addSIs [exI] addSEs partsEs - addDs [Key_in_parts_respond] - addss (!simpset)) 1); + addDs [Key_in_parts_respond]) 1); +(*Case analysis on K=KAB*) by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [exI] 2)); by (ex_strip_tac 1); -be respond.elim 1; -by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac)); -by (ALLGOALS (asm_full_simp_tac - (!simpset addsimps [all_conj_distrib, ex_disj_distrib]))); -by (Fast_tac 1); +by (dtac respond_certificate 1); by (Fast_tac 1); val lemma = result(); goal thy "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \ \ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \ -\ (j,PB,RB) : respond i |] \ +\ (PB,RB,KXY) : respond evs |] \ \ ==> (A'=A & B'=B) | (A'=B & B'=A)"; -by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*) +by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*) qed "unique_session_keys"; @@ -533,47 +446,34 @@ the premises, e.g. by having A=Spy **) goal thy - "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \ -\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}"; -be respond.elim 1; -by (ALLGOALS Asm_full_simp_tac); -qed "newK2_respond_lemma"; - - -goal thy - "!!evs. [| (j,PB,RB) : respond (length evs); evs : recur lost |] \ + "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur lost |] \ \ ==> ALL A A' N. A ~: lost & A' ~: lost --> \ \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ \ Key K ~: analz (insert RB (sees lost Spy evs))"; -be respond.induct 1; +by (etac respond.induct 1); by (forward_tac [respond_imp_responses] 2); -by (ALLGOALS (*4 MINUTES???*) +by (forward_tac [respond_imp_not_used] 2); +by (ALLGOALS (*43 seconds*) (asm_simp_tac - (!simpset addsimps - ([analz_image_newK, not_parts_not_analz, - read_instantiate [("H", "?ff``?xx")] parts_insert, - Un_assoc RS sym, resp_analz_image_newK, - insert_Key_singleton, analz_insert_Key_newK]) - setloop split_tac [expand_if]))); -by (ALLGOALS (simp_tac (simpset_of "Message"))); -by (Fast_tac 1); + (analz_image_freshK_ss addsimps + [analz_image_freshK, not_parts_not_analz, + shrK_in_analz_respond, + read_instantiate [("H", "?ff``?xx")] parts_insert, + resp_analz_image_freshK, analz_insert_freshK]))); +by (ALLGOALS Simp_tac); +by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); by (step_tac (!claset addSEs [MPair_parts]) 1); -(** LEVEL 6 **) -by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond] - addSEs [new_keys_not_seen RS not_parts_not_analz - RSN(2,rev_notE)] - addss (!simpset)) 4); -by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3); +(** LEVEL 7 **) +by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond] + addDs [impOfSubs analz_subset_parts]) 4); +by (fast_tac (!claset addSDs [respond_certificate]) 3); by (best_tac (!claset addSEs partsEs addDs [Key_in_parts_respond] addss (!simpset)) 2); -by (thin_tac "ALL x.?P(x)" 1); -be respond.elim 1; -by (fast_tac (!claset addss (!simpset)) 1); -by (step_tac (!claset addss (!simpset)) 1); -by (best_tac (!claset addSEs partsEs - addDs [Key_in_parts_respond] - addss (!simpset)) 1); +by (dtac unique_session_keys 1); +by (etac respond_certificate 1); +by (assume_tac 1); +by (Fast_tac 1); qed_spec_mp "respond_Spy_not_see_encrypted_key"; @@ -586,7 +486,7 @@ by analz_Fake_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] + (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] setloop split_tac [expand_if]))); (*RA4*) by (spy_analz_tac 4); @@ -596,13 +496,14 @@ (*RA2*) by (spy_analz_tac 1); (*RA3, case 2: K is an old key*) -by (fast_tac (!claset addSDs [resp_analz_insert] - addSEs partsEs - addDs [Key_in_parts_respond] - addEs [Says_imp_old_keys RS less_irrefl]) 2); +by (best_tac (!claset addSDs [resp_analz_insert] + addSEs partsEs + addDs [Key_in_parts_respond, + Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)] + addss (!simpset)) 2); (*RA3, case 1: use lemma previously proved by induction*) by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN - (2,rev_notE)]) 1); + (2,rev_notE)]) 1); bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp)); @@ -622,34 +523,29 @@ (**** Authenticity properties for Agents ****) (*The response never contains Hashes*) -(*NEEDED????????????????*) goal thy - "!!evs. (j,PB,RB) : respond i \ + "!!evs. (PB,RB,K) : respond evs \ \ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \ \ Hash {|Key (shrK B), M|} : parts H"; -be (respond_imp_responses RS responses.induct) 1; +by (etac (respond_imp_responses RS responses.induct) 1); by (Auto_tac()); bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp)); -(*NEEDED????????????????*) (*Only RA1 or RA2 can have caused such a part of a message to appear.*) goalw thy [HPair_def] "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \ \ : parts (sees lost Spy evs); \ \ A ~: lost; evs : recur lost |] \ -\ ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|}) \ +\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \ \ : set_of_list evs"; -be rev_mp 1; +by (etac rev_mp 1); by (parts_induct_tac 1); (*RA3*) by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1); qed_spec_mp "Hash_auth_sender"; -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); - - -(** These two results should subsume (for all agents) the guarantees proved +(** These two results subsume (for all agents) the guarantees proved separately for A and B in the Otway-Rees protocol. **) diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Recur.thy Fri Jan 17 12:49:31 1997 +0100 @@ -8,56 +8,47 @@ Recur = Shared + -syntax - newK2 :: "nat*nat => key" - -translations - "newK2 x" == "newK(nPair x)" - (*Two session keys are distributed to each agent except for the initiator, - who receives one. + who receives one. Perhaps the two session keys could be bundled into a single message. *) -consts respond :: "nat => (nat*msg*msg)set" -inductive "respond i" (*Server's response to the nested message*) +consts respond :: "event list => (msg*msg*key)set" +inductive "respond evs" (*Server's response to the nested message*) intrs (*The message "Agent Server" marks the end of a list.*) - One "A ~= Server - ==> (j, HPair (Key(shrK A)) + One "[| A ~= Server; Key KAB ~: used evs |] + ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|}, - {|Agent A, - Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|}, - Agent Server|}) - : respond i" + {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|}, + KAB) : respond evs" (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*) - Cons "[| (Suc j, PA, RA) : respond i; - PA = HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|}; + Cons "[| (PA, RA, KAB) : respond evs; + Key KBC ~: used evs; Key KBC ~: parts {RA}; + PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}; B ~= Server |] - ==> (j, HPair (Key(shrK B)) {|Agent B, Agent C, Nonce NB, PA|}, - {|Agent B, - Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|}, - Agent B, - Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|}, - RA|}) - : respond i" + ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, + {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, + Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, + RA|}, + KBC) + : respond evs" (*Induction over "respond" can be difficult due to the complexity of the subgoals. The "responses" relation formalizes the general form of its third component. *) -consts responses :: nat => msg set -inductive "responses i" +consts responses :: event list => msg set +inductive "responses evs" intrs (*Server terminates lists*) - Nil "Agent Server : responses i" + Nil "Agent Server : responses evs" - Cons "RA : responses i - ==> {|Agent B, - Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|}, - RA|} : responses i" + Cons "[| RA : responses evs; Key KAB ~: used evs |] + ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, + RA|} : responses evs" consts recur :: agent set => event list set @@ -75,40 +66,36 @@ (*Alice initiates a protocol run. "Agent Server" is just a placeholder, to terminate the nesting.*) - RA1 "[| evs: recur lost; A ~= B; A ~= Server |] + RA1 "[| evs: recur lost; A ~= B; A ~= Server; Nonce NA ~: used evs |] ==> Says A B - (HPair (Key(shrK A)) - {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}) + (Hash[Key(shrK A)] + {|Agent A, Agent B, Nonce NA, Agent Server|}) # evs : recur lost" (*Bob's response to Alice's message. C might be the Server. XA should be the Hash of the remaining components with KA, but - Bob cannot check that. + Bob cannot check that. P is the previous recur message from Alice's caller. NOTE: existing proofs don't need PA and are complicated by its - presence! See parts_Fake_tac.*) - RA2 "[| evs: recur lost; B ~= C; B ~= Server; + presence! See parts_Fake_tac.*) + RA2 "[| evs: recur lost; B ~= C; B ~= Server; Nonce NB ~: used evs; Says A' B PA : set_of_list evs; PA = {|XA, Agent A, Agent B, Nonce NA, P|} |] - ==> Says B C - (HPair (Key(shrK B)) - {|Agent B, Agent C, Nonce (newN(length evs)), PA|}) + ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) # evs : recur lost" (*The Server receives and decodes Bob's message. Then he generates a new session key and a response.*) RA3 "[| evs: recur lost; B ~= Server; Says B' Server PB : set_of_list evs; - (0,PB,RB) : respond (length evs) |] + (PB,RB,K) : respond evs |] ==> Says Server B RB # evs : recur lost" (*Bob receives the returned message and compares the Nonces with - those in the message he previously sent the Server.*) + those in the message he previously sent the Server.*) RA4 "[| evs: recur lost; A ~= B; - Says C' B {|Agent B, - Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, - Agent B, - Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|} + Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, + Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|} : set_of_list evs; Says B C {|XH, Agent B, Agent C, Nonce NB, XA, Agent A, Agent B, Nonce NA, P|} diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Shared.ML Fri Jan 17 12:49:31 1997 +0100 @@ -28,18 +28,16 @@ (*Injectiveness and freshness of new keys and nonces*) AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, - inj_newK RS inj_eq, inj_nPair RS inj_eq]; + inj_newK RS inj_eq, inj_nPair RS inj_eq]; (* invKey (shrK A) = shrK A *) -bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK); +bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys); -(* invKey (newK i) = newK i *) -bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); -Addsimps [invKey_shrK, invKey_newK]; +Addsimps [invKey_id]; goal thy "!!K. newK i = invKey K ==> newK i = K"; by (rtac (invKey_eq RS iffD1) 1); -by (Simp_tac 1); +by (Full_simp_tac 1); val newK_invKey = result(); AddSDs [newK_invKey, sym RS newK_invKey]; @@ -54,12 +52,7 @@ by (Auto_tac ()); qed "newK_notin_initState"; -goal thy "Nonce (newN i) ~: parts (initState lost B)"; -by (agent.induct_tac "B" 1); -by (Auto_tac ()); -qed "newN_notin_initState"; - -AddIffs [newK_notin_initState, newN_notin_initState]; +AddIffs [newK_notin_initState]; goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; by (agent.induct_tac "C" 1); @@ -156,6 +149,10 @@ by (Auto_tac ()); qed_spec_mp "Says_imp_sees_Spy"; +(*Use with addSEs to derive contradictions from old Says events containing + items known to be fresh*) +val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs; + goal thy "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost |] \ \ ==> X : analz (sees lost Spy evs)"; @@ -194,6 +191,181 @@ Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) +(*** Fresh nonces ***) + +goal thy "Nonce N ~: parts (initState lost B)"; +by (agent.induct_tac "B" 1); +by (Auto_tac ()); +qed "Nonce_notin_initState"; + +AddIffs [Nonce_notin_initState]; + +goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs"; +by (etac (impOfSubs parts_mono) 1); +by (Fast_tac 1); +qed "usedI"; + +AddIs [usedI]; + +(** Fresh keys never clash with long-term shared keys **) + +goal thy "Key (shrK A) : used evs"; +by (Best_tac 1); +qed "shrK_in_used"; +AddIffs [shrK_in_used]; + +(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys + from long-term shared keys*) +goal thy "!!K. Key K ~: used evs ==> K ~: range shrK"; +by (Best_tac 1); +qed "Key_not_used"; + +(*A session key cannot clash with a long-term shared key*) +goal thy "!!K. K ~: range shrK ==> shrK B ~= K"; +by (Fast_tac 1); +qed "shrK_neq"; + +Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym]; + + +goal thy "used (Says A B X # evs) = parts{X} Un used evs"; +by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1); +qed "used_Says"; +Addsimps [used_Says]; + +goal thy "used [] <= used l"; +by (list.induct_tac "l" 1); +by (event.induct_tac "a" 2); +by (ALLGOALS Asm_simp_tac); +by (Best_tac 1); +qed "used_nil_subset"; + +goal thy "used l <= used (l@l')"; +by (list.induct_tac "l" 1); +by (simp_tac (!simpset addsimps [used_nil_subset]) 1); +by (event.induct_tac "a" 1); +by (Asm_simp_tac 1); +by (Best_tac 1); +qed "used_subset_append"; + + +(*** Supply fresh nonces for possibility theorems. ***) + +goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs"; +by (list.induct_tac "evs" 1); +by (res_inst_tac [("x","0")] exI 1); +by (Step_tac 1); +by (Full_simp_tac 1); +(*Inductive step*) +by (event.induct_tac "a" 1); +by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1); +by (msg.induct_tac "msg" 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2]))); +by (Step_tac 1); +(*MPair case*) +by (res_inst_tac [("x","Na+Nb")] exI 2); +by (fast_tac (!claset addSEs [add_leE]) 2); +(*Nonce case*) +by (res_inst_tac [("x","N + Suc nat")] exI 1); +by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1); +val lemma = result(); + +goal thy "EX N. Nonce N ~: used evs"; +by (rtac (lemma RS exE) 1); +by (Fast_tac 1); +qed "Nonce_supply1"; + +goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'"; +by (cut_inst_tac [("evs","evs")] lemma 1); +by (cut_inst_tac [("evs","evs'")] lemma 1); +by (Step_tac 1); +by (res_inst_tac [("x","N")] exI 1); +by (res_inst_tac [("x","Suc (N+Na)")] exI 1); +by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, + le_add2, le_add1, + le_eq_less_Suc RS sym]) 1); +qed "Nonce_supply2"; + +goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \ +\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''"; +by (cut_inst_tac [("evs","evs")] lemma 1); +by (cut_inst_tac [("evs","evs'")] lemma 1); +by (cut_inst_tac [("evs","evs''")] lemma 1); +by (Step_tac 1); +by (res_inst_tac [("x","N")] exI 1); +by (res_inst_tac [("x","Suc (N+Na)")] exI 1); +by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1); +by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, + le_add2, le_add1, + le_eq_less_Suc RS sym]) 1); +by (rtac (less_trans RS less_not_refl2 RS not_sym) 1); +by (stac (le_eq_less_Suc RS sym) 1); +by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2); +by (REPEAT (rtac le_add1 1)); +qed "Nonce_supply3"; + +goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; +by (rtac (lemma RS exE) 1); +by (rtac selectI 1); +by (Fast_tac 1); +qed "Nonce_supply"; + +(*** Supply fresh keys for possibility theorems. ***) + +goal thy "EX K. Key K ~: used evs"; +by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1); +by (Fast_tac 1); +qed "Key_supply1"; + +val Fin_UNIV_insertI = UNIV_I RS Fin.insertI; + +goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'"; +by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1); +by (etac exE 1); +by (cut_inst_tac [("evs","evs'")] + (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1); +by (Auto_tac()); +qed "Key_supply2"; + +goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \ +\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''"; +by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1); +by (etac exE 1); +by (cut_inst_tac [("evs","evs'")] + (Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1); +by (etac exE 1); +by (cut_inst_tac [("evs","evs''")] + (Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1); +by (Step_tac 1); +by (Full_simp_tac 1); +by (fast_tac (!claset addSEs [allE]) 1); +qed "Key_supply3"; + +goal thy "Key (@ K. Key K ~: used evs) ~: used evs"; +by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1); +by (rtac selectI 1); +by (Fast_tac 1); +qed "Key_supply"; + +(*** Tactics for possibility theorems ***) + +val possibility_tac = + REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*) + (ALLGOALS (simp_tac + (!simpset delsimps [used_Says] setsolver safe_solver)) + THEN + REPEAT_FIRST (eq_assume_tac ORELSE' + resolve_tac [refl, conjI, Nonce_supply, Key_supply])); + +(*For harder protocols (such as Recur) where we have to set up some + nonces and keys initially*) +val basic_possibility_tac = + REPEAT + (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)) + THEN + REPEAT_FIRST (resolve_tac [refl, conjI])); + + (** Power of the Spy **) (*The Spy can see more than anybody else, except for their initial state*) @@ -227,25 +399,35 @@ (*Push newK applications in, allowing other keys to be pulled out*) val pushKey_newK = insComm thy "Key (newK ?evs)" "Key (shrK ?C)"; -Delsimps [image_insert]; -Addsimps [image_insert RS sym]; - -Delsimps [image_Un]; -Addsimps [image_Un RS sym]; - -goal thy "insert (Key (newK x)) H = Key `` (newK``{x}) Un H"; +goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A"; by (Fast_tac 1); -qed "insert_Key_singleton"; +qed "subset_Compl_range"; goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ \ Key `` (f `` (insert x E)) Un C"; by (Fast_tac 1); qed "insert_Key_image"; +goal thy "insert (Key K) H = Key `` {K} Un H"; +by (Fast_tac 1); +qed "insert_Key_singleton"; + +goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; +by (Fast_tac 1); +qed "insert_Key_image'"; + +val analz_image_freshK_ss = + !simpset delsimps [image_insert, image_Un] + addsimps ([image_insert RS sym, image_Un RS sym, + Key_not_used, + insert_Key_singleton, subset_Compl_range, + insert_Key_image', Un_assoc RS sym] + @disj_comms) + setloop split_tac [expand_if]; (*Lemma for the trivial direction of the if-and-only-if*) goal thy "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \ \ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)"; by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); -qed "analz_image_newK_lemma"; +qed "analz_image_freshK_lemma"; diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Shared.thy Fri Jan 17 12:49:31 1997 +0100 @@ -8,13 +8,14 @@ Server keys; initial states of agents; new nonces and keys; function "sees" *) -Shared = Message + List + +Shared = Message + List + Finite + consts shrK :: agent => key (*symmetric keys*) rules - isSym_shrK "isSymKey (shrK A)" + (*ALL keys are symmetric*) + isSym_keys "isSymKey K" consts (*Initial states of agents -- parameter of the construction*) initState :: [agent set, agent] => msg set @@ -44,6 +45,23 @@ sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" +constdefs + (*Set of items that might be visible to somebody: complement of the set + of fresh items*) + used :: event list => msg set + "used evs == parts (UN lost B. sees lost B evs)" + + +rules + (*Unlike the corresponding property of nonces, this cannot be proved. + We have infinitely many agents and there is nothing to stop their + long-term keys from exhausting all the natural numbers. The axiom + assumes that their keys are dispersed so as to leave room for infinitely + many fresh session keys. We could, alternatively, restrict agents to + an unspecified finite number.*) + Key_supply_ax "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs" + + (*Agents generate random (symmetric) keys and nonces. The numeric argument is typically the length of the current trace. An injective pairing function allows multiple keys/nonces to be generated @@ -63,6 +81,5 @@ inj_newK "inj newK" newK_neq_shrK "newK i ~= shrK A" - isSym_newK "isSymKey (newK i)" end diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/WooLam.ML Fri Jan 17 12:49:31 1997 +0100 @@ -25,10 +25,11 @@ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS - woolam.WL4 RS woolam.WL5) 2); + woolam.WL4 RS woolam.WL5) 2); by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE] + addss (!simpset setsolver safe_solver)))); result(); @@ -94,23 +95,6 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future nonces can't be seen or used! ***) - -goal thy "!!i. evs : woolam ==> \ -\ length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -by (REPEAT_FIRST (fast_tac (!claset - addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_nonces_not_seen"; -Addsimps [new_nonces_not_seen]; - - (**** Autheticity properties for Woo-Lam ****) @@ -201,6 +185,5 @@ \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; by (parts_induct_tac 1); by (Step_tac 1); -by (best_tac (!claset addSEs partsEs - addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); +by (best_tac (!claset addSEs partsEs) 1); **) diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/WooLam.thy --- a/src/HOL/Auth/WooLam.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/WooLam.thy Fri Jan 17 12:49:31 1997 +0100 @@ -35,16 +35,16 @@ ==> Says A B (Agent A) # evs : woolam" (*Bob responds to Alice's message with a challenge.*) - WL2 "[| evs: woolam; A ~= B; + WL2 "[| evs: woolam; A ~= B; Says A' B (Agent A) : set_of_list evs |] - ==> Says B A (Nonce (newN(length evs))) # evs : woolam" + ==> Says B A (Nonce NB) # evs : woolam" (*Alice responds to Bob's challenge by encrypting NB with her key. B is *not* properly determined -- Alice essentially broadcasts her reply.*) WL3 "[| evs: woolam; A ~= B; - Says B' A (Nonce NB) : set_of_list evs; - Says A B (Agent A) : set_of_list evs |] + Says A B (Agent A) : set_of_list evs; + Says B' A (Nonce NB) : set_of_list evs |] ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam" (*Bob forwards Alice's response to the Server.*) diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Yahalom.ML Fri Jan 17 12:49:31 1997 +0100 @@ -14,7 +14,7 @@ proof_timing:=true; HOL_quantifiers := false; -Pretty.setdepth 20; +Pretty.setdepth 25; (*A "possibility property": there are traces that reach the end*) @@ -23,9 +23,9 @@ \ ==> EX X NB K. EX evs: yahalom lost. \ \ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (ALLGOALS Fast_tac); +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS + yahalom.YM4) 2); +by possibility_tac; result(); @@ -115,64 +115,20 @@ AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) - -(*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!i. evs : yahalom lost ==> \ -\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)"; +(*Nobody can have used non-existent keys!*) +goal thy "!!evs. evs : yahalom lost ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK i) : parts {X}; \ -\ evs : yahalom lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - -(*Ready-made for the classical reasoner*) -goal thy "!!evs. [| Says A B {|Crypt K {|b,Key(newK(length evs)),na,nb|}, X|}\ -\ : set_of_list evs; evs : yahalom lost |] \ -\ ==> R"; -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] - addss (!simpset addsimps [parts_insertI])) 1); -qed "Says_too_new_key"; -AddSEs [Says_too_new_key]; - - -(*Nobody can have USED keys that will be generated in the future. - ...very like new_keys_not_seen*) -goal thy "!!i. evs : yahalom lost ==> \ -\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))"; -by (parts_induct_tac 1); -(*YM1, YM2 and YM3*) -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); -(*Fake and Oops: these messages send unknown (X) components*) -by (EVERY - (map (fast_tac - (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addss (!simpset))) [3,1])); -(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*) -by (fast_tac - (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [new_keys_not_seen RSN(2,rev_notE)] - addDs [Suc_leD]) 1); +(*YM4: Key K is not fresh!*) +by (fast_tac (!claset addSEs sees_Spy_partsEs) 3); +(*YM3*) +by (fast_tac (!claset addss (!simpset)) 2); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -185,10 +141,10 @@ (*Describes the form of K when the Server sends this message. Useful for Oops as well as main secrecy property.*) goal thy - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \ -\ evs : yahalom lost |] \ -\ ==> EX i. K = Key(newK i)"; + "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \ +\ : set_of_list evs; \ +\ evs : yahalom lost |] \ +\ ==> K ~: range shrK"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -199,68 +155,42 @@ val analz_Fake_tac = forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN - assume_tac 7 THEN Full_simp_tac 7 THEN - REPEAT ((etac exE ORELSE' hyp_subst_tac) 7); + assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy 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 : yahalom lost ==> \ -\ (Crypt (newK i) X) : parts (sees lost Spy evs) & \ -\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)"; -by (etac yahalom.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Deals with Faked messages*) -by (best_tac (!claset addSEs partsEs - addDs [impOfSubs parts_insert_subset_Un] - addss (!simpset)) 2); -(*Base case*) -by (Auto_tac()); -result(); - - (** Session keys are not used to encrypt other session keys **) goal thy "!!evs. evs : yahalom lost ==> \ -\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ -\ (K : newK``E | Key K : analz (sees lost Spy evs))"; +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac yahalom.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 11 secs*) - (asm_simp_tac - (!simpset addsimps [Un_assoc RS sym, - insert_Key_singleton, insert_Key_image, pushKey_newK] - setloop split_tac [expand_if]))); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); +(*Base*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); (*YM4, Fake*) -by (EVERY (map spy_analz_tac [4, 2])); -(*Oops, YM3, Base*) -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -qed_spec_mp "analz_image_newK"; +by (REPEAT (spy_analz_tac 1)); +qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. evs : yahalom lost ==> \ -\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \ -\ (K = newK i | Key K : analz (sees lost Spy evs))"; -by (asm_simp_tac (HOL_ss addsimps [analz_image_newK, - insert_Key_singleton]) 1); -by (Fast_tac 1); -qed "analz_insert_Key_newK"; + "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; (*** The Key K uniquely identifies the Server's message. **) @@ -279,8 +209,10 @@ (*Remaining case: YM3*) by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -(*...we assume X is a very new message, and handle this case by contradiction*) -by (Fast_tac 1); (*uses Says_too_new_key*) +(*...we assume X is a recent message and handle this case by contradiction*) +by (fast_tac (!claset addSEs sees_Spy_partsEs + delrules [conjI] (*prevent split-up into 4 subgoals*) + addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); goal thy @@ -324,10 +256,13 @@ by analz_Fake_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] + (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] setloop split_tac [expand_if]))); (*YM3*) -by (Fast_tac 2); (*uses Says_too_new_key*) +by (fast_tac (!claset delrules [impCE] + addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts] + addss (!simpset addsimps [parts_insert2])) 2); (*OR4, Fake*) by (REPEAT_FIRST spy_analz_tac); (*Oops*) @@ -339,25 +274,27 @@ (*Final version: Server's message in the most abstract form*) goal thy - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, \ -\ Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs; \ -\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \ -\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \ -\ K ~: analz (sees lost Spy evs)"; + "!!evs. [| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set_of_list evs; \ +\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : yahalom lost |] \ +\ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; goal thy - "!!evs. [| C ~: {A,B,Server}; \ -\ Says Server A \ -\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, \ -\ Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs; \ -\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \ -\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \ -\ K ~: analz (sees lost C evs)"; + "!!evs. [| C ~: {A,B,Server}; \ +\ Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, \ +\ Crypt (shrK B) {|Agent A, Key K|}|} \ +\ : set_of_list evs; \ +\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : yahalom lost |] \ +\ ==> Key K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); @@ -374,7 +311,7 @@ \ B ~: lost; evs : yahalom lost |] \ \ ==> EX NA NB. Says Server A \ \ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ +\ Nonce NA, Nonce NB|}, \ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs"; by (etac rev_mp 1); @@ -384,40 +321,8 @@ qed "B_trusts_YM4_shrK"; -(*** General properties of nonces ***) - -goal thy "!!evs. evs : yahalom lost ==> \ -\ length evs <= i --> \ -\ Nonce (newN i) ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); -by (REPEAT_FIRST (fast_tac (!claset - addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_nonces_not_seen"; -Addsimps [new_nonces_not_seen]; - -(*Variant: old messages must contain old nonces!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN i) : parts {X}; \ -\ evs : yahalom lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_nonces"; - - (** The Nonce NB uniquely identifies B's message. **) -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); - goal thy "!!evs. evs : yahalom lost ==> \ \ EX NA' A' B'. ALL NA A B. \ @@ -427,14 +332,15 @@ (*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*) by (REPEAT (etac exE 2) THEN best_tac (!claset addSIs [exI] - addDs [impOfSubs Fake_parts_insert] - addss (!simpset)) 2); + addDs [impOfSubs Fake_parts_insert] + addss (!simpset)) 2); (*Base case*) by (fast_tac (!claset addss (!simpset)) 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); (*YM2: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NB = ?y" 1); -by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1); +by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1)); +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); val lemma = result(); goal thy @@ -447,16 +353,6 @@ by (prove_unique_tac lemma 1); qed "unique_NB"; -(*OLD VERSION -fun lost_tac s = - case_tac ("(" ^ s ^ ") : lost") THEN' - SELECT_GOAL - (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN - REPEAT_DETERM (etac MPair_analz 1) THEN - dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN - assume_tac 1 THEN Fast_tac 1); -*) - fun lost_tac s = case_tac ("(" ^ s ^ ") : lost") THEN' SELECT_GOAL @@ -502,7 +398,6 @@ by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj] addSIs [parts_insertI] addSEs partsEs - addEs [Says_imp_old_nonces RS less_irrefl] addss (!simpset)) 1); val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE); @@ -518,8 +413,8 @@ \ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ \ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \ \ (EX A B NA. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ +\ {|Crypt (shrK A) {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|}, \ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs)"; by (etac yahalom.induct 1); @@ -602,81 +497,97 @@ val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD; -fun grind_tac i = - SELECT_GOAL - (REPEAT_FIRST - (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE' - assume_tac ORELSE' - depth_tac (!claset delrules [conjI] - addSIs [exI, analz_insertI, - impOfSubs (Un_upper2 RS analz_mono)]) 2)) i; (*The only nonces that can be found with the help of session keys are those distributed as nonce NB by the Server. The form of the theorem - recalls analz_image_newK, but it is much more complicated.*) + recalls analz_image_freshK, but it is much more complicated.*) + +(*As with analz_image_freshK, we take some pains to express the property + as a logical equivalence so that the simplifier can apply it.*) +goal thy + "!!evs. P --> (X : analz (G Un H)) --> (X : analz H) ==> \ +\ P --> (X : analz (G Un H)) = (X : analz H)"; +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); +qed "Nonce_secrecy_lemma"; + goal thy - "!!evs. evs : yahalom lost ==> \ -\ ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \ -\ (EX K: newK``E. EX A B na X. \ -\ Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ -\ : set_of_list evs) | Nonce NB : analz (sees lost Spy evs)"; + "!!evs. evs : yahalom lost ==> \ +\ (ALL KK. KK <= Compl (range shrK) --> \ +\ (ALL K: KK. ALL A B na X. \ +\ Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ +\ ~: set_of_list evs) --> \ +\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (Nonce NB : analz (sees lost Spy evs)))"; by (etac yahalom.induct 1); by analz_Fake_tac; +by (REPEAT_FIRST (resolve_tac [impI RS allI])); +by (REPEAT_FIRST (rtac Nonce_secrecy_lemma )); +by (rtac ccontr 7); +by (subgoal_tac "ALL A B na X. \ +\ Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ +\ ~: set_of_list evsa" 7); +by (eres_inst_tac [("P","?PP-->?QQ")] notE 7); +by (subgoal_tac "ALL A B na X. \ +\ Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \ +\ ~: set_of_list evsa" 5); by (ALLGOALS (*22 seconds*) (asm_simp_tac - (!simpset addsimps ([not_parts_not_analz, analz_image_newK, - insert_Key_singleton, insert_Key_image] - @ pushes) - setloop split_tac [expand_if]))); + (analz_image_freshK_ss addsimps + ([all_conj_distrib, + not_parts_not_analz, analz_image_freshK] + @ pushes @ ball_simps)))); (*Base*) by (fast_tac (!claset addss (!simpset)) 1); -(*Fake*) (** LEVEL 4 **) +(*Fake*) (** LEVEL 10 **) by (spy_analz_tac 1); -(*YM1-YM3*) (*24 seconds*) -by (EVERY (map grind_tac [3,2,1])); +(*YM3*) +by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); (*Oops*) -by (Full_simp_tac 2); -by (simp_tac (!simpset addsimps [insert_Key_image]) 2); -by (grind_tac 2); -by (fast_tac (!claset delrules [bexI] - addDs [unique_session_keys] +(*20 secs*) +by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys] addss (!simpset)) 2); (*YM4*) -(** LEVEL 10 **) -by (rtac (impI RS allI) 1); +(** LEVEL 13 **) +by (REPEAT (resolve_tac [impI, allI] 1)); by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1); +by (stac insert_commute 1); by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1); -by (asm_simp_tac (!simpset addsimps [analz_image_newK] - setloop split_tac [expand_if]) 1); -(** LEVEL 14 **) -by (grind_tac 1); -by (REPEAT (dtac not_analz_insert 1)); +by (asm_simp_tac (analz_image_freshK_ss + addsimps [analz_insertI, analz_image_freshK]) 1); +by (step_tac (!claset addSDs [not_analz_insert]) 1); by (lost_tac "A" 1); +(** LEVEL 20 **) by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 THEN REPEAT (assume_tac 1)); -by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1); -by (fast_tac (!claset delrules [conjI] - addIs [analz_insertI] - addss (!simpset)) 1); -val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard; +by (thin_tac "All ?PP" 1); +by (Fast_tac 1); +qed_spec_mp "Nonce_secrecy"; (*Version required below: if NB can be decrypted using a session key then it was distributed with that key. The more general form above is required for the induction to carry through.*) goal thy - "!!evs. [| Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key (newK i), na, Nonce NB'|}, X|} \ -\ : set_of_list evs; \ -\ Nonce NB : analz (insert (Key (newK i)) (sees lost Spy evs)); \ -\ evs : yahalom lost |] \ -\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'"; -by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1); -by (dtac Nonce_secrecy 1 THEN assume_tac 1); -by (fast_tac (!claset addDs [unique_session_keys] - addss (!simpset)) 1); -val single_Nonce_secrecy = result(); + "!!evs. [| Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \ +\ : set_of_list evs; \ +\ Nonce NB : analz (insert (Key KAB) (sees lost Spy evs)); \ +\ Nonce NB ~: analz (sees lost Spy evs); \ +\ KAB ~: range shrK; evs : yahalom lost |] \ +\ ==> NB = NB'"; +by (rtac ccontr 1); +by (subgoal_tac "ALL A B na X. \ +\ Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \ +\ ~: set_of_list evs" 1); +by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1); +by (asm_simp_tac (analz_image_freshK_ss + addsimps ([Nonce_secrecy] @ ball_simps)) 1); +by (auto_tac (!claset addDs [unique_session_keys], (!simpset))); +qed "single_Nonce_secrecy"; goal thy @@ -691,46 +602,41 @@ by (ALLGOALS (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, - analz_insert_Key_newK] @ pushes) + analz_insert_freshK] @ pushes) setloop split_tac [expand_if]))); by (fast_tac (!claset addSIs [parts_insertI] - addSEs partsEs - addEs [Says_imp_old_nonces RS less_irrefl] + addSEs sees_Spy_partsEs addss (!simpset)) 2); (*Proof of YM2*) (** LEVEL 4 **) -by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); -by (fast_tac (!claset addIs [parts_insertI] - addSEs partsEs - addEs [Says_imp_old_nonces RS less_irrefl] - addss (!simpset)) 3); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2); +by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj, + impOfSubs analz_subset_parts] + addSEs partsEs) 3 2); (*Prove YM3 by showing that no NB can also be an NA*) by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2)); by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2); (*Fake*) by (spy_analz_tac 1); -(*YM4*) (** LEVEL 10 **) +(*YM4*) (** LEVEL 8 **) by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1); by (simp_tac (!simpset setloop split_tac [expand_if]) 1); +(*43 secs??*) by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1); -(** LEVEL 13 **) by (lost_tac "Aa" 1); by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); by (forward_tac [Says_Server_message_form] 3); by (forward_tac [Says_Server_imp_YM2] 4); +(** LEVEL 15 **) by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE]))); -by (Full_simp_tac 1); -by (REPEAT_FIRST hyp_subst_tac); -(** LEVEL 20 **) by (lost_tac "Ba" 1); by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1); by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] addSEs [MPair_parts]) 1); by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); +(** LEVEL 20 **) by (dtac Spy_not_see_encrypted_key 1); by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); by (spy_analz_tac 1); -(*Oops case*) (** LEVEL 27 **) +(*Oops case*) (** LEVEL 23 **) by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1); by (step_tac (!claset delrules [disjE, conjI]) 1); by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); @@ -738,7 +644,7 @@ by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1); by (rtac conjI 1); by (no_nonce_tac 1); -(** LEVEL 34 **) +(** LEVEL 30 **) by (thin_tac "?PP|?QQ" 1); (*subsumption!*) by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1); val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard; @@ -750,16 +656,16 @@ ALL POSSIBLE keys instead of our particular K (though at least the nonces are forced to agree with NA and NB). *) goal thy - "!!evs. [| Says B Server \ + "!!evs. [| Says B Server \ \ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ \ : set_of_list evs; \ \ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ \ Crypt K (Nonce NB)|} : set_of_list evs; \ \ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \ -\ ==> Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ +\ ==> Says Server A \ +\ {|Crypt (shrK A) {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|}, \ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs"; by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); @@ -771,4 +677,3 @@ by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1); qed "B_trusts_YM4"; - diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Yahalom.thy Fri Jan 17 12:49:31 1997 +0100 @@ -26,30 +26,26 @@ ==> Says Spy B X # evs : yahalom lost" (*Alice initiates a protocol run*) - YM1 "[| evs: yahalom lost; A ~= B |] - ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs - : yahalom lost" + YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |] + ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost" (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field.*) - YM2 "[| evs: yahalom lost; B ~= Server; + YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs; Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] ==> Says B Server - {|Agent B, - Crypt (shrK B) - {|Agent A, Nonce NA, Nonce (newN(length evs))|}|} - # evs : yahalom lost" + {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} + # evs : yahalom lost" (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob.*) - YM3 "[| evs: yahalom lost; A ~= Server; + YM3 "[| evs: yahalom lost; A ~= Server; Key KAB ~: used evs; Says B' Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} : set_of_list evs |] ==> Says Server A - {|Crypt (shrK A) {|Agent B, Key (newK(length evs)), - Nonce NA, Nonce NB|}, - Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|} + {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key KAB|}|} # evs : yahalom lost" (*Alice receives the Server's (?) message, checks her Nonce, and diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Fri Jan 17 12:49:31 1997 +0100 @@ -24,9 +24,9 @@ \ ==> EX X NB K. EX evs: yahalom lost. \ \ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2); -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); -by (ALLGOALS Fast_tac); +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS + yahalom.YM4) 2); +by possibility_tac; result(); @@ -91,87 +91,45 @@ (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) -(*Spy never sees another agent's shared key! (unless it is leaked at start)*) +(*Spy never sees another agent's shared key! (unless it's lost at start)*) goal thy - "!!evs. [| evs : yahalom lost; A ~: lost |] \ -\ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; + "!!evs. evs : yahalom lost \ +\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; by (parts_induct_tac 1); by (Auto_tac()); -qed "Spy_not_see_shrK"; - -bind_thm ("Spy_not_analz_shrK", - [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); - -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; +qed "Spy_see_shrK"; +Addsimps [Spy_see_shrK]; -(*We go to some trouble to preserve R in the 3rd and 4th subgoals - As usual fast_tac cannot be used because it uses the equalities too soon*) -val major::prems = -goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \ -\ evs : yahalom lost; \ -\ A:lost ==> R \ -\ |] ==> R"; -by (rtac ccontr 1); -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); -by (swap_res_tac prems 2); -by (ALLGOALS (fast_tac (!claset addIs prems))); -qed "Spy_see_shrK_E"; +goal thy + "!!evs. evs : yahalom lost \ +\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_shrK"; +Addsimps [Spy_analz_shrK]; -bind_thm ("Spy_analz_shrK_E", - analz_subset_parts RS subsetD RS Spy_see_shrK_E); +goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ +\ evs : yahalom lost |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +qed "Spy_see_shrK_D"; -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; -(*** Future keys can't be seen or used! ***) - -(*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!i. evs : yahalom lost ==> \ -\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)"; +(*Nobody can have used non-existent keys!*) +goal thy "!!evs. evs : yahalom lost ==> \ +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -qed_spec_mp "new_keys_not_seen"; -Addsimps [new_keys_not_seen]; - -(*Variant: old messages must contain old keys!*) -goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK i) : parts {X}; \ -\ evs : yahalom lost \ -\ |] ==> i < length evs"; -by (rtac ccontr 1); -by (dtac leI 1); -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] - addIs [impOfSubs parts_mono]) 1); -qed "Says_imp_old_keys"; - - -(*Nobody can have USED keys that will be generated in the future. - ...very like new_keys_not_seen*) -goal thy "!!i. evs : yahalom lost ==> \ -\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))"; -by (parts_induct_tac 1); -by (dtac YM4_Key_parts_sees_Spy 5); -(*YM1, YM2 and YM3*) -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); -(*Fake and Oops: these messages send unknown (X) components*) -by (EVERY - (map (fast_tac - (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] - addss (!simpset))) [3,1])); -(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*) -by (fast_tac - (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addEs [new_keys_not_seen RSN(2,rev_notE)] - addDs [Suc_leD]) 1); +(*YM4: Key K is not fresh!*) +by (fast_tac (!claset addSEs sees_Spy_partsEs) 3); +(*YM3*) +by (fast_tac (!claset addss (!simpset)) 2); +(*Fake*) +by (best_tac + (!claset addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono)] + addss (!simpset)) 1); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -184,10 +142,10 @@ (*Describes the form of K when the Server sends this message. Useful for Oops as well as main secrecy property.*) goal thy - "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \ + "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \ \ : set_of_list evs; \ \ evs : yahalom lost |] \ -\ ==> (EX i. K = Key(newK i)) & A ~= B"; +\ ==> K ~: range shrK & A ~= B"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -198,14 +156,14 @@ val analz_Fake_tac = dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN - assume_tac 7 THEN Full_simp_tac 7 THEN - REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7); + assume_tac 7 THEN + REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -216,30 +174,26 @@ goal thy "!!evs. evs : yahalom lost ==> \ -\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ -\ (K : newK``E | Key K : analz (sees lost Spy evs))"; +\ ALL K KK. KK <= Compl (range shrK) --> \ +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ +\ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac yahalom.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 11 secs*) - (asm_simp_tac - (!simpset addsimps [Un_assoc RS sym, - insert_Key_singleton, insert_Key_image, pushKey_newK] - setloop split_tac [expand_if]))); +by (REPEAT_FIRST (resolve_tac [allI, impI])); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); +(*Base*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); (*YM4, Fake*) -by (EVERY (map spy_analz_tac [4, 2])); -(*Oops, YM3, Base*) -by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -qed_spec_mp "analz_image_newK"; +by (REPEAT (spy_analz_tac 1)); +qed_spec_mp "analz_image_freshK"; goal thy - "!!evs. evs : yahalom lost ==> \ -\ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \ -\ (K = newK i | Key K : analz (sees lost Spy 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"; + "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \ +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ +\ (K = KAB | Key K : analz (sees lost Spy evs))"; +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); +qed "analz_insert_freshK"; (*** The Key K uniquely identifies the Server's message. **) @@ -256,8 +210,8 @@ (*Remaining case: YM3*) by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -(*...we assume X is a very new message, and handle this case by contradiction*) -by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] +(*...we assume X is a recent message and handle this case by contradiction*) +by (fast_tac (!claset addSEs sees_Spy_partsEs delrules [conjI] (*prevent split-up into 4 subgoals*) addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); @@ -290,12 +244,13 @@ by analz_Fake_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] + (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] setloop split_tac [expand_if]))); (*YM3*) -by (fast_tac (!claset addIs [parts_insertI] - addEs [Says_imp_old_keys RS less_irrefl] - addss (!simpset)) 2); +by (fast_tac (!claset delrules [impCE] + addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts] + addss (!simpset addsimps [parts_insert2])) 2); (*OR4, Fake*) by (REPEAT_FIRST spy_analz_tac); (*Oops*) @@ -308,12 +263,12 @@ (*Final version: Server's message in the most abstract form*) goal thy "!!evs. [| Says Server A \ -\ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \ -\ Crypt (shrK B) {|NB, K, Agent A|}|} \ +\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \ +\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ \ : set_of_list evs; \ -\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \ +\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : yahalom lost |] \ -\ ==> K ~: analz (sees lost Spy evs)"; +\ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -322,12 +277,12 @@ goal thy "!!evs. [| C ~: {A,B,Server}; \ \ Says Server A \ -\ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \ -\ Crypt (shrK B) {|NB, K, Agent A|}|} \ +\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \ +\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ \ : set_of_list evs; \ -\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \ +\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : yahalom lost |] \ -\ ==> K ~: analz (sees lost C evs)"; +\ ==> Key K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Fri Jan 17 11:50:09 1997 +0100 +++ b/src/HOL/Auth/Yahalom2.thy Fri Jan 17 12:49:31 1997 +0100 @@ -30,26 +30,26 @@ ==> Says Spy B X # evs : yahalom lost" (*Alice initiates a protocol run*) - YM1 "[| evs: yahalom lost; A ~= B |] - ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost" + YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |] + ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost" (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field.*) - YM2 "[| evs: yahalom lost; B ~= Server; + YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs; Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] - ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|} - # evs : yahalom lost" + ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs + : yahalom lost" (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob. Fields are reversed in the 2nd packet to prevent attacks.*) - YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; + YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs; Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set_of_list evs |] ==> Says Server A {|Nonce NB, - Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|}, - Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|} + Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|}, + Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} # evs : yahalom lost" (*Alice receives the Server's (?) message, checks her Nonce, and