--- a/src/HOL/Auth/NS_Public.ML Tue Dec 23 11:41:12 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML Tue Dec 23 11:43:48 1997 +0100
@@ -5,6 +5,9 @@
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
Version incorporating Lowe's fix (inclusion of B's identify in round 2).
+
+This version is experimental. It adds many more rules to the claset and even
+replaces Fake_parts_insert_tac by Blast_tac.
*)
open NS_Public;
@@ -12,6 +15,10 @@
set proof_timing;
HOL_quantifiers := false;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
AddIffs [Spy_in_bad];
(*A "possibility property": there are traces that reach the end*)
@@ -53,27 +60,18 @@
goal thy
"!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
-AddDs [impOfSubs analz_subset_parts];
-AddDs [Says_imp_spies RS parts.Inj];
-AddDs [impOfSubs Fake_parts_insert];
-
goal thy
"!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
by (Auto_tac());
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
-goal thy "!!A. [| Key (priK A) : parts (spies evs); \
-\ evs : ns_public |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_priK]) 1);
-qed "Spy_see_priK_D";
-
-bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
-AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
+AddSDs [Spy_see_priK RSN (2, rev_iffD1),
+ Spy_analz_priK RSN (2, rev_iffD1)];
(**** Authenticity properties obtained from NS2 ****)
@@ -88,13 +86,12 @@
by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
-(*NS3*)
-by (blast_tac (claset() addSEs partsEs) 3);
-(*NS2*)
-by (blast_tac (claset() addSEs partsEs) 2);
-by (Fake_parts_insert_tac 1);
+by (ALLGOALS Blast_tac);
qed "no_nonce_NS1_NS2";
+(*Adding it to the claset slows down proofs...*)
+val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE);
+
(*Unicity for NS1: nonce NA identifies agents A and B*)
goal thy
@@ -105,13 +102,14 @@
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
+ (asm_simp_tac (simpset() addsimps [all_conj_distrib,
+ parts_insert_spies])));
(*NS1*)
-by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
+by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2);
(*Fake*)
by (Clarify_tac 1);
by (ex_strip_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
val lemma = result();
goal thy
@@ -127,8 +125,7 @@
(*Tactic for proving secrecy theorems*)
fun analz_induct_tac i =
etac ns_public.induct i THEN
- ALLGOALS (asm_simp_tac
- (simpset() addsplits [expand_if]));
+ ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
@@ -139,12 +136,11 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
+by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
(*NS2*)
-by (blast_tac (claset() addSEs [MPair_parts]
- addDs [parts.Body, unique_NA]) 3);
+by (blast_tac (claset() addDs [unique_NA]) 3);
(*NS1*)
-by (blast_tac (claset() addSEs spies_partsEs) 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
qed "Spy_not_see_NA";
@@ -165,7 +161,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
(*NS1*)
-by (blast_tac (claset() addSEs spies_partsEs) 2);
+by (Blast_tac 2);
(*Fake*)
by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
qed "A_trusts_NS2";
@@ -179,7 +175,7 @@
by (etac rev_mp 1);
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "B_trusts_NS1";
@@ -200,11 +196,11 @@
(asm_simp_tac (simpset() addsimps [all_conj_distrib,
parts_insert_spies])));
(*NS2*)
-by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
+by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2);
(*Fake*)
by (Clarify_tac 1);
by (ex_strip_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
val lemma = result();
goal thy
@@ -218,6 +214,8 @@
by (prove_unique_tac lemma 1);
qed "unique_NB";
+AddDs [unique_NB];
+
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
goal thy
@@ -228,12 +226,11 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-by (blast_tac (claset() addDs [unique_NB]) 4);
+by (Blast_tac 4);
(*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
- addEs partsEs) 3);
+by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
(*NS1*)
-by (blast_tac (claset() addSEs spies_partsEs) 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
qed "Spy_not_see_NB";
@@ -254,12 +251,7 @@
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
by (parts_induct_tac 1);
by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A*)
-by (blast_tac (claset() addDs [unique_NB]) 3);
-(*NS1: by freshness*)
-by (blast_tac (claset() addSEs spies_partsEs) 2);
-(*Fake*)
-by (Blast_tac 1);
+by (ALLGOALS Blast_tac);
qed "B_trusts_NS3";
@@ -284,11 +276,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A and NA*)
-by (blast_tac (claset() addDs [unique_NB]) 3);
-(*NS1*)
-by (blast_tac (claset() addSEs spies_partsEs) 2);
-(*Fake*)
-by (Blast_tac 1);
+(*NS3 holds because NB determines A and NA*)
+by (ALLGOALS Blast_tac);
qed "B_trusts_protocol";
--- a/src/HOL/Auth/NS_Shared.ML Tue Dec 23 11:41:12 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Tue Dec 23 11:43:48 1997 +0100
@@ -15,6 +15,10 @@
set proof_timing;
HOL_quantifiers := false;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -49,13 +53,13 @@
(*For reasoning about the encrypted portion of message NS3*)
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
\ ==> X : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
qed "NS3_msg_in_parts_spies";
goal thy
"!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
\ ==> K : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
qed "Oops_parts_spies";
(*For proving the easier theorems about X ~: parts (spies evs).*)
@@ -74,24 +78,18 @@
goal thy
"!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
"!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
+by (Auto_tac());
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
-\ evs : ns_shared |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
+ Spy_analz_shrK RSN (2, rev_iffD1)];
(*Nobody can have used non-existent keys!*)
@@ -105,7 +103,7 @@
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
addss (simpset())) 1);
(*NS2, NS4, NS5*)
-by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
+by (ALLGOALS (Blast_tac));
qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
@@ -138,7 +136,7 @@
\ : set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "A_trusts_NS2";
@@ -162,7 +160,7 @@
by (case_tac "A : bad" 1);
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
addss (simpset())) 1);
-by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 1);
+by (blast_tac (claset() addSDs [cert_A_form]) 1);
qed "Says_S_message_form";
@@ -191,7 +189,7 @@
\ (Crypt KAB X) : parts (spies evs) & \
\ Key K : parts {X} --> Key K : parts (spies evs)";
by (parts_induct_tac 1);
-(*Deals with Faked messages*)
+(*Fake*)
by (blast_tac (claset() addSEs partsEs
addDs [impOfSubs parts_insert_subset_Un]) 1);
(*Base, NS4 and NS5*)
@@ -242,8 +240,7 @@
(*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 splitup into 4 subgoals*)
- addSEs spies_partsEs) 1);
+by (Blast_tac 1);
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
@@ -278,9 +275,7 @@
(*NS3, replay sub-case*)
by (Blast_tac 4);
(*NS2*)
-by (blast_tac (claset() addSEs spies_partsEs
- addIs [parts_insertI,
- impOfSubs analz_subset_parts]) 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS3, Server sub-case*) (**LEVEL 6 **)
@@ -288,7 +283,7 @@
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
by (assume_tac 2);
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
- Crypt_Spy_analz_bad]) 1);
+ Crypt_Spy_analz_bad]) 1);
by (blast_tac (claset() addDs [unique_session_keys]) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -320,8 +315,6 @@
\ : set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-(*Fake case*)
by (ALLGOALS Blast_tac);
qed "B_trusts_NS3";
@@ -339,7 +332,7 @@
by (parts_induct_tac 1);
(*NS3*)
by (Blast_tac 3);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(*NS2: contradiction from the assumptions
Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *)
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
@@ -348,8 +341,7 @@
(*NS4*)
by (Clarify_tac 1);
by (not_bad_tac "Ba" 1);
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3,
- unique_session_keys]) 1);
+by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
qed "A_trusts_NS4_lemma";
@@ -381,7 +373,7 @@
by (parts_induct_tac 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
by (ALLGOALS Clarify_tac);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(**LEVEL 7**)
(*NS2*)
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
@@ -407,19 +399,18 @@
\ Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
by (parts_induct_tac 1);
(*NS4*)
-by (blast_tac (claset() addSEs spies_partsEs) 4);
+by (Blast_tac 4);
(*NS3*)
-by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 3);
+by (blast_tac (claset() addSDs [cert_A_form]) 3);
(*NS2*)
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
addSDs [Crypt_imp_keysFor]) 2);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(**LEVEL 5**)
(*NS5*)
by (Clarify_tac 1);
by (not_bad_tac "Aa" 1);
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS A_trusts_NS2,
- unique_session_keys]) 1);
+by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
val lemma = result();
--- a/src/HOL/Auth/OtwayRees.ML Tue Dec 23 11:41:12 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Tue Dec 23 11:43:48 1997 +0100
@@ -17,6 +17,10 @@
set proof_timing;
HOL_quantifiers := false;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -45,17 +49,19 @@
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
\ ==> X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+bd (Says_imp_spies RS analz.Inj) 1;
+by (Blast_tac 1);
qed "OR2_analz_spies";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
\ ==> X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+bd (Says_imp_spies RS analz.Inj) 1;
+by (Blast_tac 1);
qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
\ ==> K : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
qed "Oops_parts_spies";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
@@ -85,7 +91,6 @@
goal thy
"!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -96,12 +101,8 @@
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
+ Spy_analz_shrK RSN (2, rev_iffD1)];
(*Nobody can have used non-existent keys!*)
@@ -111,9 +112,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);
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
@@ -201,8 +202,7 @@
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message, and handle this case by contradiction*)
-by (blast_tac (claset() addSEs spies_partsEs
- delrules [conjI] (*no split-up into 4 subgoals*)) 1);
+by (Blast_tac 1);
val lemma = result();
goal thy
@@ -224,7 +224,7 @@
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -236,11 +236,11 @@
\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
\ --> B = B'";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
by (simp_tac (simpset() addsimps [all_conj_distrib]) 1);
(*OR1: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NA = ?y" 1);
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
val lemma = result();
goal thy
@@ -261,11 +261,10 @@
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
\ ~: parts (spies evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (REPEAT (blast_tac (claset() addSEs spies_partsEs
- addSDs [impOfSubs parts_insert_subset_Un]) 1));
+by (ALLGOALS Blast_tac);
qed_spec_mp"no_nonce_OR1_OR2";
+val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE);
(*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!*)
@@ -281,24 +280,19 @@
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
-by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
+by (Blast_tac 1);
(*OR3 and OR4*)
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]
- addEs spies_partsEs) 3);
-(*OR3, two cases*) (** LEVEL 5 **)
-by (blast_tac (claset() addSEs [MPair_parts]
- addSDs [Says_imp_spies RS parts.Inj]
- addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)]
- delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
-by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
- addSEs [MPair_parts]
- addIs [unique_NA]) 1);
+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);
qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -316,8 +310,7 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs";
-by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
- addEs spies_partsEs) 1);
+by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
qed "A_trusts_OR4";
@@ -343,8 +336,7 @@
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (claset() addSEs spies_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -374,7 +366,6 @@
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
\ : set evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -387,11 +378,11 @@
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
\ --> NA = NA' & A = A'";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
by (simp_tac (simpset() addsimps [all_conj_distrib]) 1);
(*OR2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
val lemma = result();
goal thy
@@ -417,20 +408,20 @@
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
-by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1);
+by (Blast_tac 1);
(*OR4*)
-by (blast_tac (claset() addSEs [MPair_parts, Crypt_imp_OR2]) 2);
+by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 2);
(*OR3*)
+(*Provable in 38s by the single command
+ by (blast_tac (claset() addDs [unique_NB] addEs[nonce_OR1_OR2_E]) 1);
+*)
by (safe_tac (claset() delrules [disjCI, impCE]));
-by (blast_tac (claset() delrules [conjI] (*stop split-up*)) 3);
-by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
- addSEs [MPair_parts]
- addDs [unique_NB]) 2);
-by (blast_tac (claset() addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
- addSDs [Says_imp_spies RS parts.Inj]
- delrules [conjI, impCE] (*stop split-up*)) 1);
+by (Blast_tac 3);
+by (blast_tac (claset() addDs [unique_NB]) 2);
+by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
+ delrules [conjI] (*stop split-up*)) 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -447,8 +438,7 @@
\ Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
- addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
qed "B_trusts_OR3";
@@ -465,8 +455,7 @@
\ : set evs)";
by (etac otway.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
- addSEs [MPair_parts, Crypt_imp_OR2]) 3);
+by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 3);
by (ALLGOALS Blast_tac);
bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -482,6 +471,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]
- addSEs [OR3_imp_OR2]) 1);
+by (blast_tac (claset() addSDs [A_trusts_OR4]
+ addSEs [OR3_imp_OR2]) 1);
qed "A_auths_B";
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 23 11:41:12 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 23 11:43:48 1997 +0100
@@ -17,6 +17,10 @@
set proof_timing;
HOL_quantifiers := false;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -45,12 +49,13 @@
goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
\ X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+bd (Says_imp_spies RS analz.Inj) 1;
+by (Blast_tac 1);
qed "OR4_analz_spies";
goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
\ : set evs ==> K : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (Blast_tac 1);
qed "Oops_parts_spies";
(*OR4_analz_spies lets us treat those cases using the same
@@ -75,7 +80,6 @@
goal thy
"!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -86,12 +90,8 @@
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
+ Spy_analz_shrK RSN (2, rev_iffD1)];
(*Nobody can have used non-existent keys!*)
@@ -101,9 +101,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);
(*OR3*)
by (Blast_tac 1);
qed_spec_mp "new_keys_not_used";
@@ -195,8 +195,7 @@
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
(*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() addSEs spies_partsEs
- delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
+by (Blast_tac 1);
val lemma = result();
@@ -227,7 +226,7 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
(*OR3*)
by (Blast_tac 1);
@@ -244,8 +243,7 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs";
-by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]
- addEs spies_partsEs) 1);
+by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
qed "A_trusts_OR4";
@@ -272,8 +270,7 @@
(*OR4*)
by (Blast_tac 3);
(*OR3*)
-by (blast_tac (claset() addSEs spies_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
+by (Blast_tac 2);
(*Fake*)
by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -302,7 +299,7 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
(*OR3*)
by (Blast_tac 1);
@@ -319,6 +316,5 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
- addEs spies_partsEs) 1);
+by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
qed "B_trusts_OR3";
--- a/src/HOL/Auth/WooLam.ML Tue Dec 23 11:41:12 1997 +0100
+++ b/src/HOL/Auth/WooLam.ML Tue Dec 23 11:43:48 1997 +0100
@@ -15,6 +15,10 @@
set proof_timing;
HOL_quantifiers := false;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
(*A "possibility property": there are traces that reach the end*)
goal thy
@@ -62,23 +66,18 @@
goal thy
"!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
goal thy
"!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
+by (Auto_tac());
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
-goal thy "!!A. [| Key (shrK A) : parts (spies evs); \
-\ evs : woolam |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
+ Spy_analz_shrK RSN (2, rev_iffD1)];
(**** Autheticity properties for Woo-Lam ****)
@@ -88,61 +87,53 @@
(*If the encrypted message appears then it originated with Alice*)
goal thy
- "!!evs. [| A ~: bad; evs : woolam |] \
-\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) \
-\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
+ "!!evs. [| Crypt (shrK A) (Nonce NB) : parts (spies evs); \
+\ A ~: bad; evs : woolam |] \
+\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
+by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "NB_Crypt_imp_Alice_msg";
+by (ALLGOALS Blast_tac);
+qed "NB_Crypt_imp_Alice_msg";
(*Guarantee for Server: if it gets a message containing a certificate from
Alice, then she originated that certificate. But we DO NOT know that B
ever saw it: the Spy may have rerouted the message to the Server.*)
goal thy
- "!!evs. [| A ~: bad; evs : woolam; \
-\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
-\ : set evs |] \
+ "!!evs. [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
+\ : set evs; \
+\ A ~: bad; evs : woolam |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]
- addSEs [MPair_parts]
- addDs [Says_imp_spies RS parts.Inj]) 1);
+by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1);
qed "Server_trusts_WL4";
+AddDs [Server_trusts_WL4];
+
(*** WL5 ***)
(*Server sent WL5 only if it received the right sort of message*)
goal thy
- "!!evs. evs : woolam ==> \
-\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs \
-\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
-\ : set evs)";
+ "!!evs. [| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
+\ evs : woolam |] \
+\ ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
+\ : set evs";
+by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
-bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
+qed "Server_sent_WL5";
+AddDs [Server_sent_WL5];
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: bad; evs : woolam |] \
-\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (spies evs) \
-\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
+ "!!evs. [| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs); \
+\ B ~: bad; evs : woolam |] \
+\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
+by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
-(*Partial guarantee for B: if it gets a message of correct form then the Server
- sent the same message.*)
-goal thy
- "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
-\ B ~: bad; evs : woolam |] \
-\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]
- addDs [Says_imp_spies RS parts.Inj]) 1);
-qed "B_got_WL5";
-
(*Guarantee for B. If B gets the Server's certificate then A has encrypted
the nonce using her key. This event can be no older than the nonce itself.
But A may have sent the nonce to some other agent and it could have reached
@@ -151,20 +142,18 @@
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
\ A ~: bad; B ~: bad; evs : woolam |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
-by (blast_tac (claset() addIs [Server_trusts_WL4]
- addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
+by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1);
qed "B_trusts_WL5";
-(*B only issues challenges in response to WL1. Useful??*)
+(*B only issues challenges in response to WL1. Not used.*)
goal thy
- "!!evs. [| B ~= Spy; evs : woolam |] \
-\ ==> Says B A (Nonce NB) : set evs \
-\ --> (EX A'. Says A' B (Agent A) : set evs)";
+ "!!evs. [| Says B A (Nonce NB) : set evs; B ~= Spy; evs : woolam |] \
+\ ==> EX A'. Says A' B (Agent A) : set evs";
+by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
by (ALLGOALS Blast_tac);
-bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
+qed "B_said_WL2";
(**CANNOT be proved because A doesn't know where challenges come from...
@@ -174,7 +163,6 @@
\ Says B A (Nonce NB) : set evs \
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
by Safe_tac;
-by (blast_tac (claset() addSEs partsEs) 1);
**)