Streamlining for the bug fix in Blast.
MPair_parts now built in using AddSEs, throughout.
1.1 --- a/src/HOL/Auth/Event_lemmas.ML Fri Feb 16 08:27:17 2001 +0100
1.2 +++ b/src/HOL/Auth/Event_lemmas.ML Fri Feb 16 13:25:08 2001 +0100
1.3 @@ -69,7 +69,7 @@
1.4 (*Use with addSEs to derive contradictions from old Says events containing
1.5 items known to be fresh*)
1.6 bind_thms ("knows_Spy_partsEs",
1.7 - make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs);
1.8 + map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]);
1.9
1.10 Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
1.11
2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML Fri Feb 16 08:27:17 2001 +0100
2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Feb 16 13:25:08 2001 +0100
2.3 @@ -16,9 +16,8 @@
2.4 Tidied by lcp.
2.5 *)
2.6
2.7 -AddEs spies_partsEs;
2.8 -AddDs [impOfSubs analz_subset_parts];
2.9 -AddDs [impOfSubs Fake_parts_insert];
2.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
2.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
2.12
2.13 AddIffs [SesKeyLife_LB, AutLife_LB];
2.14
2.15 @@ -229,10 +228,9 @@
2.16 by analz_spies_tac;
2.17 by (ALLGOALS
2.18 (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq,
2.19 - analz_insert_freshK]
2.20 - @ pushes)));
2.21 -(*Oops*)
2.22 -by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
2.23 + analz_insert_freshK] @ pushes)));
2.24 +(*Oops: PROOF FAILED if addIs below*)
2.25 +by (blast_tac (claset() addDs [unique_session_keys] addSIs [less_SucI]) 4);
2.26 (*Kb2*)
2.27 by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
2.28 (*Fake*)
3.1 --- a/src/HOL/Auth/Message.ML Fri Feb 16 08:27:17 2001 +0100
3.2 +++ b/src/HOL/Auth/Message.ML Fri Feb 16 13:25:08 2001 +0100
3.3 @@ -120,12 +120,11 @@
3.4
3.5 AddIs [parts.Inj];
3.6
3.7 -val partsEs = [MPair_parts, make_elim parts.Body];
3.8 -
3.9 -AddSEs partsEs;
3.10 +AddSEs [MPair_parts, make_elim parts.Body];
3.11 (*NB These two rules are UNSAFE in the formal sense, as they discard the
3.12 - compound message. They work well on THIS FILE, perhaps because its
3.13 - proofs concern only atomic messages.*)
3.14 + compound message. They work well on THIS FILE.
3.15 + MPair_parts is left as SAFE because it speeds up proofs.
3.16 + The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*)
3.17
3.18 Goal "H <= parts(H)";
3.19 by (Blast_tac 1);
3.20 @@ -327,9 +326,9 @@
3.21 by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
3.22 qed "MPair_analz";
3.23
3.24 +AddSEs [MPair_analz]; (*Making it safe speeds up proofs*)
3.25 +AddDs [analz.Decrypt]; (*Unsafe: we don't want to split up certificates!*)
3.26 AddIs [analz.Inj];
3.27 -AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*)
3.28 -AddDs [analz.Decrypt];
3.29
3.30 Addsimps [analz.Inj];
3.31
3.32 @@ -829,7 +828,7 @@
3.33
3.34
3.35 (*We do NOT want Crypt... messages broken up in protocols!!*)
3.36 -Delrules partsEs;
3.37 +Delrules [make_elim parts.Body];
3.38
3.39
3.40 (** Rewrites to push in Key and Crypt messages, so that other messages can
4.1 --- a/src/HOL/Auth/NS_Public_Bad.thy Fri Feb 16 08:27:17 2001 +0100
4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Feb 16 13:25:08 2001 +0100
4.3 @@ -202,7 +202,7 @@
4.4 apply (erule ns_public.induct, simp_all)
4.5 apply spy_analz
4.6 (*NS1: by freshness*)
4.7 -apply (blast)
4.8 +apply blast
4.9 (*NS2: by freshness and unicity of NB*)
4.10 apply (blast intro: no_nonce_NS1_NS2)
4.11 (*NS3: unicity of NB identifies A and NA, but not B*)
5.1 --- a/src/HOL/Auth/NS_Shared.thy Fri Feb 16 08:27:17 2001 +0100
5.2 +++ b/src/HOL/Auth/NS_Shared.thy Fri Feb 16 13:25:08 2001 +0100
5.3 @@ -71,9 +71,13 @@
5.4 \<in> set evso\<rbrakk>
5.5 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
5.6
5.7 -declare knows_Spy_partsEs [elim]
5.8 +
5.9 +declare Says_imp_knows_Spy [THEN parts.Inj, dest]
5.10 +declare parts.Body [dest]
5.11 +declare MPair_parts [elim!] (*can speed up some proofs*)
5.12 +
5.13 declare analz_subset_parts [THEN subsetD, dest]
5.14 -declare Fake_parts_insert [THEN subsetD, dest]
5.15 +declare Fake_parts_insert [THEN subsetD, dest]
5.16 declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
5.17
5.18
5.19 @@ -171,10 +175,8 @@
5.20 evs \<in> ns_shared\<rbrakk>
5.21 \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
5.22 \<or> X \<in> analz (spies evs)"
5.23 -apply (frule Says_imp_knows_Spy)
5.24 -(*mystery: why is this frule needed?*)
5.25 -apply (blast dest: cert_A_form analz.Inj)
5.26 -done
5.27 +by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
5.28 +
5.29
5.30 (*Alternative version also provable
5.31 lemma Says_S_message_form2:
5.32 @@ -251,7 +253,8 @@
5.33
5.34 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
5.35
5.36 -lemma secrecy_lemma [rule_format]:
5.37 +(*Beware of [rule_format] and the universal quantifier!*)
5.38 +lemma secrecy_lemma:
5.39 "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
5.40 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
5.41 \<in> set evs;
5.42 @@ -269,7 +272,7 @@
5.43 (*NS3, Server sub-case*) (**LEVEL 6 **)
5.44 apply clarify
5.45 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
5.46 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad])
5.47 +apply (blast dest: Says_imp_knows_Spy analz.Inj Crypt_Spy_analz_bad)
5.48 apply assumption
5.49 apply (blast dest: unique_session_keys)+ (*also proves Oops*)
5.50 done
5.51 @@ -281,9 +284,7 @@
5.52 \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
5.53 A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
5.54 \<Longrightarrow> Key K \<notin> analz (spies evs)"
5.55 -apply (frule Says_Server_message_form, assumption)
5.56 -apply (auto dest: Says_Server_message_form secrecy_lemma)
5.57 -done
5.58 +by (blast dest: Says_Server_message_form secrecy_lemma)
5.59
5.60
5.61 (**** Guarantees available at various stages of protocol ***)
5.62 @@ -291,8 +292,8 @@
5.63 (*If the encrypted message appears then it originated with the Server*)
5.64 lemma B_trusts_NS3:
5.65 "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
5.66 - B \<notin> bad; evs \<in> ns_shared\<rbrakk>
5.67 - \<Longrightarrow> \<exists>NA. Says Server A
5.68 + B \<notin> bad; evs \<in> ns_shared\<rbrakk>
5.69 + \<Longrightarrow> \<exists>NA. Says Server A
5.70 (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
5.71 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
5.72 \<in> set evs"
5.73 @@ -317,10 +318,9 @@
5.74 apply (force dest!: Crypt_imp_keysFor)
5.75 apply blast (*NS3*)
5.76 (*NS4*)
5.77 -apply clarify;
5.78 -apply (frule Says_imp_knows_Spy [THEN analz.Inj])
5.79 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
5.80 - B_trusts_NS3 unique_session_keys)
5.81 +apply (blast dest!: B_trusts_NS3
5.82 + dest: Says_imp_knows_Spy [THEN analz.Inj]
5.83 + Crypt_Spy_analz_bad unique_session_keys)
5.84 done
5.85
5.86 (*This version no longer assumes that K is secure*)
5.87 @@ -349,11 +349,9 @@
5.88 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
5.89 apply blast (*NS3*)
5.90 (*NS4*)
5.91 -apply (case_tac "Ba \<in> bad")
5.92 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
5.93 -apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3],
5.94 - assumption+)
5.95 -apply (blast dest: unique_session_keys)
5.96 +apply (blast dest!: B_trusts_NS3
5.97 + dest: Says_imp_knows_Spy [THEN analz.Inj]
5.98 + unique_session_keys Crypt_Spy_analz_bad)
5.99 done
5.100
5.101
5.102 @@ -371,12 +369,10 @@
5.103 apply blast (*Fake*)
5.104 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
5.105 apply (blast dest!: cert_A_form) (*NS3*)
5.106 -(**LEVEL 5**)
5.107 (*NS5*)
5.108 -apply clarify
5.109 -apply (case_tac "Aa \<in> bad")
5.110 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
5.111 -apply (blast dest: A_trusts_NS2 unique_session_keys)
5.112 +apply (blast dest!: A_trusts_NS2
5.113 + dest: Says_imp_knows_Spy [THEN analz.Inj]
5.114 + unique_session_keys Crypt_Spy_analz_bad)
5.115 done
5.116
5.117
5.118 @@ -387,10 +383,7 @@
5.119 \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
5.120 A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
5.121 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
5.122 -apply (drule B_trusts_NS3, clarify+)
5.123 -apply (blast intro: B_trusts_NS5_lemma
5.124 - dest: dest: Spy_not_see_encrypted_key)
5.125 -(*surprisingly delicate proof due to quantifier interactions*)
5.126 -done
5.127 +by (blast intro: B_trusts_NS5_lemma
5.128 + dest: B_trusts_NS3 Spy_not_see_encrypted_key)
5.129
5.130 end
6.1 --- a/src/HOL/Auth/OtwayRees.ML Fri Feb 16 08:27:17 2001 +0100
6.2 +++ b/src/HOL/Auth/OtwayRees.ML Fri Feb 16 13:25:08 2001 +0100
6.3 @@ -12,9 +12,8 @@
6.4 Proc. Royal Soc. 426 (1989)
6.5 *)
6.6
6.7 -AddEs knows_Spy_partsEs;
6.8 -AddDs [impOfSubs analz_subset_parts];
6.9 -AddDs [impOfSubs Fake_parts_insert];
6.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
6.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
6.12
6.13
6.14 (*A "possibility property": there are traces that reach the end*)
6.15 @@ -40,7 +39,7 @@
6.16 Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs";
6.17 by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
6.18 qed"Gets_imp_knows_Spy";
6.19 -AddDs [Gets_imp_knows_Spy RS parts.Inj];
6.20 +AddSDs [Gets_imp_knows_Spy RS parts.Inj];
6.21
6.22
6.23 (**** Inductive proofs about otway ****)
6.24 @@ -103,12 +102,7 @@
6.25 (*OR2, OR3*)
6.26 by (ALLGOALS Blast_tac);
6.27 qed_spec_mp "new_keys_not_used";
6.28 -
6.29 -bind_thm ("new_keys_not_analzd",
6.30 - [analz_subset_parts RS keysFor_mono,
6.31 - new_keys_not_used] MRS contra_subsetD);
6.32 -
6.33 -Addsimps [new_keys_not_used, new_keys_not_analzd];
6.34 +Addsimps [new_keys_not_used];
6.35
6.36
6.37
6.38 @@ -233,29 +227,21 @@
6.39 (*Crucial property: If the encrypted message appears, and A has used NA
6.40 to start a run, then it originated with the Server!*)
6.41 Goal "[| A ~: bad; evs : otway |] \
6.42 -\ ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \
6.43 -\ --> Says A B {|NA, Agent A, Agent B, \
6.44 -\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
6.45 -\ : set evs --> \
6.46 -\ (EX NB. Says Server B \
6.47 -\ {|NA, \
6.48 -\ Crypt (shrK A) {|NA, Key K|}, \
6.49 -\ Crypt (shrK B) {|NB, Key K|}|} \
6.50 -\ : set evs)";
6.51 +\ ==> Says A B {|NA, Agent A, Agent B, \
6.52 +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \
6.53 +\ Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \
6.54 +\ --> (EX NB. Says Server B \
6.55 +\ {|NA, \
6.56 +\ Crypt (shrK A) {|NA, Key K|}, \
6.57 +\ Crypt (shrK B) {|NB, Key K|}|} : set evs)";
6.58 by (parts_induct_tac 1);
6.59 by (Blast_tac 1);
6.60 (*OR1: it cannot be a new Nonce, contradiction.*)
6.61 by (Blast_tac 1);
6.62 -(*OR3 and OR4*)
6.63 +(*OR4*)
6.64 +by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
6.65 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
6.66 -by (rtac conjI 1);
6.67 -by (ALLGOALS Clarify_tac);
6.68 -(*OR4*)
6.69 -by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3);
6.70 -(*OR3, two cases*) (** LEVEL 7 **)
6.71 -by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
6.72 - delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
6.73 -by (blast_tac (claset() addIs [unique_NA]) 1);
6.74 +by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] addIs [unique_NA]) 1);
6.75 qed_spec_mp "NA_Crypt_imp_Server_msg";
6.76
6.77
6.78 @@ -308,8 +294,7 @@
6.79 \ Notes Spy {|NA, NB, Key K|} ~: set evs; \
6.80 \ A ~: bad; B ~: bad; evs : otway |] \
6.81 \ ==> Key K ~: analz (knows Spy evs)";
6.82 -by (ftac Says_Server_message_form 1 THEN assume_tac 1);
6.83 -by (blast_tac (claset() addSEs [lemma]) 1);
6.84 +by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1);
6.85 qed "Spy_not_see_encrypted_key";
6.86
6.87
6.88 @@ -356,7 +341,7 @@
6.89 qed "unique_NB";
6.90
6.91 (*If the encrypted message appears, and B has used Nonce NB,
6.92 - then it originated with the Server!*)
6.93 + then it originated with the Server! Quite messy proof.*)
6.94 Goal "[| B ~: bad; evs : otway |] \
6.95 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \
6.96 \ --> (ALL X'. Says B Server \
6.97 @@ -367,14 +352,16 @@
6.98 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \
6.99 \ Crypt (shrK B) {|NB, Key K|}|} \
6.100 \ : set evs)";
6.101 +by (asm_full_simp_tac (simpset() addsimps []) 1);
6.102 by (parts_induct_tac 1);
6.103 by (Blast_tac 1);
6.104 (*OR1: it cannot be a new Nonce, contradiction.*)
6.105 by (Blast_tac 1);
6.106 (*OR4*)
6.107 by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 2);
6.108 -(*OR3*)
6.109 -by (blast_tac (claset() addDs [unique_NB] addEs [nonce_OR1_OR2_E]) 1);
6.110 +(*OR3: needs AddSEs [MPair_parts] or it takes forever!*)
6.111 +by (blast_tac (claset() addDs [unique_NB]
6.112 + addEs [nonce_OR1_OR2_E]) 1);
6.113 qed_spec_mp "NB_Crypt_imp_Server_msg";
6.114
6.115
6.116 @@ -431,5 +418,6 @@
6.117 \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
6.118 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
6.119 \ : set evs";
6.120 -by (blast_tac (claset() addSDs [A_trusts_OR4, OR3_imp_OR2]) 1);
6.121 +by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj]
6.122 + addSDs [A_trusts_OR4, OR3_imp_OR2]) 1);
6.123 qed "A_auths_B";
7.1 --- a/src/HOL/Auth/OtwayRees_AN.ML Fri Feb 16 08:27:17 2001 +0100
7.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Feb 16 13:25:08 2001 +0100
7.3 @@ -12,9 +12,8 @@
7.4 IEEE Trans. SE 22 (1), 1996
7.5 *)
7.6
7.7 -AddEs knows_Spy_partsEs;
7.8 -AddDs [impOfSubs analz_subset_parts];
7.9 -AddDs [impOfSubs Fake_parts_insert];
7.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
7.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
7.12
7.13
7.14 (*A "possibility property": there are traces that reach the end*)
8.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Feb 16 08:27:17 2001 +0100
8.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Feb 16 13:25:08 2001 +0100
8.3 @@ -15,10 +15,8 @@
8.4 indicates the possibility of this attack.
8.5 *)
8.6
8.7 -AddEs knows_Spy_partsEs;
8.8 -AddDs [impOfSubs analz_subset_parts];
8.9 -AddDs [impOfSubs Fake_parts_insert];
8.10 -
8.11 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
8.12 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
8.13
8.14 (*A "possibility property": there are traces that reach the end*)
8.15 Goal "[| A ~= B; B ~= Server |] \
8.16 @@ -107,12 +105,7 @@
8.17 (*OR2, OR3*)
8.18 by (ALLGOALS Blast_tac);
8.19 qed_spec_mp "new_keys_not_used";
8.20 -
8.21 -bind_thm ("new_keys_not_analzd",
8.22 - [analz_subset_parts RS keysFor_mono,
8.23 - new_keys_not_used] MRS contra_subsetD);
8.24 -
8.25 -Addsimps [new_keys_not_used, new_keys_not_analzd];
8.26 +Addsimps [new_keys_not_used];
8.27
8.28
8.29
9.1 --- a/src/HOL/Auth/Recur.ML Fri Feb 16 08:27:17 2001 +0100
9.2 +++ b/src/HOL/Auth/Recur.ML Fri Feb 16 13:25:08 2001 +0100
9.3 @@ -8,9 +8,8 @@
9.4
9.5 Pretty.setdepth 30;
9.6
9.7 -AddEs spies_partsEs;
9.8 -AddDs [impOfSubs analz_subset_parts];
9.9 -AddDs [impOfSubs Fake_parts_insert];
9.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
9.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
9.12
9.13
9.14 (** Possibility properties: traces that reach the end
9.15 @@ -343,9 +342,7 @@
9.16 by (Asm_full_simp_tac 1);
9.17 (*by unicity, either B=Aa or B=A', a contradiction if B \\<in> bad*)
9.18 by (blast_tac
9.19 - (claset() addSEs [MPair_parts]
9.20 - addDs [parts.Body,
9.21 - respond_certificate RSN (2, unique_session_keys)]) 1);
9.22 + (claset() addDs [respond_certificate RSN (2, unique_session_keys)]) 1);
9.23 qed_spec_mp "respond_Spy_not_see_session_key";
9.24
9.25
9.26 @@ -371,7 +368,6 @@
9.27 by (safe_tac (claset() delrules [impCE]));
9.28 (*RA3, case 2: K is an old key*)
9.29 by (blast_tac (claset() addSDs [resp_analz_insert]
9.30 - addSEs partsEs
9.31 addDs [Key_in_parts_respond]) 2);
9.32 (*RA3, case 1: use lemma previously proved by induction*)
9.33 by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN
10.1 --- a/src/HOL/Auth/TLS.ML Fri Feb 16 08:27:17 2001 +0100
10.2 +++ b/src/HOL/Auth/TLS.ML Fri Feb 16 13:25:08 2001 +0100
10.3 @@ -17,9 +17,8 @@
10.4 rollback attacks).
10.5 *)
10.6
10.7 -AddEs spies_partsEs;
10.8 -AddDs [impOfSubs analz_subset_parts];
10.9 -AddDs [impOfSubs Fake_parts_insert];
10.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
10.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
10.12
10.13 (*Automatically unfold the definition of "certificate"*)
10.14 Addsimps [certificate_def];
10.15 @@ -129,10 +128,8 @@
10.16 needless information about analz (insert X (spies evs)) *)
10.17 fun parts_induct_tac i =
10.18 etac tls.induct i
10.19 - THEN
10.20 - REPEAT (FIRSTGOAL analz_mono_contra_tac)
10.21 - THEN
10.22 - fast_tac (claset() addss (simpset())) i THEN
10.23 + THEN REPEAT (FIRSTGOAL analz_mono_contra_tac)
10.24 + THEN Force_tac i THEN
10.25 ALLGOALS Asm_simp_tac;
10.26
10.27
10.28 @@ -438,14 +435,14 @@
10.29 \ Nonce PMS ~: analz (spies evs)";
10.30 by (analz_induct_tac 1); (*4 seconds*)
10.31 (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
10.32 -by (REPEAT (fast_tac (claset() addss (simpset())) 6));
10.33 +by (REPEAT (Force_tac 6));
10.34 (*ClientHello, ServerHello, ClientKeyExch, ServerResume:
10.35 mostly freshness reasoning*)
10.36 -by (REPEAT (blast_tac (claset() addSEs partsEs
10.37 +by (REPEAT (blast_tac (claset() addSDs [parts.Body]
10.38 addDs [Notes_Crypt_parts_spies,
10.39 Says_imp_spies RS analz.Inj]) 3));
10.40 (*SpyKeys*)
10.41 -by (fast_tac (claset() addss (simpset())) 2);
10.42 +by (Force_tac 2);
10.43 (*Fake*)
10.44 by (spy_analz_tac 1);
10.45 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
10.46 @@ -469,7 +466,7 @@
10.47 (*Fake*)
10.48 by (spy_analz_tac 1);
10.49 (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
10.50 -by (REPEAT (blast_tac (claset() addSEs partsEs
10.51 +by (REPEAT (blast_tac (claset() addSDs [parts.Body]
10.52 addDs [Notes_Crypt_parts_spies,
10.53 Says_imp_spies RS analz.Inj]) 1));
10.54 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
10.55 @@ -578,7 +575,6 @@
10.56 \ X : parts (spies evs) --> Says B A X : set evs";
10.57 by (hyp_subst_tac 1);
10.58 by (analz_induct_tac 1); (*7 seconds*)
10.59 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
10.60 by (ALLGOALS Clarify_tac);
10.61 (*ClientKeyExch*)
10.62 by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
11.1 --- a/src/HOL/Auth/WooLam.ML Fri Feb 16 08:27:17 2001 +0100
11.2 +++ b/src/HOL/Auth/WooLam.ML Fri Feb 16 13:25:08 2001 +0100
11.3 @@ -10,9 +10,8 @@
11.4 IEEE Trans. S.E. 22(1), 1996, pages 6-15.
11.5 *)
11.6
11.7 -AddEs spies_partsEs;
11.8 -AddDs [impOfSubs analz_subset_parts];
11.9 -AddDs [impOfSubs Fake_parts_insert];
11.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
11.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
11.12
11.13
11.14 (*A "possibility property": there are traces that reach the end*)
12.1 --- a/src/HOL/Auth/Yahalom.ML Fri Feb 16 08:27:17 2001 +0100
12.2 +++ b/src/HOL/Auth/Yahalom.ML Fri Feb 16 13:25:08 2001 +0100
12.3 @@ -58,8 +58,8 @@
12.4 (*For Oops*)
12.5 Goal "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs \
12.6 \ ==> K : parts (knows Spy evs)";
12.7 -by (blast_tac (claset() addSEs partsEs
12.8 - addSDs [Says_imp_knows_Spy RS parts.Inj]) 1);
12.9 +by (blast_tac (claset() addSDs [parts.Body,
12.10 + Says_imp_knows_Spy RS parts.Inj]) 1);
12.11 qed "YM4_Key_parts_knows_Spy";
12.12
12.13 (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
12.14 @@ -439,7 +439,7 @@
12.15 by (Fake_parts_insert_tac 1);
12.16 by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj]
12.17 addSIs [parts_insertI]
12.18 - addSEs partsEs) 1);
12.19 + addSDs [parts.Body]) 1);
12.20 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
12.21
12.22 (*more readable version cited in Yahalom paper*)
12.23 @@ -475,7 +475,7 @@
12.24 addSEs [no_nonce_YM1_YM2, MPair_parts]
12.25 addDs [Gets_imp_Says, Says_unique_NB]) 4);
12.26 (*YM2: similar freshness reasoning*)
12.27 -by (blast_tac (claset() addSEs partsEs
12.28 +by (blast_tac (claset() addSDs [parts.Body]
12.29 addDs [Gets_imp_Says,
12.30 Says_imp_knows_Spy RS analz.Inj,
12.31 impOfSubs analz_subset_parts]) 3);
13.1 --- a/src/HOL/Auth/Yahalom2.ML Fri Feb 16 08:27:17 2001 +0100
13.2 +++ b/src/HOL/Auth/Yahalom2.ML Fri Feb 16 13:25:08 2001 +0100
13.3 @@ -12,9 +12,8 @@
13.4 Proc. Royal Soc. 426 (1989)
13.5 *)
13.6
13.7 -AddEs knows_Spy_partsEs;
13.8 -AddDs [impOfSubs analz_subset_parts];
13.9 -AddDs [impOfSubs Fake_parts_insert];
13.10 +AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
13.11 +AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
13.12
13.13
13.14 (*A "possibility property": there are traces that reach the end*)
13.15 @@ -57,8 +56,8 @@
13.16 (*For Oops*)
13.17 Goal "Says Server A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs \
13.18 \ ==> K : parts (knows Spy evs)";
13.19 -by (blast_tac (claset() addSEs partsEs
13.20 - addSDs [Says_imp_knows_Spy RS parts.Inj]) 1);
13.21 +by (blast_tac (claset() addSDs [parts.Body,
13.22 + Says_imp_knows_Spy RS parts.Inj]) 1);
13.23 qed "YM4_Key_parts_knows_Spy";
13.24
13.25 (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
13.26 @@ -361,7 +360,7 @@
13.27 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
13.28 (*yes: delete a useless induction hypothesis; apply unicity of session keys*)
13.29 by (thin_tac "?P-->?Q" 1);
13.30 -by (ftac Gets_imp_Says 1 THEN assume_tac 1);
13.31 +by (dtac Gets_imp_Says 1 THEN assume_tac 1);
13.32 by (not_bad_tac "Aa" 1);
13.33 by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
13.34 addDs [unique_session_keys]) 1);