# HG changeset patch # User paulson # Date 850993119 -3600 # Node ID ce85a2aafc7a56ed431388b15566ab81ad1a38a6 # Parent 3ad2493fa0e0364e198ca95c767dfbcac7b0733c Extensive tidying and simplification, largely stemming from changing newN and newK to take an integer argument diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/NS_Public.ML Thu Dec 19 11:58:39 1996 +0100 @@ -84,9 +84,9 @@ (*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : ns_public ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +goal thy "!!evs. evs : ns_public ==> \ +\ length evs <= i --> \ +\ Nonce (newN i) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs @@ -104,8 +104,8 @@ fun analz_induct_tac i = etac ns_public.induct i THEN ALLGOALS (asm_simp_tac - (!simpset addsimps ([not_parts_not_analz] @ pushes) - setloop split_tac [expand_if])); + (!simpset addsimps [not_parts_not_analz] + setloop split_tac [expand_if])); (**** Authenticity properties obtained from NS2 ****) diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/NS_Public.thy --- a/src/HOL/Auth/NS_Public.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/NS_Public.thy Thu Dec 19 11:58:39 1996 +0100 @@ -25,15 +25,16 @@ (*Alice initiates a protocol run, sending a nonce to Bob*) NS1 "[| evs: ns_public; A ~= B |] - ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs - : ns_public" + ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|}) + # evs : ns_public" (*Bob responds to Alice's message with a further nonce*) NS2 "[| evs: ns_public; A ~= B; Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs |] - ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs), Agent B|}) - # evs : ns_public" + ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)), + Agent B|}) + # evs : ns_public" (*Alice proves her existence by sending NB back to Bob.*) NS3 "[| evs: ns_public; A ~= B; diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/NS_Public_Bad.ML --- a/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 19 11:58:39 1996 +0100 @@ -89,9 +89,8 @@ (*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : ns_public ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +goal thy "!!i. evs : ns_public ==> \ +\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs @@ -109,7 +108,7 @@ fun analz_induct_tac i = etac ns_public.induct i THEN ALLGOALS (asm_simp_tac - (!simpset addsimps ([not_parts_not_analz] @ pushes) + (!simpset addsimps [not_parts_not_analz] setloop split_tac [expand_if])); diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Dec 19 11:58:39 1996 +0100 @@ -29,15 +29,15 @@ (*Alice initiates a protocol run, sending a nonce to Bob*) NS1 "[| evs: ns_public; A ~= B |] - ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs - : ns_public" + ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|}) + # evs : ns_public" (*Bob responds to Alice's message with a further nonce*) NS2 "[| evs: ns_public; A ~= B; Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs |] - ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs - : ns_public" + ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs))|}) + # evs : ns_public" (*Alice proves her existence by sending NB back to Bob.*) NS3 "[| evs: ns_public; A ~= B; diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Thu Dec 19 11:58:39 1996 +0100 @@ -111,8 +111,7 @@ (*Nobody can have SEEN keys that will be generated in the future. *) goal thy "!!evs. evs : ns_shared lost ==> \ -\ length evs <= length evs' --> \ -\ Key (newK evs') ~: parts (sees lost Spy evs)"; +\ 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, @@ -124,10 +123,10 @@ (*Variant: old messages must contain old keys!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK evt) : parts {X}; \ -\ evs : ns_shared lost \ -\ |] ==> length evt < length evs"; + "!!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] @@ -139,8 +138,7 @@ (*** Future nonces can't be seen or used! ***) goal thy "!!evs. evs : ns_shared lost ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs @@ -156,8 +154,8 @@ (*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 <= length evs' --> \ -\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; +\ 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])); @@ -189,11 +187,10 @@ (*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 evt: ns_shared lost. \ -\ K = Key(newK evt) & \ -\ X = (Crypt (shrK B) {|K, Agent A|}) & \ -\ K' = shrK A)"; +\ evs : ns_shared lost |] \ +\ ==> (EX i. K = Key(newK i) & \ +\ X = (Crypt (shrK B) {|K, Agent A|}) & \ +\ K' = shrK A)"; by (etac rev_mp 1); by (etac ns_shared.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -222,9 +219,8 @@ 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 evt: ns_shared lost. K = newK evt & \ -\ length evt < length evs & \ -\ X = (Crypt (shrK B) {|Key K, Agent A|})) \ +\ ==> (EX i. K = newK i & i < length evs & \ +\ 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] @@ -242,14 +238,14 @@ 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, bexE, disjE] ORELSE' hyp_subst_tac); + REPEAT_FIRST (eresolve_tac [asm_rl, exE, disjE] ORELSE' hyp_subst_tac); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==> - Key K : analz (sees lost Spy evs) + Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -261,7 +257,7 @@ We require that agents should behave like this subsequently also.*) goal thy "!!evs. evs : ns_shared lost ==> \ -\ (Crypt (newK evt) X) : parts (sees lost Spy evs) & \ +\ (Crypt (newK i) 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; @@ -285,23 +281,22 @@ by (etac ns_shared.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS +by (ALLGOALS (*Takes 18 secs*) (asm_simp_tac - (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] - @ pushes) + (!simpset addsimps [Un_assoc RS sym, + insert_Key_singleton, insert_Key_image, pushKey_newK] setloop split_tac [expand_if]))); -(*NS3, Fake*) +(*NS4, Fake*) by (EVERY (map spy_analz_tac [5,2])); +(*NS3, NS2, Base*) by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); -(*NS3, NS2, Base*) -by (REPEAT (Fast_tac 3)); qed_spec_mp "analz_image_newK"; goal thy "!!evs. evs : ns_shared lost ==> \ -\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ -\ (K = newK evt | Key K : analz (sees lost Spy evs))"; +\ 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); @@ -312,8 +307,8 @@ with a secure key **) goal thy - "!!evs. evs : ns_shared lost ==> \ -\ EX A' NA' B' X'. ALL A NA B X. \ + "!!evs. evs : ns_shared lost ==> \ +\ EX A' NA' B' X'. ALL A NA B X. \ \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ \ : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'"; by (etac ns_shared.induct 1); @@ -339,12 +334,7 @@ \ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \ \ : set_of_list evs; \ \ evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'"; -by (dtac lemma 1); -by (REPEAT (etac exE 1)); -(*Duplicate the assumption*) -by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1); -by (fast_tac (!claset addSDs [ spec] - delrules [conjI] addss (!simpset)) 1); +by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -369,14 +359,14 @@ by (fast_tac (!claset addIs [parts_insertI] addEs [Says_imp_old_keys RS less_irrefl] addss (!simpset)) 2); -(*OR4, OR2, Fake*) -by (REPEAT_FIRST spy_analz_tac); -(*NS3 and Oops subcases*) (**LEVEL 7 **) +(*NS4, Fake*) +by (EVERY (map spy_analz_tac [3,1])); +(*NS3 and Oops subcases*) (**LEVEL 5 **) by (step_tac (!claset delrules [impCE]) 1); by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); by (etac conjE 2); by (mp_tac 2); -(**LEVEL 11 **) +(**LEVEL 9 **) by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 2); by (assume_tac 3); by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2); @@ -460,7 +450,7 @@ by (Fast_tac 2); by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); (*Contradiction from the assumption - Crypt (newK evsa) (Nonce NB) : parts (sees lost Spy evsa) *) + Crypt (newK(length evsa)) (Nonce NB) : parts (sees lost Spy evsa) *) by (dtac Crypt_imp_invKey_keysFor 1); (**LEVEL 10**) by (Asm_full_simp_tac 1); diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.thy Thu Dec 19 11:58:39 1996 +0100 @@ -27,8 +27,8 @@ (*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 evs)|} # evs - : ns_shared lost" + ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|} + # evs : ns_shared lost" (*Server's response to Alice's message. !! It may respond more than once to A's request !! @@ -36,9 +36,10 @@ the sender field.*) NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; 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 evs), - (Crypt (shrK B) {|Key (newK evs), Agent A|})|}) + ==> Says Server A + (Crypt (shrK A) + {|Nonce NA, Agent B, Key (newK(length evs)), + (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) # evs : ns_shared lost" (*We can't assume S=Server. Agent A "remembers" her nonce. @@ -53,7 +54,8 @@ from, but responds to A because she is mentioned inside.*) NS4 "[| evs: ns_shared lost; A ~= B; Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |] - ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost" + ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs + : ns_shared lost" (*Alice responds with Nonce NB if she has seen the key before. Maybe should somehow check Nonce NA again. diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Thu Dec 19 11:58:39 1996 +0100 @@ -16,7 +16,6 @@ proof_timing:=true; HOL_quantifiers := false; -Pretty.setdepth 15; (*A "possibility property": there are traces that reach the end*) @@ -132,9 +131,8 @@ (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!evs. evs : otway lost ==> \ -\ length evs <= length evs' --> \ -\ Key (newK evs') ~: parts (sees lost Spy evs)"; +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, @@ -146,10 +144,10 @@ (*Variant: old messages must contain old keys!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK evt) : parts {X}; \ -\ evs : otway lost \ -\ |] ==> length evt < length evs"; + "!!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] @@ -159,9 +157,9 @@ (*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : otway lost ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +goal thy "!!evs. evs : otway 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 @@ -175,10 +173,10 @@ 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 evt) : parts {X}; \ -\ evs : otway lost \ -\ |] ==> length evt < length evs"; +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] @@ -188,9 +186,8 @@ (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) -goal thy "!!evs. evs : otway lost ==> \ -\ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; +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])); @@ -218,9 +215,9 @@ for Oops case.*) goal thy "!!evs. [| Says Server B \ -\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ -\ evs : otway lost |] \ -\ ==> (EX evt: otway lost. K = Key(newK evt)) & \ +\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ +\ evs : otway lost |] \ +\ ==> (EX n. K = Key(newK n)) & \ \ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); @@ -234,14 +231,14 @@ 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 - REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); + 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 evt)) (sees lost Spy evs)) ==> - Key K : analz (sees lost Spy evs) + Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. ****) @@ -257,10 +254,10 @@ by (etac otway.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 12 secs*) +by (ALLGOALS (*Takes 11 secs*) (asm_simp_tac - (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] - @ pushes) + (!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])); @@ -271,8 +268,8 @@ goal thy "!!evs. evs : otway lost ==> \ -\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ -\ (K = newK evt | Key K : analz (sees lost Spy evs))"; +\ 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); @@ -442,8 +439,8 @@ by (etac otway.induct 1); by analz_Fake_tac; by (ALLGOALS - (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, - analz_insert_Key_newK] @ pushes) + (asm_simp_tac (!simpset addsimps [not_parts_not_analz, + analz_insert_Key_newK] setloop split_tac [expand_if]))); (*OR3*) by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/OtwayRees.thy Thu Dec 19 11:58:39 1996 +0100 @@ -29,9 +29,9 @@ (*Alice initiates a protocol run*) OR1 "[| evs: otway lost; A ~= B; B ~= Server |] - ==> Says A B {|Nonce (newN evs), Agent A, Agent B, + ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, Crypt (shrK A) - {|Nonce (newN evs), Agent A, Agent B|} |} + {|Nonce (newN(length evs)), Agent A, Agent B|} |} # evs : otway lost" (*Bob's response to Alice's message. Bob doesn't know who @@ -41,8 +41,8 @@ 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 evs), Agent A, Agent B|}|} + Crypt (shrK B) + {|Nonce NA, Nonce(newN(length evs)), Agent A, Agent B|}|} # evs : otway lost" (*The Server receives Bob's message and checks that the three NAs @@ -56,8 +56,8 @@ : set_of_list evs |] ==> Says Server B {|Nonce NA, - Crypt (shrK A) {|Nonce NA, Key (newK evs)|}, - Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|} + Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|}, + Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|} # evs : otway lost" (*Bob receives the Server's (?) message and compares the Nonces with diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Dec 19 11:58:39 1996 +0100 @@ -120,9 +120,8 @@ (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!evs. evs : otway lost ==> \ -\ length evs <= length evs' --> \ -\ Key (newK evs') ~: parts (sees lost Spy evs)"; +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, @@ -134,10 +133,10 @@ (*Variant: old messages must contain old keys!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK evt) : parts {X}; \ -\ evs : otway lost \ -\ |] ==> length evt < length evs"; + "!!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] @@ -147,9 +146,8 @@ (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) -goal thy "!!evs. evs : otway lost ==> \ -\ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; +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 @@ -180,9 +178,8 @@ \ {|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 evt: otway lost. K = Key(newK evt)) & \ -\ (EX i. NA = Nonce i) & \ -\ (EX j. NB = Nonce j)"; +\ ==> (EX n. K = Key(newK n)) & \ +\ (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)))); @@ -194,14 +191,14 @@ 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 - REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); + 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 evt)) (sees lost Spy evs)) ==> - Key K : analz (sees lost Spy evs) + Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -218,12 +215,11 @@ by (etac otway.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 28 secs*) +by (ALLGOALS (*Takes 18 secs*) (asm_simp_tac - (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] - @ pushes) + (!simpset addsimps [Un_assoc RS sym, + insert_Key_singleton, insert_Key_image, pushKey_newK] setloop split_tac [expand_if]))); -(** LEVEL 5 **) (*OR4, Fake*) by (EVERY (map spy_analz_tac [4,2])); (*Oops, OR3, Base*) @@ -233,8 +229,8 @@ goal thy "!!evs. evs : otway lost ==> \ -\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ -\ (K = newK evt | Key K : analz (sees lost Spy evs))"; +\ 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); @@ -333,8 +329,8 @@ by (etac otway.induct 1); by analz_Fake_tac; by (ALLGOALS - (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, - analz_insert_Key_newK] @ pushes) + (asm_simp_tac (!simpset addsimps [not_parts_not_analz, + analz_insert_Key_newK] setloop split_tac [expand_if]))); (*OR3*) by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Dec 19 11:58:39 1996 +0100 @@ -29,14 +29,15 @@ (*Alice initiates a protocol run*) OR1 "[| evs: otway lost; A ~= B; B ~= Server |] - ==> Says A B {|Agent A, Agent B, Nonce (newN evs)|} + ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|} # 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 evs)|} + ==> Says B Server {|Agent A, Agent B, Nonce NA, + Nonce (newN(length evs))|} # evs : otway lost" (*The Server receives Bob's message. Then he sends a new @@ -45,8 +46,10 @@ 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 evs)|}, - Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|} + {|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))|}|} # evs : otway lost" (*Bob receives the Server's (?) message and compares the Nonces with diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Dec 19 11:58:39 1996 +0100 @@ -132,9 +132,8 @@ (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!evs. evs : otway ==> \ -\ length evs <= length evs' --> \ -\ Key (newK evs') ~: parts (sees lost Spy evs)"; +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, @@ -146,10 +145,10 @@ (*Variant: old messages must contain old keys!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK evt) : parts {X}; \ -\ evs : otway \ -\ |] ==> length evt < length evs"; + "!!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] @@ -159,9 +158,8 @@ (*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : otway ==> \ -\ length evs <= length evs' --> \ -\ Nonce (newN evs') ~: parts (sees lost Spy evs)"; +goal thy "!!i. evs : otway ==> \ +\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs @@ -175,10 +173,10 @@ (*Variant: old messages must contain old nonces!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN evt) : parts {X}; \ -\ evs : otway \ -\ |] ==> length evt < length evs"; + "!!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] @@ -188,9 +186,8 @@ (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) -goal thy "!!evs. evs : otway ==> \ -\ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; +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])); @@ -219,8 +216,8 @@ goal thy "!!evs. [| Says Server B \ \ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \ -\ evs : otway |] \ -\ ==> (EX evt: otway. K = Key(newK evt)) & \ +\ evs : otway |] \ +\ ==> (EX n. K = Key(newK n)) & \ \ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); @@ -234,14 +231,14 @@ dtac OR4_analz_sees_Spy 6 THEN forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN Full_simp_tac 7 THEN - REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); + 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 evt)) (sees lost Spy evs)) ==> - Key K : analz (sees lost Spy evs) + Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -267,12 +264,11 @@ by (etac otway.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (ares_tac [allI, lemma])); -by (ALLGOALS +by (ALLGOALS (*Takes 18 secs*) (asm_simp_tac - (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] - @ pushes) + (!simpset addsimps [Un_assoc RS sym, + insert_Key_singleton, insert_Key_image, pushKey_newK] setloop split_tac [expand_if]))); -(** LEVEL 7 **) (*OR4, OR2, Fake*) by (EVERY (map spy_analz_tac [5,3,2])); (*Oops, OR3, Base*) @@ -282,8 +278,8 @@ goal thy "!!evs. evs : otway ==> \ -\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ -\ (K = newK evt | Key K : analz (sees lost Spy evs))"; +\ 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); @@ -293,7 +289,7 @@ (*** The Key K uniquely identifies the Server's message. **) goal thy - "!!evs. evs : otway ==> \ + "!!evs. evs : otway ==> \ \ EX B' NA' NB' X'. ALL B NA NB X. \ \ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \ \ B=B' & NA=NA' & NB=NB' & X=X'"; @@ -332,8 +328,8 @@ by (etac otway.induct 1); by analz_Fake_tac; by (ALLGOALS - (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, - analz_insert_Key_newK] @ pushes) + (asm_simp_tac (!simpset addsimps [not_parts_not_analz, + analz_insert_Key_newK] setloop split_tac [expand_if]))); (*OR3*) by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Dec 19 11:58:39 1996 +0100 @@ -28,9 +28,9 @@ (*Alice initiates a protocol run*) OR1 "[| evs: otway; A ~= B; B ~= Server |] - ==> Says A B {|Nonce (newN evs), Agent A, Agent B, + ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, Crypt (shrK A) - {|Nonce (newN evs), Agent A, Agent B|} |} + {|Nonce (newN(length evs)), Agent A, Agent B|} |} # evs : otway" (*Bob's response to Alice's message. Bob doesn't know who @@ -39,7 +39,7 @@ OR2 "[| evs: otway; B ~= Server; 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 evs), + {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)), Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} # evs : otway" @@ -55,8 +55,8 @@ : set_of_list evs |] ==> Says Server B {|Nonce NA, - Crypt (shrK A) {|Nonce NA, Key (newK evs)|}, - Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|} + Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|}, + Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|} # evs : otway" (*Bob receives the Server's (?) message and compares the Nonces with diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Public.ML --- a/src/HOL/Auth/Public.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Public.ML Thu Dec 19 11:58:39 1996 +0100 @@ -27,15 +27,14 @@ (*** Basic properties of pubK ***) (*Injectiveness and freshness of new keys and nonces*) -AddIffs [inj_pubK RS inj_eq]; -AddSDs [newN_length]; +AddIffs [inj_pubK RS inj_eq, inj_newN RS inj_eq]; (** Rewrites should not refer to initState(Friend i) -- not in normal form! **) Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym]; -goal thy "Nonce (newN evs) ~: parts (initState lost B)"; +goal thy "Nonce (newN i) ~: parts (initState lost B)"; by (agent.induct_tac "B" 1); by (Auto_tac ()); qed "newN_notin_initState"; diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Public.thy Thu Dec 19 11:58:39 1996 +0100 @@ -50,17 +50,16 @@ sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" -(*Agents generate "random" nonces. These are uniquely determined by - the length of their argument, a trace.*) +(*Agents generate "random" nonces, uniquely determined by their argument.*) consts - newN :: "event list => nat" + newN :: nat => nat rules (*Public keys are disjoint, and never clash with private keys*) - inj_pubK "inj pubK" - priK_neq_pubK "priK A ~= pubK B" + inj_pubK "inj pubK" + priK_neq_pubK "priK A ~= pubK B" - newN_length "(newN evs = newN evt) ==> (length evs = length evt)" + inj_newN "inj newN" end diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Recur.ML Thu Dec 19 11:58:39 1996 +0100 @@ -27,8 +27,8 @@ \ Agent Server|} \ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (recur.Nil RS recur.NA1 RS - (respond.One RSN (4,recur.NA3))) 2); +by (rtac (recur.Nil RS recur.RA1 RS + (respond.One RSN (4,recur.RA3))) 2); by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); by (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])); result(); @@ -42,9 +42,9 @@ \ Agent Server|} \ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (recur.Nil RS recur.NA1 RS recur.NA2 RS - (respond.One RS respond.Cons RSN (4,recur.NA3)) RS - recur.NA4) 2); +by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS + (respond.One RS respond.Cons RSN (4,recur.RA3)) RS + recur.RA4) 2); by (REPEAT (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]) THEN @@ -60,9 +60,9 @@ \ Agent Server|} \ \ : set_of_list evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (recur.Nil RS recur.NA1 RS recur.NA2 RS recur.NA2 RS +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.NA3)) RS recur.NA4 RS recur.NA4) 2); + (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); by (REPEAT (*SLOW: 37 seconds*) (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]) THEN @@ -104,30 +104,30 @@ (** For reasoning about the encrypted portion of messages **) -val NA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard; +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 \ \ ==> RA : analz (sees lost Spy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); -qed "NA4_analz_sees_Spy"; +qed "RA4_analz_sees_Spy"; -(*NA2_analz... and NA4_analz... let us treat those cases using the same +(*RA2_analz... and RA4_analz... let us treat those cases using the same argument as for the Fake case. This is possible for most, but not all, - proofs: Fake does not invent new nonces (as in NA2), and of course Fake + proofs: Fake does not invent new nonces (as in RA2), and of course Fake messages originate from the Spy. *) -bind_thm ("NA2_parts_sees_Spy", - NA2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); -bind_thm ("NA4_parts_sees_Spy", - NA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); +bind_thm ("RA2_parts_sees_Spy", + RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); +bind_thm ("RA4_parts_sees_Spy", + RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); (*We instantiate the variable to "lost". Leaving it as a Var makes proofs harder to complete, since simplification does less for us.*) val parts_Fake_tac = let val tac = forw_inst_tac [("lost","lost")] - in tac NA2_parts_sees_Spy 4 THEN + in tac RA2_parts_sees_Spy 4 THEN forward_tac [respond_imp_responses] 5 THEN - tac NA4_parts_sees_Spy 6 + tac RA4_parts_sees_Spy 6 end; (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) @@ -159,10 +159,10 @@ "!!evs. evs : recur lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; by (parts_induct_tac 1); -(*NA2*) +(*RA2*) by (best_tac (!claset addSEs partsEs addSDs [parts_cut] addss (!simpset)) 1); -(*NA3*) +(*RA3*) by (fast_tac (!claset addDs [Key_in_parts_respond] addss (!simpset addsimps [parts_insert_sees])) 1); qed "Spy_see_shrK"; @@ -191,7 +191,7 @@ \ length evs <= i --> \ \ Key (newK2(i,j)) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); -(*NA2*) +(*RA2*) by (best_tac (!claset addSEs partsEs addSDs [parts_cut] addDs [Suc_leD] @@ -201,9 +201,9 @@ impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)) 1); -(*For NA3*) +(*For RA3*) by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2); -(*NA1-NA4*) +(*RA1-RA4*) by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD] addss (!simpset)) 1)); qed_spec_mp "new_keys_not_seen"; @@ -235,7 +235,7 @@ goal thy "!!i. evs : recur lost ==> \ \ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); -(*For NA3*) +(*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] @@ -245,7 +245,7 @@ impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)) 1); -(*NA1, NA2, NA4*) +(*RA1, RA2, RA4*) by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs addEs [leD RS notE] @@ -279,13 +279,13 @@ goal thy "!!i. evs : recur lost ==> \ \ length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -(*NA3*) +(*RA3*) by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD] addss (!simpset addsimps [parts_insert_sees])) 4); -(*NA2*) +(*RA2*) by (fast_tac (!claset addSEs partsEs addDs [Suc_leD] addss (!simpset)) 3); -(*Fake, NA1, NA4*) +(*Fake, RA1, RA4*) by (REPEAT (best_tac (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), @@ -308,14 +308,14 @@ (*For proofs involving analz. We again instantiate the variable to "lost".*) val analz_Fake_tac = - dres_inst_tac [("lost","lost")] NA2_analz_sees_Spy 4 THEN + dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN forward_tac [respond_imp_responses] 5 THEN - dres_inst_tac [("lost","lost")] NA4_analz_sees_Spy 6; + dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6; (** Session keys are not used to encrypt other session keys **) -(*Version for "responses" relation. Handles case NA3 in the theorem below. +(*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 @@ -340,12 +340,12 @@ \ (K : newK``I | Key K : analz (sees lost Spy evs))"; by (etac recur.induct 1); by analz_Fake_tac; -be ssubst 4; (*NA2: DELETE needless definition of PA!*) +be ssubst 4; (*RA2: DELETE needless definition of PA!*) by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma]))); (*Base*) by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); -(*NA4, NA2, Fake*) +(*RA4, RA2, Fake*) by (REPEAT (spy_analz_tac 1)); val raw_analz_image_newK = result(); qed_spec_mp "analz_image_newK"; @@ -381,12 +381,12 @@ \ (Nonce (newN i) : parts {X} --> \ \ Hash X ~: parts (sees lost Spy evs))"; be recur.induct 1; -be ssubst 4; (*NA2: DELETE needless definition of PA!*) +be ssubst 4; (*RA2: DELETE needless definition of PA!*) by parts_Fake_tac; -(*NA3 requires a further induction*) +(*RA3 requires a further induction*) be responses.induct 5; by (ALLGOALS Asm_simp_tac); -(*NA2*) +(*RA2*) by (best_tac (!claset addDs [Suc_leD, parts_cut] addEs [leD RS notE, new_nonces_not_seen RSN(2,rev_notE)] @@ -405,7 +405,7 @@ (** The Nonce NA uniquely identifies A's message. - This theorem applies to rounds NA1 and NA2! + This theorem applies to rounds RA1 and RA2! **) goal thy @@ -414,15 +414,15 @@ \ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \ \ : parts (sees lost Spy evs) --> B=B' & P=P'"; be recur.induct 1; -be ssubst 4; (*NA2: DELETE needless definition of PA!*) -(*For better simplification of NA2*) +be ssubst 4; (*RA2: DELETE needless definition of PA!*) +(*For better simplification of RA2*) by (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 4); by parts_Fake_tac; -(*NA3 requires a further induction*) +(*RA3 requires a further induction*) be responses.induct 5; by (ALLGOALS Asm_simp_tac); by (step_tac (!claset addSEs partsEs) 1); -(*NA3: inductive case*) +(*RA3: inductive case*) by (best_tac (!claset addss (!simpset)) 5); (*Fake*) by (best_tac (!claset addSIs [exI] @@ -433,13 +433,13 @@ by (fast_tac (!claset addss (!simpset)) 1); by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); -(*NA1: creation of new Nonce. Move assertion into global context*) +(*RA1: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NA = ?y" 1); by (best_tac (!claset addSIs [exI] addEs [Hash_new_nonces_not_seen] addss (!simpset)) 1); by (best_tac (!claset addss (!simpset)) 1); -(*NA2: creation of new Nonce*) +(*RA2: creation of new Nonce*) by (expand_case_tac "NA = ?y" 1); by (best_tac (!claset addSIs [exI] addDs [parts_cut] @@ -510,7 +510,7 @@ (*The Server does not send such messages. This theorem lets us avoid - assuming B~=Server in NA4.*) + assuming B~=Server in RA4.*) goal thy "!!evs. evs : recur lost \ \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \ @@ -557,7 +557,7 @@ qed "unique_session_keys"; -(** Crucial secrecy property: Spy does not see the keys sent in msg NA3 +(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 Does not in itself guarantee security: an attack could violate the premises, e.g. by having A=Spy **) @@ -614,24 +614,24 @@ \ Key K ~: analz (sees lost Spy evs)"; by (etac recur.induct 1); by analz_Fake_tac; -be ssubst 4; (*NA2: DELETE needless definition of PA!*) +be ssubst 4; (*RA2: DELETE needless definition of PA!*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] setloop split_tac [expand_if]))); -(*NA4*) +(*RA4*) by (spy_analz_tac 4); (*Fake*) by (spy_analz_tac 1); by (step_tac (!claset delrules [impCE]) 1); -(*NA2*) +(*RA2*) by (spy_analz_tac 1); -(*NA3, case 2: K is an old key*) +(*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); -(*NA3, case 1: use lemma previously proved by induction*) +(*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); bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp)); @@ -652,7 +652,7 @@ (**** Authenticity properties for Agents ****) -(*Only NA1 or NA2 can have caused such a part of a message to appear.*) +(*Only RA1 or RA2 can have caused such a part of a message to appear.*) goal thy "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \ \ : parts (sees lost Spy evs); \ @@ -662,9 +662,9 @@ \ : set_of_list evs"; be rev_mp 1; by (parts_induct_tac 1); -(*NA3*) +(*RA3*) by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2); -(*NA2*) +(*RA2*) by ((REPEAT o CHANGED) (*Push in XA*) (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1)); by (best_tac (!claset addSEs partsEs @@ -692,22 +692,22 @@ in a run, then it originated with the Server!*) goal thy "!!evs. [| A ~: lost; A ~= Spy; evs : recur lost |] \ -\ ==> Crypt (shrK A) {|Key K, Agent B, NA|} : parts (sees lost Spy evs) \ +\ ==> Crypt (shrK A) {|Key K, Agent A', NA|} : parts (sees lost Spy evs) \ \ --> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \ \ Agent A, Agent B, NA, P|} \ \ : set_of_list evs \ \ --> (EX C RC. Says Server C RC : set_of_list evs & \ -\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RC})"; +\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC})"; by (parts_induct_tac 1); -(*NA4*) +(*RA4*) by (best_tac (!claset addSEs [MPair_parts] addSDs [Hash_auth_sender] addSIs [disjI2]) 4); -(*NA1: it cannot be a new Nonce, contradiction.*) +(*RA1: it cannot be a new Nonce, contradiction.*) by (fast_tac (!claset delrules [impCE] addSEs [nonce_not_seen_now, MPair_parts] addDs [parts.Body]) 1); -(*NA2: it cannot be a new Nonce, contradiction.*) +(*RA2: it cannot be a new Nonce, contradiction.*) by ((REPEAT o CHANGED) (*Push in XA*) (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1)); by (deepen_tac (!claset delrules [impCE] @@ -715,7 +715,7 @@ addSEs [MPair_parts] addDs [parts_cut, parts.Body] addss (!simpset)) 0 1); -(*NA3*) (** LEVEL 5 **) +(*RA3*) (** LEVEL 5 **) by (REPEAT (safe_step_tac (!claset addSEs [responses_no_Hash_Server] delrules [impCE]) 1)); by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 1); @@ -727,13 +727,13 @@ then the key really did come from the Server!*) goal thy "!!evs. [| Says B' A RA : set_of_list evs; \ -\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RA}; \ +\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \ \ Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \ \ Agent A, Agent B, NA, P|} \ \ : set_of_list evs; \ \ A ~: lost; A ~= Spy; evs : recur lost |] \ \ ==> EX C RC. Says Server C RC : set_of_list evs & \ -\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RC}"; +\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC}"; by (best_tac (!claset addSIs [Crypt_imp_Server_msg] addDs [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)] addss (!simpset)) 1); @@ -744,12 +744,12 @@ then the only other agent who knows the key is B.*) goal thy "!!evs. [| Says B' A RA : set_of_list evs; \ -\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RA}; \ +\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \ \ Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \ \ Agent A, Agent B, NA, P|} \ \ : set_of_list evs; \ -\ C ~: {A,B,Server}; \ -\ A ~: lost; B ~: lost; A ~= Spy; evs : recur lost |] \ +\ C ~: {A,A',Server}; \ +\ A ~: lost; A' ~: lost; A ~= Spy; evs : recur lost |] \ \ ==> Key K ~: analz (sees lost C evs)"; by (dtac Agent_trust 1 THEN REPEAT_FIRST assume_tac); by (fast_tac (!claset addSEs [Agent_not_see_encrypted_key RSN(2,rev_notE)]) 1); diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Recur.thy Thu Dec 19 11:58:39 1996 +0100 @@ -77,7 +77,7 @@ (*Alice initiates a protocol run. "Agent Server" is just a placeholder, to terminate the nesting.*) - NA1 "[| evs: recur lost; A ~= B; A ~= Server; + RA1 "[| evs: recur lost; A ~= B; A ~= Server; MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|] ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost" @@ -85,7 +85,7 @@ XA should be the Hash of the remaining components with KA, but Bob cannot check that. P is the previous recur message from Alice's caller.*) - NA2 "[| evs: recur lost; B ~= C; B ~= Server; + RA2 "[| evs: recur lost; B ~= C; B ~= Server; Says A' B PA : set_of_list evs; PA = {|XA, Agent A, Agent B, Nonce NA, P|}; MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |] @@ -93,14 +93,14 @@ (*The Server receives and decodes Bob's message. Then he generates a new session key and a response.*) - NA3 "[| evs: recur lost; B ~= Server; + RA3 "[| evs: recur lost; B ~= Server; Says B' Server PB : set_of_list evs; (0,PB,RB) : respond (length 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.*) - NA4 "[| evs: recur lost; A ~= B; + RA4 "[| evs: recur lost; A ~= B; Says C' B {|Agent B, Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, Agent B, diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Shared.ML Thu Dec 19 11:58:39 1996 +0100 @@ -26,62 +26,35 @@ (*** Basic properties of shrK and newK ***) -goalw thy [newN_def] "!!evs. newN evs = newN evt ==> length evs = length evt"; -by (fast_tac (!claset addSDs [inj_random RS injD]) 1); -qed "newN_length"; - -goalw thy [newK_def] "!!evs. newK evs = newK evt ==> length evs = length evt"; -by (fast_tac (!claset addSDs [inj_random RS injD]) 1); -qed "newK_length"; - -goalw thy [newK_def] "newK evs ~= shrK A"; -by (rtac random_neq_shrK 1); -qed "newK_neq_shrK"; - -goalw thy [newK_def] "isSymKey (newK evs)"; -by (rtac isSym_random 1); -qed "isSym_newK"; +(*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]; (* invKey (shrK A) = shrK A *) bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK); -(* invKey (random x) = random x *) -bind_thm ("invKey_random", rewrite_rule [isSymKey_def] isSym_random); - -(* invKey (newK evs) = newK evs *) +(* invKey (newK i) = newK i *) bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); -Addsimps [invKey_shrK, invKey_random, invKey_newK]; +Addsimps [invKey_shrK, invKey_newK]; -goal thy "!!K. random x = invKey K ==> random x = K"; -by (rtac (invKey_eq RS iffD1) 1); -by (Simp_tac 1); -val random_invKey = result(); - -AddSDs [random_invKey, sym RS random_invKey]; - -goal thy "!!K. newK evs = invKey K ==> newK evs = K"; +goal thy "!!K. newK i = invKey K ==> newK i = K"; by (rtac (invKey_eq RS iffD1) 1); by (Simp_tac 1); val newK_invKey = result(); AddSDs [newK_invKey, sym RS newK_invKey]; -(*Injectiveness and freshness of new keys and nonces*) -AddIffs [inj_shrK RS inj_eq, inj_random RS inj_eq]; -AddSDs [newN_length, newK_length]; - -Addsimps [random_neq_shrK, random_neq_shrK RS not_sym, - newK_neq_shrK, newK_neq_shrK RS not_sym]; +Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym]; (** Rewrites should not refer to initState(Friend i) -- not in normal form! **) -goal thy "Key (newK evs) ~: parts (initState lost B)"; +goal thy "Key (newK i) ~: parts (initState lost B)"; by (agent.induct_tac "B" 1); by (Auto_tac ()); qed "newK_notin_initState"; -goal thy "Nonce (newN evs) ~: parts (initState lost B)"; +goal thy "Nonce (newN i) ~: parts (initState lost B)"; by (agent.induct_tac "B" 1); by (Auto_tac ()); qed "newN_notin_initState"; @@ -105,12 +78,6 @@ qed "shrK_notin_image_newK"; Addsimps [shrK_notin_image_newK]; -goal thy "shrK A ~: random``E"; -by (agent.induct_tac "A" 1); -by (Auto_tac ()); -qed "shrK_notin_image_random"; -Addsimps [shrK_notin_image_random]; - (*** Function "sees" ***) diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Shared.thy Thu Dec 19 11:58:39 1996 +0100 @@ -44,24 +44,25 @@ sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" -(*Agents generate "random" numbers for use as symmetric keys, as well as - nonces.*) +(*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 + in one protocol round. A typical candidate for npair(i,j) is + 2^j(2i+1) +*) consts - random :: "nat*nat => nat" - -constdefs - newN :: event list => nat - "newN evs == random (length evs, 0)" - - newK :: event list => nat - "newK evs == random (length evs, 1)" + nPair :: "nat*nat => nat" + newN :: "nat => nat" + newK :: "nat => key" rules inj_shrK "inj shrK" - inj_random "inj random" + inj_nPair "inj nPair" + inj_newN "inj newN" + inj_newK "inj newK" - random_neq_shrK "random ij ~= shrK A" - isSym_random "isSymKey (random ij)" + newK_neq_shrK "newK i ~= shrK A" + isSym_newK "isSymKey (newK i)" end diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/WooLam.ML Thu Dec 19 11:58:39 1996 +0100 @@ -96,9 +96,8 @@ (*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : woolam ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +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 diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/WooLam.thy --- a/src/HOL/Auth/WooLam.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/WooLam.thy Thu Dec 19 11:58:39 1996 +0100 @@ -37,7 +37,7 @@ (*Bob responds to Alice's message with a challenge.*) WL2 "[| evs: woolam; A ~= B; Says A' B (Agent A) : set_of_list evs |] - ==> Says B A (Nonce (newN evs)) # evs : woolam" + ==> Says B A (Nonce (newN(length evs))) # evs : woolam" (*Alice responds to Bob's challenge by encrypting NB with her key. B is *not* properly determined -- Alice essentially broadcasts diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Yahalom.ML Thu Dec 19 11:58:39 1996 +0100 @@ -118,9 +118,8 @@ (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!evs. evs : yahalom lost ==> \ -\ length evs <= length evs' --> \ -\ Key (newK evs') ~: parts (sees lost Spy evs)"; +goal thy "!!i. evs : yahalom 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, @@ -132,10 +131,10 @@ (*Variant: old messages must contain old keys!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK evt) : parts {X}; \ -\ evs : yahalom lost \ -\ |] ==> length evt < length evs"; + "!!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] @@ -144,7 +143,7 @@ (*Ready-made for the classical reasoner*) -goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|} \ +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] @@ -155,9 +154,8 @@ (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) -goal thy "!!evs. evs : yahalom lost ==> \ -\ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; +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])); @@ -187,10 +185,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 \ + "!!evs. [| Says Server A \ \ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \ -\ evs : yahalom lost |] \ -\ ==> (EX evt: yahalom lost. K = Key(newK evt))"; +\ evs : yahalom lost |] \ +\ ==> EX i. K = Key(newK i)"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -202,14 +200,14 @@ 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 bexE ORELSE' hyp_subst_tac) 7); + REPEAT ((etac exE ORELSE' hyp_subst_tac) 7); (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==> - Key K : analz (sees lost Spy evs) + Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> + Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -221,7 +219,7 @@ We require that agents should behave like this subsequently also.*) goal thy "!!evs. evs : yahalom lost ==> \ -\ (Crypt (newK evt) X) : parts (sees lost Spy evs) & \ +\ (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; @@ -244,12 +242,11 @@ by (etac yahalom.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS +by (ALLGOALS (*Takes 11 secs*) (asm_simp_tac - (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] - @ pushes) + (!simpset addsimps [Un_assoc RS sym, + insert_Key_singleton, insert_Key_image, pushKey_newK] setloop split_tac [expand_if]))); -(** LEVEL 5 **) (*YM4, Fake*) by (EVERY (map spy_analz_tac [4, 2])); (*Oops, YM3, Base*) @@ -258,8 +255,8 @@ goal thy "!!evs. evs : yahalom lost ==> \ -\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ -\ (K = newK evt | Key K : analz (sees lost Spy evs))"; +\ 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); @@ -295,11 +292,7 @@ \ : set_of_list evs; \ \ evs : yahalom lost |] \ \ ==> A=A' & B=B' & NA=NA' & NB=NB'"; -by (dtac lemma 1); -by (REPEAT (etac exE 1)); -(*Duplicate the assumption*) -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); -by (fast_tac (!claset addSDs [spec]) 1); +by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -331,14 +324,13 @@ 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_Key_newK] setloop split_tac [expand_if]))); (*YM3*) by (Fast_tac 2); (*uses Says_too_new_key*) (*OR4, Fake*) by (REPEAT_FIRST spy_analz_tac); -(*Oops*) (** LEVEL 6 **) +(*Oops*) by (fast_tac (!claset delrules [disjE] addDs [unique_session_keys] addss (!simpset)) 1); @@ -381,8 +373,8 @@ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \ \ B ~: lost; evs : yahalom lost |] \ \ ==> EX NA NB. 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 rev_mp 1); @@ -394,9 +386,9 @@ (*** General properties of nonces ***) -goal thy "!!evs. evs : yahalom lost ==> \ -\ length evs <= length evt --> \ -\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +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 @@ -411,10 +403,10 @@ (*Variant: old messages must contain old nonces!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN evt) : parts {X}; \ -\ evs : yahalom lost \ -\ |] ==> length evt < length evs"; + "!!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] @@ -427,11 +419,19 @@ 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. \ + "!!evs. evs : yahalom lost ==> \ +\ EX NA' A' B'. ALL NA A B. \ \ Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \ \ --> B ~: lost --> NA = NA' & A = A' & B = B'"; -by (parts_induct_tac 1); (*100 seconds??*) -by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); +by (etac yahalom.induct 1 THEN parts_Fake_tac); +(*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); +(*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); @@ -444,11 +444,7 @@ \ : parts (sees lost Spy evs); \ \ evs : yahalom lost; B ~: lost; B' ~: lost |] \ \ ==> NA' = NA & A' = A & B' = B"; -by (dtac lemma 1); -by (REPEAT (etac exE 1)); -(*Duplicate the assumption*) -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); -by (fast_tac (!claset addSDs [spec]) 1); +by (prove_unique_tac lemma 1); qed "unique_NB"; (*OLD VERSION @@ -627,7 +623,7 @@ \ : set_of_list evs) | Nonce NB : analz (sees lost Spy evs)"; by (etac yahalom.induct 1); by analz_Fake_tac; -by (ALLGOALS (*28 seconds*) +by (ALLGOALS (*22 seconds*) (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, analz_image_newK, @@ -638,11 +634,10 @@ by (fast_tac (!claset addss (!simpset)) 1); (*Fake*) (** LEVEL 4 **) by (spy_analz_tac 1); -(*YM1-YM3*) (*29 seconds*) +(*YM1-YM3*) (*24 seconds*) by (EVERY (map grind_tac [3,2,1])); (*Oops*) by (Full_simp_tac 2); -by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2)); by (simp_tac (!simpset addsimps [insert_Key_image]) 2); by (grind_tac 2); by (fast_tac (!claset delrules [bexI] @@ -672,11 +667,11 @@ 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 evt), na, Nonce NB'|}, X|} \ -\ : set_of_list evs; \ -\ Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs)); \ -\ evs : yahalom lost |] \ + "!!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); diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Yahalom.thy Thu Dec 19 11:58:39 1996 +0100 @@ -27,7 +27,8 @@ (*Alice initiates a protocol run*) YM1 "[| evs: yahalom lost; A ~= B |] - ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost" + ==> Says A B {|Agent A, Nonce (newN(length evs))|} # 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.*) @@ -35,7 +36,8 @@ 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 evs)|}|} + Crypt (shrK B) + {|Agent A, Nonce NA, Nonce (newN(length evs))|}|} # evs : yahalom lost" (*The Server receives Bob's message. He responds by sending a @@ -45,9 +47,9 @@ {|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 evs), + {|Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA, Nonce NB|}, - Crypt (shrK B) {|Agent A, Key (newK evs)|}|} + Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|} # evs : yahalom lost" (*Alice receives the Server's (?) message, checks her Nonce, and diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Thu Dec 19 11:58:39 1996 +0100 @@ -126,9 +126,8 @@ (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. *) -goal thy "!!evs. evs : yahalom lost ==> \ -\ length evs <= length evs' --> \ -\ Key (newK evs') ~: parts (sees lost Spy evs)"; +goal thy "!!i. evs : yahalom 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, @@ -141,9 +140,9 @@ (*Variant: old messages must contain old keys!*) goal thy "!!evs. [| Says A B X : set_of_list evs; \ -\ Key (newK evt) : parts {X}; \ +\ Key (newK i) : parts {X}; \ \ evs : yahalom lost \ -\ |] ==> length evt < length evs"; +\ |] ==> i < length evs"; by (rtac ccontr 1); by (dtac leI 1); by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] @@ -153,9 +152,8 @@ (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) -goal thy "!!evs. evs : yahalom lost ==> \ -\ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; +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*) @@ -189,7 +187,7 @@ "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \ \ : set_of_list evs; \ \ evs : yahalom lost |] \ -\ ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B"; +\ ==> (EX i. K = Key(newK i)) & A ~= B"; by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -201,13 +199,13 @@ 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 [bexE,conjE] ORELSE' hyp_subst_tac) 7); + 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 evt)) (sees lost Spy evs)) ==> + Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> Key K : analz (sees lost Spy evs) A more general formula must be proved inductively. @@ -223,10 +221,10 @@ by (etac yahalom.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 26 secs*) +by (ALLGOALS (*Takes 11 secs*) (asm_simp_tac - (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] - @ pushes) + (!simpset addsimps [Un_assoc RS sym, + insert_Key_singleton, insert_Key_image, pushKey_newK] setloop split_tac [expand_if]))); (*YM4, Fake*) by (EVERY (map spy_analz_tac [4, 2])); @@ -236,8 +234,8 @@ goal thy "!!evs. evs : yahalom lost ==> \ -\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ -\ (K = newK evt | Key K : analz (sees lost Spy evs))"; +\ 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); @@ -273,11 +271,7 @@ \ : set_of_list evs; \ \ evs : yahalom lost |] \ \ ==> A=A' & B=B' & NA=NA' & NB=NB'"; -by (dtac lemma 1); -by (REPEAT (etac exE 1)); -(*Duplicate the assumption*) -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); -by (fast_tac (!claset addSDs [spec]) 1); +by (prove_unique_tac lemma 1); qed "unique_session_keys"; @@ -296,8 +290,7 @@ 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_Key_newK] setloop split_tac [expand_if]))); (*YM3*) by (fast_tac (!claset addIs [parts_insertI] diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Yahalom2.thy Thu Dec 19 11:58:39 1996 +0100 @@ -31,13 +31,13 @@ (*Alice initiates a protocol run*) YM1 "[| evs: yahalom lost; A ~= B |] - ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost" + ==> Says A B {|Agent A, Nonce (newN(length evs))|} # 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; Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] - ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|} + ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|} # evs : yahalom lost" (*The Server receives Bob's message. He responds by sending a @@ -48,8 +48,8 @@ : set_of_list evs |] ==> Says Server A {|Nonce NB, - Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|}, - Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|} + Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|}, + Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|} # evs : yahalom lost" (*Alice receives the Server's (?) message, checks her Nonce, and