# HG changeset patch # User paulson # Date 982326308 -3600 # Node ID 67387142225eaf6e6b1a3ab091017167e17c1a46 # Parent e258b536a137d95368a5a892be39410aa90564eb Streamlining for the bug fix in Blast. MPair_parts now built in using AddSEs, throughout. diff -r e258b536a137 -r 67387142225e src/HOL/Auth/Event_lemmas.ML --- a/src/HOL/Auth/Event_lemmas.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/Event_lemmas.ML Fri Feb 16 13:25:08 2001 +0100 @@ -69,7 +69,7 @@ (*Use with addSEs to derive contradictions from old Says events containing items known to be fresh*) bind_thms ("knows_Spy_partsEs", - make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs); + map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]); Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets]; diff -r e258b536a137 -r 67387142225e src/HOL/Auth/Kerberos_BAN.ML --- a/src/HOL/Auth/Kerberos_BAN.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Feb 16 13:25:08 2001 +0100 @@ -16,9 +16,8 @@ Tidied by lcp. *) -AddEs spies_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; AddIffs [SesKeyLife_LB, AutLife_LB]; @@ -229,10 +228,9 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq, - analz_insert_freshK] - @ pushes))); -(*Oops*) -by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4); + analz_insert_freshK] @ pushes))); +(*Oops: PROOF FAILED if addIs below*) +by (blast_tac (claset() addDs [unique_session_keys] addSIs [less_SucI]) 4); (*Kb2*) by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2); (*Fake*) diff -r e258b536a137 -r 67387142225e src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/Message.ML Fri Feb 16 13:25:08 2001 +0100 @@ -120,12 +120,11 @@ AddIs [parts.Inj]; -val partsEs = [MPair_parts, make_elim parts.Body]; - -AddSEs partsEs; +AddSEs [MPair_parts, make_elim parts.Body]; (*NB These two rules are UNSAFE in the formal sense, as they discard the - compound message. They work well on THIS FILE, perhaps because its - proofs concern only atomic messages.*) + compound message. They work well on THIS FILE. + MPair_parts is left as SAFE because it speeds up proofs. + The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*) Goal "H <= parts(H)"; by (Blast_tac 1); @@ -327,9 +326,9 @@ by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); qed "MPair_analz"; +AddSEs [MPair_analz]; (*Making it safe speeds up proofs*) +AddDs [analz.Decrypt]; (*Unsafe: we don't want to split up certificates!*) AddIs [analz.Inj]; -AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) -AddDs [analz.Decrypt]; Addsimps [analz.Inj]; @@ -829,7 +828,7 @@ (*We do NOT want Crypt... messages broken up in protocols!!*) -Delrules partsEs; +Delrules [make_elim parts.Body]; (** Rewrites to push in Key and Crypt messages, so that other messages can diff -r e258b536a137 -r 67387142225e src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Feb 16 13:25:08 2001 +0100 @@ -202,7 +202,7 @@ apply (erule ns_public.induct, simp_all) apply spy_analz (*NS1: by freshness*) -apply (blast) +apply blast (*NS2: by freshness and unicity of NB*) apply (blast intro: no_nonce_NS1_NS2) (*NS3: unicity of NB identifies A and NA, but not B*) diff -r e258b536a137 -r 67387142225e src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/NS_Shared.thy Fri Feb 16 13:25:08 2001 +0100 @@ -71,9 +71,13 @@ \ set evso\ \ Notes Spy \Nonce NA, Nonce NB, Key K\ # evso \ ns_shared" -declare knows_Spy_partsEs [elim] + +declare Says_imp_knows_Spy [THEN parts.Inj, dest] +declare parts.Body [dest] +declare MPair_parts [elim!] (*can speed up some proofs*) + declare analz_subset_parts [THEN subsetD, dest] -declare Fake_parts_insert [THEN subsetD, dest] +declare Fake_parts_insert [THEN subsetD, dest] declare image_eq_UN [simp] (*accelerates proofs involving nested images*) @@ -171,10 +175,8 @@ evs \ ns_shared\ \ (K \ range shrK \ X = (Crypt (shrK B) \Key K, Agent A\)) \ X \ analz (spies evs)" -apply (frule Says_imp_knows_Spy) -(*mystery: why is this frule needed?*) -apply (blast dest: cert_A_form analz.Inj) -done +by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj) + (*Alternative version also provable lemma Says_S_message_form2: @@ -251,7 +253,8 @@ (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) -lemma secrecy_lemma [rule_format]: +(*Beware of [rule_format] and the universal quantifier!*) +lemma secrecy_lemma: "\Says Server A (Crypt (shrK A) \NA, Agent B, Key K, Crypt (shrK B) \Key K, Agent A\\) \ set evs; @@ -269,7 +272,7 @@ (*NS3, Server sub-case*) (**LEVEL 6 **) apply clarify apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2]) -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad]) +apply (blast dest: Says_imp_knows_Spy analz.Inj Crypt_Spy_analz_bad) apply assumption apply (blast dest: unique_session_keys)+ (*also proves Oops*) done @@ -281,9 +284,7 @@ \NB. Notes Spy \NA, NB, Key K\ \ set evs; A \ bad; B \ bad; evs \ ns_shared\ \ Key K \ analz (spies evs)" -apply (frule Says_Server_message_form, assumption) -apply (auto dest: Says_Server_message_form secrecy_lemma) -done +by (blast dest: Says_Server_message_form secrecy_lemma) (**** Guarantees available at various stages of protocol ***) @@ -291,8 +292,8 @@ (*If the encrypted message appears then it originated with the Server*) lemma B_trusts_NS3: "\Crypt (shrK B) \Key K, Agent A\ \ parts (spies evs); - B \ bad; evs \ ns_shared\ - \ \NA. Says Server A + B \ bad; evs \ ns_shared\ + \ \NA. Says Server A (Crypt (shrK A) \NA, Agent B, Key K, Crypt (shrK B) \Key K, Agent A\\) \ set evs" @@ -317,10 +318,9 @@ apply (force dest!: Crypt_imp_keysFor) apply blast (*NS3*) (*NS4*) -apply clarify; -apply (frule Says_imp_knows_Spy [THEN analz.Inj]) -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad - B_trusts_NS3 unique_session_keys) +apply (blast dest!: B_trusts_NS3 + dest: Says_imp_knows_Spy [THEN analz.Inj] + Crypt_Spy_analz_bad unique_session_keys) done (*This version no longer assumes that K is secure*) @@ -349,11 +349,9 @@ apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) apply blast (*NS3*) (*NS4*) -apply (case_tac "Ba \ bad") -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad); -apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3], - assumption+) -apply (blast dest: unique_session_keys) +apply (blast dest!: B_trusts_NS3 + dest: Says_imp_knows_Spy [THEN analz.Inj] + unique_session_keys Crypt_Spy_analz_bad) done @@ -371,12 +369,10 @@ apply blast (*Fake*) apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) apply (blast dest!: cert_A_form) (*NS3*) -(**LEVEL 5**) (*NS5*) -apply clarify -apply (case_tac "Aa \ bad") -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad); -apply (blast dest: A_trusts_NS2 unique_session_keys) +apply (blast dest!: A_trusts_NS2 + dest: Says_imp_knows_Spy [THEN analz.Inj] + unique_session_keys Crypt_Spy_analz_bad) done @@ -387,10 +383,7 @@ \NA NB. Notes Spy \NA, NB, Key K\ \ set evs; A \ bad; B \ bad; evs \ ns_shared\ \ Says A B (Crypt K \Nonce NB, Nonce NB\) \ set evs" -apply (drule B_trusts_NS3, clarify+) -apply (blast intro: B_trusts_NS5_lemma - dest: dest: Spy_not_see_encrypted_key) -(*surprisingly delicate proof due to quantifier interactions*) -done +by (blast intro: B_trusts_NS5_lemma + dest: B_trusts_NS3 Spy_not_see_encrypted_key) end diff -r e258b536a137 -r 67387142225e src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Fri Feb 16 13:25:08 2001 +0100 @@ -12,9 +12,8 @@ Proc. Royal Soc. 426 (1989) *) -AddEs knows_Spy_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) @@ -40,7 +39,7 @@ Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs"; by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); qed"Gets_imp_knows_Spy"; -AddDs [Gets_imp_knows_Spy RS parts.Inj]; +AddSDs [Gets_imp_knows_Spy RS parts.Inj]; (**** Inductive proofs about otway ****) @@ -103,12 +102,7 @@ (*OR2, OR3*) by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; - -bind_thm ("new_keys_not_analzd", - [analz_subset_parts RS keysFor_mono, - new_keys_not_used] MRS contra_subsetD); - -Addsimps [new_keys_not_used, new_keys_not_analzd]; +Addsimps [new_keys_not_used]; @@ -233,29 +227,21 @@ (*Crucial property: If the encrypted message appears, and A has used NA to start a run, then it originated with the Server!*) Goal "[| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \ -\ --> Says A B {|NA, Agent A, Agent B, \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ -\ : set evs --> \ -\ (EX NB. Says Server B \ -\ {|NA, \ -\ Crypt (shrK A) {|NA, Key K|}, \ -\ Crypt (shrK B) {|NB, Key K|}|} \ -\ : set evs)"; +\ ==> Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \ +\ Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \ +\ --> (EX NB. Says Server B \ +\ {|NA, \ +\ Crypt (shrK A) {|NA, Key K|}, \ +\ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; by (parts_induct_tac 1); by (Blast_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (Blast_tac 1); -(*OR3 and OR4*) +(*OR4*) +by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2); by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); -by (rtac conjI 1); -by (ALLGOALS Clarify_tac); -(*OR4*) -by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3); -(*OR3, two cases*) (** LEVEL 7 **) -by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] - delrules [conjI] (*stop split-up into 4 subgoals*)) 2); -by (blast_tac (claset() addIs [unique_NA]) 1); +by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] addIs [unique_NA]) 1); qed_spec_mp "NA_Crypt_imp_Server_msg"; @@ -308,8 +294,7 @@ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ \ ==> Key K ~: analz (knows Spy evs)"; -by (ftac Says_Server_message_form 1 THEN assume_tac 1); -by (blast_tac (claset() addSEs [lemma]) 1); +by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -356,7 +341,7 @@ qed "unique_NB"; (*If the encrypted message appears, and B has used Nonce NB, - then it originated with the Server!*) + then it originated with the Server! Quite messy proof.*) Goal "[| B ~: bad; evs : otway |] \ \ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \ \ --> (ALL X'. Says B Server \ @@ -367,14 +352,16 @@ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set evs)"; +by (asm_full_simp_tac (simpset() addsimps []) 1); by (parts_induct_tac 1); by (Blast_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (Blast_tac 1); (*OR4*) by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 2); -(*OR3*) -by (blast_tac (claset() addDs [unique_NB] addEs [nonce_OR1_OR2_E]) 1); +(*OR3: needs AddSEs [MPair_parts] or it takes forever!*) +by (blast_tac (claset() addDs [unique_NB] + addEs [nonce_OR1_OR2_E]) 1); qed_spec_mp "NB_Crypt_imp_Server_msg"; @@ -431,5 +418,6 @@ \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ \ : set evs"; -by (blast_tac (claset() addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); +by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj] + addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); qed "A_auths_B"; diff -r e258b536a137 -r 67387142225e src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Feb 16 13:25:08 2001 +0100 @@ -12,9 +12,8 @@ IEEE Trans. SE 22 (1), 1996 *) -AddEs knows_Spy_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) diff -r e258b536a137 -r 67387142225e src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Feb 16 13:25:08 2001 +0100 @@ -15,10 +15,8 @@ indicates the possibility of this attack. *) -AddEs knows_Spy_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; - +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) Goal "[| A ~= B; B ~= Server |] \ @@ -107,12 +105,7 @@ (*OR2, OR3*) by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; - -bind_thm ("new_keys_not_analzd", - [analz_subset_parts RS keysFor_mono, - new_keys_not_used] MRS contra_subsetD); - -Addsimps [new_keys_not_used, new_keys_not_analzd]; +Addsimps [new_keys_not_used]; diff -r e258b536a137 -r 67387142225e src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/Recur.ML Fri Feb 16 13:25:08 2001 +0100 @@ -8,9 +8,8 @@ Pretty.setdepth 30; -AddEs spies_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (** Possibility properties: traces that reach the end @@ -343,9 +342,7 @@ by (Asm_full_simp_tac 1); (*by unicity, either B=Aa or B=A', a contradiction if B \\ bad*) by (blast_tac - (claset() addSEs [MPair_parts] - addDs [parts.Body, - respond_certificate RSN (2, unique_session_keys)]) 1); + (claset() addDs [respond_certificate RSN (2, unique_session_keys)]) 1); qed_spec_mp "respond_Spy_not_see_session_key"; @@ -371,7 +368,6 @@ by (safe_tac (claset() delrules [impCE])); (*RA3, case 2: K is an old key*) by (blast_tac (claset() addSDs [resp_analz_insert] - addSEs partsEs addDs [Key_in_parts_respond]) 2); (*RA3, case 1: use lemma previously proved by induction*) by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN diff -r e258b536a137 -r 67387142225e src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/TLS.ML Fri Feb 16 13:25:08 2001 +0100 @@ -17,9 +17,8 @@ rollback attacks). *) -AddEs spies_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*Automatically unfold the definition of "certificate"*) Addsimps [certificate_def]; @@ -129,10 +128,8 @@ needless information about analz (insert X (spies evs)) *) fun parts_induct_tac i = etac tls.induct i - THEN - REPEAT (FIRSTGOAL analz_mono_contra_tac) - THEN - fast_tac (claset() addss (simpset())) i THEN + THEN REPEAT (FIRSTGOAL analz_mono_contra_tac) + THEN Force_tac i THEN ALLGOALS Asm_simp_tac; @@ -438,14 +435,14 @@ \ Nonce PMS ~: analz (spies evs)"; by (analz_induct_tac 1); (*4 seconds*) (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) -by (REPEAT (fast_tac (claset() addss (simpset())) 6)); +by (REPEAT (Force_tac 6)); (*ClientHello, ServerHello, ClientKeyExch, ServerResume: mostly freshness reasoning*) -by (REPEAT (blast_tac (claset() addSEs partsEs +by (REPEAT (blast_tac (claset() addSDs [parts.Body] addDs [Notes_Crypt_parts_spies, Says_imp_spies RS analz.Inj]) 3)); (*SpyKeys*) -by (fast_tac (claset() addss (simpset())) 2); +by (Force_tac 2); (*Fake*) by (spy_analz_tac 1); bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp)); @@ -469,7 +466,7 @@ (*Fake*) by (spy_analz_tac 1); (*ServerHello and ClientKeyExch: mostly freshness reasoning*) -by (REPEAT (blast_tac (claset() addSEs partsEs +by (REPEAT (blast_tac (claset() addSDs [parts.Body] addDs [Notes_Crypt_parts_spies, Says_imp_spies RS analz.Inj]) 1)); bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); @@ -578,7 +575,6 @@ \ X : parts (spies evs) --> Says B A X : set evs"; by (hyp_subst_tac 1); by (analz_induct_tac 1); (*7 seconds*) -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); by (ALLGOALS Clarify_tac); (*ClientKeyExch*) by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); diff -r e258b536a137 -r 67387142225e src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/WooLam.ML Fri Feb 16 13:25:08 2001 +0100 @@ -10,9 +10,8 @@ IEEE Trans. S.E. 22(1), 1996, pages 6-15. *) -AddEs spies_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) diff -r e258b536a137 -r 67387142225e src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/Yahalom.ML Fri Feb 16 13:25:08 2001 +0100 @@ -58,8 +58,8 @@ (*For Oops*) Goal "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs \ \ ==> K : parts (knows Spy evs)"; -by (blast_tac (claset() addSEs partsEs - addSDs [Says_imp_knows_Spy RS parts.Inj]) 1); +by (blast_tac (claset() addSDs [parts.Body, + Says_imp_knows_Spy RS parts.Inj]) 1); qed "YM4_Key_parts_knows_Spy"; (*For proving the easier theorems about X ~: parts (knows Spy evs).*) @@ -439,7 +439,7 @@ by (Fake_parts_insert_tac 1); by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj] addSIs [parts_insertI] - addSEs partsEs) 1); + addSDs [parts.Body]) 1); bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); (*more readable version cited in Yahalom paper*) @@ -475,7 +475,7 @@ addSEs [no_nonce_YM1_YM2, MPair_parts] addDs [Gets_imp_Says, Says_unique_NB]) 4); (*YM2: similar freshness reasoning*) -by (blast_tac (claset() addSEs partsEs +by (blast_tac (claset() addSDs [parts.Body] addDs [Gets_imp_Says, Says_imp_knows_Spy RS analz.Inj, impOfSubs analz_subset_parts]) 3); diff -r e258b536a137 -r 67387142225e src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Fri Feb 16 08:27:17 2001 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Fri Feb 16 13:25:08 2001 +0100 @@ -12,9 +12,8 @@ Proc. Royal Soc. 426 (1989) *) -AddEs knows_Spy_partsEs; -AddDs [impOfSubs analz_subset_parts]; -AddDs [impOfSubs Fake_parts_insert]; +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) @@ -57,8 +56,8 @@ (*For Oops*) Goal "Says Server A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs \ \ ==> K : parts (knows Spy evs)"; -by (blast_tac (claset() addSEs partsEs - addSDs [Says_imp_knows_Spy RS parts.Inj]) 1); +by (blast_tac (claset() addSDs [parts.Body, + Says_imp_knows_Spy RS parts.Inj]) 1); qed "YM4_Key_parts_knows_Spy"; (*For proving the easier theorems about X ~: parts (knows Spy evs).*) @@ -361,7 +360,7 @@ by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); (*yes: delete a useless induction hypothesis; apply unicity of session keys*) by (thin_tac "?P-->?Q" 1); -by (ftac Gets_imp_Says 1 THEN assume_tac 1); +by (dtac Gets_imp_Says 1 THEN assume_tac 1); by (not_bad_tac "Aa" 1); by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK] addDs [unique_session_keys]) 1);