# HG changeset patch # User paulson # Date 847189252 -3600 # Node ID ad4382e546fccc1f000f575415449255b95979e4 # Parent e650a3f6f6005c19eabff8cbf0119fe990a4900b Simplified new_keys_not_seen, etc.: replaced the union over all agents by the Spy alone. Proofs run faster and they do not have to be set up in terms of a previous lemma. diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Tue Nov 05 11:20:52 1996 +0100 @@ -109,35 +109,23 @@ (*** Future keys can't be seen or used! ***) -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The length comparison, and Union over C, are essential for the - induction! *) -goal thy "!!evs. evs : ns_shared lost ==> \ +(*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') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : ns_shared lost; length evs <= length evs' |] \ -\ ==> Key (newK evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_keys_not_seen"; +qed_spec_mp "new_keys_not_seen"; Addsimps [new_keys_not_seen]; -(*Another variant: old messages must contain old keys!*) +(*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 \ +\ evs : ns_shared lost \ \ |] ==> length evt < length evs"; by (rtac ccontr 1); by (dtac leI 1); @@ -147,38 +135,27 @@ -(*** Future nonces can't be seen or used! [proofs resemble those above] ***) +(*** Future nonces can't be seen or used! ***) -goal thy "!!evs. evs : ns_shared lost ==> \ +goal thy "!!evs. evs : ns_shared lost ==> \ \ length evs <= length evt --> \ -\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))"; -by (etac ns_shared.induct 1); -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2] - addcongs [disj_cong]))); -by (REPEAT_FIRST (fast_tac (!claset - addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -val lemma = result(); - -(*Variant needed below*) -goal thy - "!!evs. [| evs : ns_shared lost; length evs <= length evs' |] \ -\ ==> Nonce (newN evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_nonces_not_seen"; +\ Nonce (newN evt) ~: 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] + 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 ==> \ +goal thy "!!evs. evs : ns_shared lost ==> \ \ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; +\ newK evs' ~: 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])); @@ -196,13 +173,7 @@ by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys] addIs [less_SucI, impOfSubs keysFor_mono] addss (!simpset addsimps [le_def])) 1)); -val lemma = result(); - -goal thy - "!!evs. [| evs : ns_shared lost; length evs <= length evs' |] \ -\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); -qed "new_keys_not_used"; +qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono, diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Tue Nov 05 11:20:52 1996 +0100 @@ -131,30 +131,19 @@ (*** Future keys can't be seen or used! ***) -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The Union over C is essential for the induction! *) +(*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') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : otway lost; length evs <= length evs' |] \ -\ ==> Key (newK evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_keys_not_seen"; +qed_spec_mp "new_keys_not_seen"; Addsimps [new_keys_not_seen]; -(*Another variant: old messages must contain old keys!*) +(*Variant: old messages must contain old keys!*) goal thy "!!evs. [| Says A B X : set_of_list evs; \ \ Key (newK evt) : parts {X}; \ @@ -167,15 +156,12 @@ qed "Says_imp_old_keys"; -(*** Future nonces can't be seen or used! [proofs resemble those above] ***) +(*** Future nonces can't be seen or used! ***) goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evt --> \ -\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))"; -by (etac otway.induct 1); -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2] - addcongs [disj_cong]))); +\ Nonce (newN evt) ~: 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] @@ -183,22 +169,14 @@ impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : otway lost; length evs <= length evs' |] \ -\ ==> Nonce (newN evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_nonces_not_seen"; +qed_spec_mp "new_nonces_not_seen"; Addsimps [new_nonces_not_seen]; -(*Another 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"; +(*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"; by (rtac ccontr 1); by (dtac leI 1); by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] @@ -208,9 +186,9 @@ (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) -goal thy "!!evs. evs : otway lost ==> \ +goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; +\ newK evs' ~: 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])); @@ -222,13 +200,7 @@ Suc_leD] addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] addss (!simpset)) 1)); -val lemma = result(); - -goal thy - "!!evs. [| evs : otway lost; length evs <= length evs' |] \ -\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); -qed "new_keys_not_used"; +qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono, @@ -283,12 +255,11 @@ by (etac otway.induct 1); by analz_Fake_tac; by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); -by (ALLGOALS (*Takes 22 secs*) +by (ALLGOALS (*Takes 14 secs*) (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); -(** LEVEL 5 **) (*OR4, OR2, Fake*) by (EVERY (map spy_analz_tac [5,3,2])); (*Oops, OR3, Base*) diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Nov 05 11:20:52 1996 +0100 @@ -119,30 +119,19 @@ (*** Future keys can't be seen or used! ***) -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The Union over C is essential for the induction! *) +(*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') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : otway lost; length evs <= length evs' |] \ -\ ==> Key (newK evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_keys_not_seen"; +qed_spec_mp "new_keys_not_seen"; Addsimps [new_keys_not_seen]; -(*Another variant: old messages must contain old keys!*) +(*Variant: old messages must contain old keys!*) goal thy "!!evs. [| Says A B X : set_of_list evs; \ \ Key (newK evt) : parts {X}; \ @@ -155,15 +144,12 @@ qed "Says_imp_old_keys"; -(*** Future nonces can't be seen or used! [proofs resemble those above] ***) +(*** Future nonces can't be seen or used! ***) goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evt --> \ -\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))"; -by (etac otway.induct 1); -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2] - addcongs [disj_cong]))); +\ Nonce (newN evt) ~: 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] @@ -171,14 +157,7 @@ impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : otway lost; length evs <= length evs' |] \ -\ ==> Nonce (newN evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_nonces_not_seen"; +qed_spec_mp "new_nonces_not_seen"; Addsimps [new_nonces_not_seen]; @@ -186,7 +165,7 @@ ...very like new_keys_not_seen*) goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; +\ newK evs' ~: 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])); @@ -198,13 +177,7 @@ Suc_leD] addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] addss (!simpset)) 1)); -val lemma = result(); - -goal thy - "!!evs. [| evs : otway lost; length evs <= length evs' |] \ -\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); -qed "new_keys_not_used"; +qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono, diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Nov 05 11:20:52 1996 +0100 @@ -131,30 +131,19 @@ (*** Future keys can't be seen or used! ***) -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The Union over C is essential for the induction! *) -goal thy "!!evs. evs : otway ==> \ +(*Nobody can have SEEN keys that will be generated in the future. *) +goal thy "!!evs. evs : otway ==> \ \ length evs <= length evs' --> \ -\ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] + impOfSubs parts_insert_subset_Un, + Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : otway; length evs <= length evs' |] \ -\ ==> Key (newK evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_keys_not_seen"; +qed_spec_mp "new_keys_not_seen"; Addsimps [new_keys_not_seen]; -(*Another variant: old messages must contain old keys!*) +(*Variant: old messages must contain old keys!*) goal thy "!!evs. [| Says A B X : set_of_list evs; \ \ Key (newK evt) : parts {X}; \ @@ -167,35 +156,24 @@ qed "Says_imp_old_keys"; -(*** Future nonces can't be seen or used! [proofs resemble those above] ***) +(*** Future nonces can't be seen or used! ***) goal thy "!!evs. evs : otway ==> \ \ length evs <= length evs' --> \ -\ Nonce (newN evs') ~: (UN C. parts (sees lost C evs))"; -by (etac otway.induct 1); -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2] - addcongs [disj_cong]))); -by (REPEAT_FIRST (fast_tac (!claset - addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : otway; length evs <= length evs' |] \ -\ ==> Nonce (newN evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_nonces_not_seen"; +\ Nonce (newN evs') ~: 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] + 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]; -(*Another variant: old messages must contain old nonces!*) +(*Variant: old messages must contain old nonces!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ + "!!evs. [| Says A B X : set_of_list evs; \ \ Nonce (newN evt) : parts {X}; \ \ evs : otway \ \ |] ==> length evt < length evs"; @@ -210,7 +188,7 @@ ...very like new_keys_not_seen*) goal thy "!!evs. evs : otway ==> \ \ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; +\ newK evs' ~: 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])); @@ -222,13 +200,7 @@ Suc_leD] addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] addss (!simpset)) 1)); -val lemma = result(); - -goal thy - "!!evs. [| evs : otway; length evs <= length evs' |] \ -\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); -qed "new_keys_not_used"; +qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono, diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/Shared.ML Tue Nov 05 11:20:52 1996 +0100 @@ -155,7 +155,7 @@ qed "sees_subset_sees_Says"; (*Pushing Unions into parts. One of the agents A is B, and thus sees Y. - Used to prove new_keys_not_seen.*) + Once used to prove new_keys_not_seen; now obsolete.*) goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \ \ parts {Y} Un (UN A. parts (sees lost A evs))"; by (Step_tac 1); @@ -202,7 +202,7 @@ by (ALLGOALS Fast_tac); qed_spec_mp "seesD"; -Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy]; +Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/Yahalom.ML Tue Nov 05 11:20:52 1996 +0100 @@ -118,30 +118,19 @@ (*** Future keys can't be seen or used! ***) -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The Union over C is essential for the induction! *) +(*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') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ -\ ==> Key (newK evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_keys_not_seen"; +qed_spec_mp "new_keys_not_seen"; Addsimps [new_keys_not_seen]; -(*Another variant: old messages must contain old keys!*) +(*Variant: old messages must contain old keys!*) goal thy "!!evs. [| Says A B X : set_of_list evs; \ \ Key (newK evt) : parts {X}; \ @@ -168,31 +157,25 @@ ...very like new_keys_not_seen*) goal thy "!!evs. evs : yahalom lost ==> \ \ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; +\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); -by (dresolve_tac [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 YM4: these messages send unknown (X) components*) -by (stac insert_commute 2); -by (Simp_tac 2); -(*YM4: the only way K could have been used is if it had been seen, - contradicting new_keys_not_seen*) -by (REPEAT - (best_tac - (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] +(*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)] - addss (!simpset)) 1)); -val lemma = result(); - -goal thy - "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ -\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); -qed "new_keys_not_used"; + addDs [Suc_leD]) 1); +qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono, @@ -413,31 +396,22 @@ goal thy "!!evs. evs : yahalom lost ==> \ \ length evs <= length evt --> \ -\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))"; -by (etac yahalom.induct 1); -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2] - addcongs [disj_cong]))); -by (REPEAT_FIRST - (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj] - addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, Suc_leD] - addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ -\ ==> Nonce (newN evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_nonces_not_seen"; +\ Nonce (newN evt) ~: 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] + 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]; -(*Another variant: old messages must contain old nonces!*) +(*Variant: old messages must contain old nonces!*) goal thy - "!!evs. [| Says A B X : set_of_list evs; \ -\ Nonce (newN evt) : parts {X}; \ + "!!evs. [| Says A B X : set_of_list evs; \ +\ Nonce (newN evt) : parts {X}; \ \ evs : yahalom lost \ \ |] ==> length evt < length evs"; by (rtac ccontr 1); diff -r e650a3f6f600 -r ad4382e546fc src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Mon Nov 04 17:23:37 1996 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Tue Nov 05 11:20:52 1996 +0100 @@ -126,30 +126,19 @@ (*** Future keys can't be seen or used! ***) -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The Union over C is essential for the induction! *) +(*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') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: parts (sees lost Spy evs)"; by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset)))); -val lemma = result(); - -(*Variant needed for the main theorem below*) -goal thy - "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ -\ ==> Key (newK evs') ~: parts (sees lost C evs)"; -by (fast_tac (!claset addDs [lemma]) 1); -qed "new_keys_not_seen"; +qed_spec_mp "new_keys_not_seen"; Addsimps [new_keys_not_seen]; -(*Another variant: old messages must contain old keys!*) +(*Variant: old messages must contain old keys!*) goal thy "!!evs. [| Says A B X : set_of_list evs; \ \ Key (newK evt) : parts {X}; \ @@ -166,31 +155,26 @@ ...very like new_keys_not_seen*) goal thy "!!evs. evs : yahalom lost ==> \ \ length evs <= length evs' --> \ -\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; +\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; by (parts_induct_tac 1); by (dresolve_tac [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 YM4: these messages send unknown (X) components*) -by (stac insert_commute 2); -by (Simp_tac 2); -(*YM4: the only way K could have been used is if it had been seen, - contradicting new_keys_not_seen*) -by (REPEAT - (best_tac - (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs (analz_subset_parts RS keysFor_mono), - impOfSubs (parts_insert_subset_Un RS keysFor_mono), - Suc_leD] +(*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)] - addss (!simpset)) 1)); -val lemma = result(); - -goal thy - "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ -\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; -by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); -qed "new_keys_not_used"; + addDs [Suc_leD]) 1); +qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", [analz_subset_parts RS keysFor_mono,