Streamlining for the bug fix in Blast.
MPair_parts now built in using AddSEs, throughout.
--- 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];
--- 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*)
--- 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
--- 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*)
--- 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 @@
\<in> set evso\<rbrakk>
\<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> 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 \<in> ns_shared\<rbrakk>
\<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
\<or> X \<in> 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:
"\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
\<in> 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 @@
\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
\<Longrightarrow> Key K \<notin> 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:
"\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
- B \<notin> bad; evs \<in> ns_shared\<rbrakk>
- \<Longrightarrow> \<exists>NA. Says Server A
+ B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> \<exists>NA. Says Server A
(Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
\<in> 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 \<in> 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 \<in> 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 @@
\<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
\<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> 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
--- 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";
--- 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*)
--- 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];
--- 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 \\<in> 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
--- 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);
--- 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*)
--- 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);
--- 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);