--- a/src/HOL/Auth/Message.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Message.thy Thu Mar 29 10:44:37 2001 +0200
@@ -10,10 +10,6 @@
theory Message = Main
files ("Message_lemmas.ML"):
-(*Eliminates a commonly-occurring expression*)
-lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
-by blast
-
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A Un (B Un A) = B Un A"
by blast
@@ -31,8 +27,8 @@
that of a public key is the private key and vice versa*)
constdefs
- isSymKey :: "key=>bool"
- "isSymKey K == (invKey K = K)"
+ symKeys :: "key set"
+ "symKeys == {K. invKey K = K}"
datatype (*We allow any number of friendly agents*)
agent = Server | Friend nat | Spy
--- a/src/HOL/Auth/Message_lemmas.ML Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Message_lemmas.ML Thu Mar 29 10:44:37 2001 +0200
@@ -14,7 +14,7 @@
val analz_mono = thm "analz_mono";
val synth_mono = thm "synth_mono";
val HPair_def = thm "HPair_def";
-val isSymKey_def = thm "isSymKey_def";
+val symKeys_def = thm "symKeys_def";
structure parts =
struct
--- a/src/HOL/Auth/NS_Public.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/NS_Public.thy Thu Mar 29 10:44:37 2001 +0200
@@ -40,8 +40,6 @@
\<in> set evs3\<rbrakk>
\<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
- (*No Oops message. Should there be one?*)
-
declare knows_Spy_partsEs [elim]
declare analz_subset_parts [THEN subsetD, dest]
declare Fake_parts_insert [THEN subsetD, dest]
--- a/src/HOL/Auth/NS_Public_Bad.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Mar 29 10:44:37 2001 +0200
@@ -43,8 +43,6 @@
Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
\<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
- (*No Oops message. Should there be one?*)
-
declare knows_Spy_partsEs [elim]
declare analz_subset_parts [THEN subsetD, dest]
declare Fake_parts_insert [THEN subsetD, dest]
--- a/src/HOL/Auth/OtwayRees.ML Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Mar 29 10:44:37 2001 +0200
@@ -18,7 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
Goal "B \\<noteq> Server \
-\ ==> \\<exists>NA K. \\<exists>evs \\<in> otway. \
+\ ==> \\<exists>K. \\<exists>evs \\<in> otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ \\<in> set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
--- a/src/HOL/Auth/OtwayRees.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Mar 29 10:44:37 2001 +0200
@@ -60,8 +60,8 @@
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
- Need B ~= Server because we allow messages to self.*)
- OR4 "[| evs4 \\<in> otway; B ~= Server;
+ Need B \\<noteq> Server because we allow messages to self.*)
+ OR4 "[| evs4 \\<in> otway; B \\<noteq> Server;
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
--- a/src/HOL/Auth/OtwayRees_AN.ML Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Mar 29 10:44:37 2001 +0200
@@ -18,7 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
Goal "B \\<noteq> Server \
-\ ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway. \
+\ ==> \\<exists>K. \\<exists>evs \\<in> otway. \
\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
\ \\<in> set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
--- a/src/HOL/Auth/OtwayRees_AN.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Mar 29 10:44:37 2001 +0200
@@ -58,8 +58,8 @@
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
- Need B ~= Server because we allow messages to self.*)
- OR4 "[| evs4 \\<in> otway; B ~= Server;
+ Need B \\<noteq> Server because we allow messages to self.*)
+ OR4 "[| evs4 \\<in> otway; B \\<noteq> Server;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \\<in>set evs4;
Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
\\<in>set evs4 |]
--- a/src/HOL/Auth/Public_lemmas.ML Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Public_lemmas.ML Thu Mar 29 10:44:37 2001 +0200
@@ -24,20 +24,24 @@
AddIffs [priK_inj_eq];
AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
-Goalw [isSymKey_def] "~ isSymKey (pubK A)";
+Goalw [symKeys_def] "pubK A \\<notin> symKeys";
by (Simp_tac 1);
-qed "not_isSymKey_pubK";
+qed "not_symKeys_pubK";
-Goalw [isSymKey_def] "~ isSymKey (priK A)";
+Goalw [symKeys_def] "priK A \\<notin> symKeys";
by (Simp_tac 1);
-qed "not_isSymKey_priK";
+qed "not_symKeys_priK";
-AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
+AddIffs [not_symKeys_pubK, not_symKeys_priK];
-Goal "[| Crypt K X \\<in> analz H; isSymKey K; Key K \\<in> analz H |] \
+Goal "(K \\<in> symKeys) \\<noteq> (K' \\<in> symKeys) ==> K \\<noteq> K'";
+by (Blast_tac 1);
+qed "symKeys_neq_imp_neq";
+
+Goal "[| Crypt K X \\<in> analz H; K \\<in> symKeys; Key K \\<in> analz H |] \
\ ==> X \\<in> analz H";
-by (auto_tac(claset(), simpset() addsimps [isSymKey_def]));
-qed "analz_isSymKey_Decrypt";
+by (auto_tac(claset(), simpset() addsimps [symKeys_def]));
+qed "analz_symKeys_Decrypt";
(** "Image" equations that hold for injective functions **)
--- a/src/HOL/Auth/Shared.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Mar 29 10:44:37 2001 +0200
@@ -15,7 +15,7 @@
shrK :: "agent => key" (*symmetric keys*)
axioms
- isSym_keys: "isSymKey K" (*All keys are symmetric*)
+ isSym_keys: "K \\<in> symKeys" (*All keys are symmetric*)
inj_shrK: "inj shrK" (*No two agents have the same long-term key*)
primrec
--- a/src/HOL/Auth/Shared_lemmas.ML Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Shared_lemmas.ML Thu Mar 29 10:44:37 2001 +0200
@@ -17,8 +17,11 @@
(*Injectiveness: Agents' long-term keys are distinct.*)
AddIffs [inj_shrK RS inj_eq];
-(* invKey(shrK A) = shrK A *)
-Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
+Goal "invKey K = K";
+by (cut_facts_tac [rewrite_rule [symKeys_def] isSym_keys] 1);
+by Auto_tac;
+qed "invKey_K";
+Addsimps [invKey_K];
Goal "[| Crypt K X \\<in> analz H; Key K \\<in> analz H |] ==> X \\<in> analz H";
@@ -87,11 +90,11 @@
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
from long-term shared keys*)
-Goal "Key K ~: used evs ==> K ~: range shrK";
+Goal "Key K \\<notin> used evs ==> K \\<notin> range shrK";
by (Blast_tac 1);
qed "Key_not_used";
-Goal "Key K ~: used evs ==> shrK B ~= K";
+Goal "Key K \\<notin> used evs ==> shrK B \\<noteq> K";
by (Blast_tac 1);
qed "shrK_neq";
@@ -100,13 +103,13 @@
(*** Fresh nonces ***)
-Goal "Nonce N ~: parts (initState B)";
+Goal "Nonce N \\<notin> parts (initState B)";
by (induct_tac "B" 1);
by Auto_tac;
qed "Nonce_notin_initState";
AddIffs [Nonce_notin_initState];
-Goal "Nonce N ~: used []";
+Goal "Nonce N \\<notin> used []";
by (simp_tac (simpset() addsimps [used_Nil]) 1);
qed "Nonce_notin_used_empty";
Addsimps [Nonce_notin_used_empty];
@@ -115,7 +118,7 @@
(*** Supply fresh nonces for possibility theorems. ***)
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+Goal "EX N. ALL n. N<=n --> Nonce n \\<notin> used evs";
by (induct_tac "evs" 1);
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
@@ -126,12 +129,12 @@
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
val lemma = result();
-Goal "EX N. Nonce N ~: used evs";
+Goal "EX N. Nonce N \\<notin> used evs";
by (rtac (lemma RS exE) 1);
by (Blast_tac 1);
qed "Nonce_supply1";
-Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
+Goal "EX N N'. Nonce N \\<notin> used evs & Nonce N' \\<notin> used evs' & N \\<noteq> N'";
by (cut_inst_tac [("evs","evs")] lemma 1);
by (cut_inst_tac [("evs","evs'")] lemma 1);
by (Clarify_tac 1);
@@ -141,8 +144,8 @@
less_Suc_eq_le]) 1);
qed "Nonce_supply2";
-Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
-\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
+Goal "EX N N' N''. Nonce N \\<notin> used evs & Nonce N' \\<notin> used evs' & \
+\ Nonce N'' \\<notin> used evs'' & N \\<noteq> N' & N' \\<noteq> N'' & N \\<noteq> N''";
by (cut_inst_tac [("evs","evs")] lemma 1);
by (cut_inst_tac [("evs","evs'")] lemma 1);
by (cut_inst_tac [("evs","evs''")] lemma 1);
@@ -154,7 +157,7 @@
less_Suc_eq_le]) 1);
qed "Nonce_supply3";
-Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
+Goal "Nonce (@ N. Nonce N \\<notin> used evs) \\<notin> used evs";
by (rtac (lemma RS exE) 1);
by (rtac someI 1);
by (Blast_tac 1);
@@ -162,12 +165,12 @@
(*** Supply fresh keys for possibility theorems. ***)
-Goal "EX K. Key K ~: used evs";
+Goal "EX K. Key K \\<notin> used evs";
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
by (Blast_tac 1);
qed "Key_supply1";
-Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
+Goal "EX K K'. Key K \\<notin> used evs & Key K' \\<notin> used evs' & K \\<noteq> K'";
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
by (etac exE 1);
by (cut_inst_tac [("evs","evs'")]
@@ -175,8 +178,8 @@
by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
qed "Key_supply2";
-Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
-\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
+Goal "EX K K' K''. Key K \\<notin> used evs & Key K' \\<notin> used evs' & \
+\ Key K'' \\<notin> used evs'' & K \\<noteq> K' & K' \\<noteq> K'' & K \\<noteq> K''";
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
by (etac exE 1);
(*Blast_tac requires instantiation of the keys for some reason*)
@@ -188,7 +191,7 @@
by (Blast_tac 1);
qed "Key_supply3";
-Goal "Key (@ K. Key K ~: used evs) ~: used evs";
+Goal "Key (@ K. Key K \\<notin> used evs) \\<notin> used evs";
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
by (rtac someI 1);
by (Blast_tac 1);
@@ -197,7 +200,7 @@
(*** Tactics for possibility theorems ***)
(*Omitting used_Says makes the tactic much faster: it leaves expressions
- such as Nonce ?N ~: used evs that match Nonce_supply*)
+ such as Nonce ?N \\<notin> used evs that match Nonce_supply*)
fun possibility_tac st = st |>
(REPEAT
(ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets]
@@ -217,7 +220,7 @@
(*** Specialized rewriting for analz_insert_freshK ***)
-Goal "A <= - (range shrK) ==> shrK x ~: A";
+Goal "A <= - (range shrK) ==> shrK x \\<notin> A";
by (Blast_tac 1);
qed "subset_Compl_range";
--- a/src/HOL/Auth/TLS.ML Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/TLS.ML Thu Mar 29 10:44:37 2001 +0200
@@ -27,21 +27,17 @@
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
(* invKey(sessionK x) = sessionK x*)
-Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
+Addsimps [isSym_sessionK, rewrite_rule [symKeys_def] isSym_sessionK];
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
Goal "pubK A \\<noteq> sessionK arg";
-by (rtac notI 1);
-by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
-by (Full_simp_tac 1);
+by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1);
qed "pubK_neq_sessionK";
Goal "priK A \\<noteq> sessionK arg";
-by (rtac notI 1);
-by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
-by (Full_simp_tac 1);
+by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1);
qed "priK_neq_sessionK";
val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
--- a/src/HOL/Auth/TLS.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/TLS.thy Thu Mar 29 10:44:37 2001 +0200
@@ -72,7 +72,7 @@
inj_sessionK "inj sessionK"
(*sessionK makes symmetric keys*)
- isSym_sessionK "isSymKey (sessionK nonces)"
+ isSym_sessionK "sessionK nonces \\<in> symKeys"
consts tls :: event list set