# HG changeset patch # User paulson # Date 879867393 -3600 # Node ID fb01353e363b4b8627c7a0cab4d5720e5381ba12 # Parent fc85fd71842987c370fe3a300a5622205e6c278d The dtac was discarding information, though apparently no proofs were hurt diff -r fc85fd718429 -r fb01353e363b src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Tue Nov 18 15:30:50 1997 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Tue Nov 18 16:36:33 1997 +0100 @@ -19,7 +19,7 @@ (*A "possibility property": there are traces that reach the end*) goal thy "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX N K. EX evs: ns_shared. \ +\ ==> EX N K. EX evs: ns_shared. \ \ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS @@ -62,7 +62,7 @@ fun parts_induct_tac i = etac ns_shared.induct i THEN forward_tac [Oops_parts_spies] (i+7) THEN - dtac NS3_msg_in_parts_spies (i+4) THEN + forward_tac [NS3_msg_in_parts_spies] (i+4) THEN prove_simple_subgoals_tac i; @@ -100,9 +100,9 @@ (*Fake*) by (best_tac (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); + addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] + addss (simpset())) 1); (*NS2, NS4, NS5*) by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); qed_spec_mp "new_keys_not_used"; @@ -152,7 +152,7 @@ \ | X : analz (spies evs)"; by (case_tac "A : bad" 1); by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] - addss (simpset())) 1); + addss (simpset())) 1); by (forward_tac [Says_imp_spies RS parts.Inj] 1); by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); qed "Says_S_message_form"; @@ -181,12 +181,12 @@ We require that agents should behave like this subsequently also.*) goal thy "!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \ -\ (Crypt KAB X) : parts (spies evs) & \ +\ (Crypt KAB X) : parts (spies evs) & \ \ Key K : parts {X} --> Key K : parts (spies evs)"; by (parts_induct_tac 1); (*Deals with Faked messages*) by (blast_tac (claset() addSEs partsEs - addDs [impOfSubs parts_insert_subset_Un]) 1); + addDs [impOfSubs parts_insert_subset_Un]) 1); (*Base, NS4 and NS5*) by (Auto_tac()); result(); @@ -196,8 +196,8 @@ (*The equality makes the induction hypothesis easier to apply*) goal thy - "!!evs. evs : ns_shared ==> \ -\ ALL K KK. KK <= Compl (range shrK) --> \ + "!!evs. evs : ns_shared ==> \ +\ ALL K KK. KK <= Compl (range shrK) --> \ \ (Key K : analz (Key``KK Un (spies evs))) = \ \ (K : KK | Key K : analz (spies evs))"; by (etac ns_shared.induct 1); @@ -214,7 +214,7 @@ goal thy - "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \ + "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \ \ Key K : analz (insert (Key KAB) (spies evs)) = \ \ (K = KAB | Key K : analz (spies evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); @@ -225,7 +225,7 @@ goal thy "!!evs. evs : ns_shared ==> \ -\ EX A' NA' B' X'. ALL A NA B X. \ +\ EX A' NA' B' X'. ALL A NA B X. \ \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \ \ --> A=A' & NA=NA' & B=B' & X=X'"; by (etac ns_shared.induct 1); @@ -237,15 +237,15 @@ (*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 (blast_tac (claset() delrules [conjI] (*prevent split-up into 4 subgoals*) - addSEs spies_partsEs) 1); +by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) + addSEs spies_partsEs) 1); val lemma = result(); (*In messages of this form, the session key uniquely identifies the rest*) goal thy - "!!evs. [| Says Server A \ -\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ -\ Says Server A' \ + "!!evs. [| Says Server A \ +\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ +\ Says Server A' \ \ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \ \ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'"; by (prove_unique_tac lemma 1); @@ -267,14 +267,15 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ - pushes @ expand_ifs)))); + pushes @ expand_ifs)))); (*Oops*) by (blast_tac (claset() addDs [unique_session_keys]) 5); (*NS3, replay sub-case*) by (Blast_tac 4); (*NS2*) by (blast_tac (claset() addSEs spies_partsEs - addIs [parts_insertI, impOfSubs analz_subset_parts]) 2); + addIs [parts_insertI, + impOfSubs analz_subset_parts]) 2); (*Fake*) by (spy_analz_tac 1); (*NS3, Server sub-case*) (**LEVEL 6 **) @@ -289,9 +290,9 @@ (*Final version: Server's message in the most abstract form*) goal thy - "!!evs. [| Says Server A \ -\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ -\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \ + "!!evs. [| Says Server A \ +\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ +\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \ \ A ~: bad; B ~: bad; evs : ns_shared \ \ |] ==> Key K ~: analz (spies evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); @@ -306,8 +307,8 @@ (*If the encrypted message appears then it originated with the Server*) goal thy - "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ -\ B ~: bad; evs : ns_shared |] \ + "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ +\ B ~: bad; evs : ns_shared |] \ \ ==> EX NA. Says Server A \ \ (Crypt (shrK A) {|NA, Agent B, Key K, \ \ Crypt (shrK B) {|Key K, Agent A|}|}) \ @@ -337,7 +338,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (**LEVEL 7**) by (blast_tac (claset() addSDs [Crypt_Fake_parts_insert] - addDs [impOfSubs analz_subset_parts]) 1); + addDs [impOfSubs analz_subset_parts]) 1); by (Blast_tac 2); by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); (*Subgoal 1: contradiction from the assumptions @@ -349,9 +350,9 @@ by (thin_tac "?PP-->?QQ" 1); by (case_tac "Ba : bad" 1); by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, - unique_session_keys]) 2); + unique_session_keys]) 2); by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS - Crypt_Spy_analz_bad]) 1); + Crypt_Spy_analz_bad]) 1); val lemma = result(); goal thy @@ -362,5 +363,5 @@ \ A ~: bad; B ~: bad; evs : ns_shared |] \ \ ==> Says B A (Crypt K (Nonce NB)) : set evs"; by (blast_tac (claset() addSIs [lemma RS mp RS mp RS mp] - addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); + addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); qed "A_trusts_NS4";