misc tidying; changing the predicate isSymKey to the set symKeys
authorpaulson
Thu Mar 29 10:44:37 2001 +0200 (2001-03-29)
changeset 11230756c5034f08b
parent 11229 f417841385b7
child 11231 30d96882f915
misc tidying; changing the predicate isSymKey to the set symKeys
src/HOL/Auth/Message.thy
src/HOL/Auth/Message_lemmas.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/Public_lemmas.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/Shared_lemmas.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Mar 28 13:40:06 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Mar 29 10:44:37 2001 +0200
     1.3 @@ -10,10 +10,6 @@
     1.4  theory Message = Main
     1.5  files ("Message_lemmas.ML"):
     1.6  
     1.7 -(*Eliminates a commonly-occurring expression*)
     1.8 -lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
     1.9 -by blast
    1.10 -
    1.11  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.12  lemma [simp] : "A Un (B Un A) = B Un A"
    1.13  by blast
    1.14 @@ -31,8 +27,8 @@
    1.15      that of a public key is the private key and vice versa*)
    1.16  
    1.17  constdefs
    1.18 -  isSymKey :: "key=>bool"
    1.19 -  "isSymKey K == (invKey K = K)"
    1.20 +  symKeys :: "key set"
    1.21 +  "symKeys == {K. invKey K = K}"
    1.22  
    1.23  datatype  (*We allow any number of friendly agents*)
    1.24    agent = Server | Friend nat | Spy
     2.1 --- a/src/HOL/Auth/Message_lemmas.ML	Wed Mar 28 13:40:06 2001 +0200
     2.2 +++ b/src/HOL/Auth/Message_lemmas.ML	Thu Mar 29 10:44:37 2001 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4  val analz_mono = thm "analz_mono";
     2.5  val synth_mono = thm "synth_mono";
     2.6  val HPair_def = thm "HPair_def";
     2.7 -val isSymKey_def = thm "isSymKey_def";
     2.8 +val symKeys_def = thm "symKeys_def";
     2.9  
    2.10  structure parts =
    2.11    struct
     3.1 --- a/src/HOL/Auth/NS_Public.thy	Wed Mar 28 13:40:06 2001 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Mar 29 10:44:37 2001 +0200
     3.3 @@ -40,8 +40,6 @@
     3.4                \<in> set evs3\<rbrakk>
     3.5            \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
     3.6  
     3.7 -  (*No Oops message.  Should there be one?*)
     3.8 -
     3.9  declare knows_Spy_partsEs [elim]
    3.10  declare analz_subset_parts [THEN subsetD, dest]
    3.11  declare Fake_parts_insert [THEN subsetD, dest]
     4.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Wed Mar 28 13:40:06 2001 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Mar 29 10:44:37 2001 +0200
     4.3 @@ -43,8 +43,6 @@
     4.4             Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
     4.5            \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
     4.6  
     4.7 -  (*No Oops message.  Should there be one?*)
     4.8 -
     4.9  declare knows_Spy_partsEs [elim]
    4.10  declare analz_subset_parts [THEN subsetD, dest]
    4.11  declare Fake_parts_insert [THEN subsetD, dest]
     5.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Mar 28 13:40:06 2001 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Mar 29 10:44:37 2001 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  
     5.5  (*A "possibility property": there are traces that reach the end*)
     5.6  Goal "B \\<noteq> Server   \
     5.7 -\     ==> \\<exists>NA K. \\<exists>evs \\<in> otway.          \
     5.8 +\     ==> \\<exists>K. \\<exists>evs \\<in> otway.          \
     5.9  \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    5.10  \              \\<in> set evs";
    5.11  by (REPEAT (resolve_tac [exI,bexI] 1));
     6.1 --- a/src/HOL/Auth/OtwayRees.thy	Wed Mar 28 13:40:06 2001 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Mar 29 10:44:37 2001 +0200
     6.3 @@ -60,8 +60,8 @@
     6.4  
     6.5           (*Bob receives the Server's (?) message and compares the Nonces with
     6.6  	   those in the message he previously sent the Server.
     6.7 -           Need B ~= Server because we allow messages to self.*)
     6.8 -    OR4  "[| evs4 \\<in> otway;  B ~= Server;
     6.9 +           Need B \\<noteq> Server because we allow messages to self.*)
    6.10 +    OR4  "[| evs4 \\<in> otway;  B \\<noteq> Server;
    6.11               Says B Server {|Nonce NA, Agent A, Agent B, X', 
    6.12                               Crypt (shrK B)
    6.13                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
     7.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Mar 28 13:40:06 2001 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Mar 29 10:44:37 2001 +0200
     7.3 @@ -18,7 +18,7 @@
     7.4  
     7.5  (*A "possibility property": there are traces that reach the end*)
     7.6  Goal "B \\<noteq> Server   \
     7.7 -\     ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway.                                      \
     7.8 +\     ==> \\<exists>K. \\<exists>evs \\<in> otway.                                      \
     7.9  \          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    7.10  \            \\<in> set evs";
    7.11  by (REPEAT (resolve_tac [exI,bexI] 1));
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Wed Mar 28 13:40:06 2001 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Mar 29 10:44:37 2001 +0200
     8.3 @@ -58,8 +58,8 @@
     8.4  
     8.5           (*Bob receives the Server's (?) message and compares the Nonces with
     8.6  	   those in the message he previously sent the Server.
     8.7 -           Need B ~= Server because we allow messages to self.*)
     8.8 -    OR4  "[| evs4 \\<in> otway;  B ~= Server; 
     8.9 +           Need B \\<noteq> Server because we allow messages to self.*)
    8.10 +    OR4  "[| evs4 \\<in> otway;  B \\<noteq> Server; 
    8.11               Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \\<in>set evs4;
    8.12               Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    8.13                 \\<in>set evs4 |]
     9.1 --- a/src/HOL/Auth/Public_lemmas.ML	Wed Mar 28 13:40:06 2001 +0200
     9.2 +++ b/src/HOL/Auth/Public_lemmas.ML	Thu Mar 29 10:44:37 2001 +0200
     9.3 @@ -24,20 +24,24 @@
     9.4  AddIffs [priK_inj_eq];
     9.5  AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
     9.6  
     9.7 -Goalw [isSymKey_def] "~ isSymKey (pubK A)";
     9.8 +Goalw [symKeys_def] "pubK A \\<notin> symKeys";
     9.9  by (Simp_tac 1);
    9.10 -qed "not_isSymKey_pubK";
    9.11 +qed "not_symKeys_pubK";
    9.12  
    9.13 -Goalw [isSymKey_def] "~ isSymKey (priK A)";
    9.14 +Goalw [symKeys_def] "priK A \\<notin> symKeys";
    9.15  by (Simp_tac 1);
    9.16 -qed "not_isSymKey_priK";
    9.17 +qed "not_symKeys_priK";
    9.18  
    9.19 -AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
    9.20 +AddIffs [not_symKeys_pubK, not_symKeys_priK];
    9.21  
    9.22 -Goal "[| Crypt K X \\<in> analz H;  isSymKey K;  Key K  \\<in> analz H |] \
    9.23 +Goal "(K \\<in> symKeys) \\<noteq> (K' \\<in> symKeys) ==> K \\<noteq> K'";
    9.24 +by (Blast_tac 1); 
    9.25 +qed "symKeys_neq_imp_neq";
    9.26 +
    9.27 +Goal "[| Crypt K X \\<in> analz H;  K \\<in> symKeys;  Key K \\<in> analz H |] \
    9.28  \     ==> X \\<in> analz H";
    9.29 -by (auto_tac(claset(), simpset() addsimps [isSymKey_def]));
    9.30 -qed "analz_isSymKey_Decrypt";
    9.31 +by (auto_tac(claset(), simpset() addsimps [symKeys_def]));
    9.32 +qed "analz_symKeys_Decrypt";
    9.33  
    9.34  
    9.35  (** "Image" equations that hold for injective functions **)
    10.1 --- a/src/HOL/Auth/Shared.thy	Wed Mar 28 13:40:06 2001 +0200
    10.2 +++ b/src/HOL/Auth/Shared.thy	Thu Mar 29 10:44:37 2001 +0200
    10.3 @@ -15,7 +15,7 @@
    10.4    shrK    :: "agent => key"  (*symmetric keys*)
    10.5  
    10.6  axioms
    10.7 -  isSym_keys: "isSymKey K"	(*All keys are symmetric*)
    10.8 +  isSym_keys: "K \\<in> symKeys"	(*All keys are symmetric*)
    10.9    inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
   10.10  
   10.11  primrec
    11.1 --- a/src/HOL/Auth/Shared_lemmas.ML	Wed Mar 28 13:40:06 2001 +0200
    11.2 +++ b/src/HOL/Auth/Shared_lemmas.ML	Thu Mar 29 10:44:37 2001 +0200
    11.3 @@ -17,8 +17,11 @@
    11.4  (*Injectiveness: Agents' long-term keys are distinct.*)
    11.5  AddIffs [inj_shrK RS inj_eq];
    11.6  
    11.7 -(* invKey(shrK A) = shrK A *)
    11.8 -Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
    11.9 +Goal "invKey K = K";
   11.10 +by (cut_facts_tac [rewrite_rule [symKeys_def] isSym_keys] 1);
   11.11 +by Auto_tac;
   11.12 +qed "invKey_K";
   11.13 +Addsimps [invKey_K];
   11.14  
   11.15  
   11.16  Goal "[| Crypt K X \\<in> analz H;  Key K  \\<in> analz H |] ==> X \\<in> analz H";
   11.17 @@ -87,11 +90,11 @@
   11.18  
   11.19  (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   11.20    from long-term shared keys*)
   11.21 -Goal "Key K ~: used evs ==> K ~: range shrK";
   11.22 +Goal "Key K \\<notin> used evs ==> K \\<notin> range shrK";
   11.23  by (Blast_tac 1);
   11.24  qed "Key_not_used";
   11.25  
   11.26 -Goal "Key K ~: used evs ==> shrK B ~= K";
   11.27 +Goal "Key K \\<notin> used evs ==> shrK B \\<noteq> K";
   11.28  by (Blast_tac 1);
   11.29  qed "shrK_neq";
   11.30  
   11.31 @@ -100,13 +103,13 @@
   11.32  
   11.33  (*** Fresh nonces ***)
   11.34  
   11.35 -Goal "Nonce N ~: parts (initState B)";
   11.36 +Goal "Nonce N \\<notin> parts (initState B)";
   11.37  by (induct_tac "B" 1);
   11.38  by Auto_tac;
   11.39  qed "Nonce_notin_initState";
   11.40  AddIffs [Nonce_notin_initState];
   11.41  
   11.42 -Goal "Nonce N ~: used []";
   11.43 +Goal "Nonce N \\<notin> used []";
   11.44  by (simp_tac (simpset() addsimps [used_Nil]) 1);
   11.45  qed "Nonce_notin_used_empty";
   11.46  Addsimps [Nonce_notin_used_empty];
   11.47 @@ -115,7 +118,7 @@
   11.48  (*** Supply fresh nonces for possibility theorems. ***)
   11.49  
   11.50  (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   11.51 -Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   11.52 +Goal "EX N. ALL n. N<=n --> Nonce n \\<notin> used evs";
   11.53  by (induct_tac "evs" 1);
   11.54  by (res_inst_tac [("x","0")] exI 1);
   11.55  by (ALLGOALS (asm_simp_tac
   11.56 @@ -126,12 +129,12 @@
   11.57  by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
   11.58  val lemma = result();
   11.59  
   11.60 -Goal "EX N. Nonce N ~: used evs";
   11.61 +Goal "EX N. Nonce N \\<notin> used evs";
   11.62  by (rtac (lemma RS exE) 1);
   11.63  by (Blast_tac 1);
   11.64  qed "Nonce_supply1";
   11.65  
   11.66 -Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
   11.67 +Goal "EX N N'. Nonce N \\<notin> used evs & Nonce N' \\<notin> used evs' & N \\<noteq> N'";
   11.68  by (cut_inst_tac [("evs","evs")] lemma 1);
   11.69  by (cut_inst_tac [("evs","evs'")] lemma 1);
   11.70  by (Clarify_tac 1);
   11.71 @@ -141,8 +144,8 @@
   11.72  				      less_Suc_eq_le]) 1);
   11.73  qed "Nonce_supply2";
   11.74  
   11.75 -Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
   11.76 -\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
   11.77 +Goal "EX N N' N''. Nonce N \\<notin> used evs & Nonce N' \\<notin> used evs' & \
   11.78 +\                   Nonce N'' \\<notin> used evs'' & N \\<noteq> N' & N' \\<noteq> N'' & N \\<noteq> N''";
   11.79  by (cut_inst_tac [("evs","evs")] lemma 1);
   11.80  by (cut_inst_tac [("evs","evs'")] lemma 1);
   11.81  by (cut_inst_tac [("evs","evs''")] lemma 1);
   11.82 @@ -154,7 +157,7 @@
   11.83  				      less_Suc_eq_le]) 1);
   11.84  qed "Nonce_supply3";
   11.85  
   11.86 -Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
   11.87 +Goal "Nonce (@ N. Nonce N \\<notin> used evs) \\<notin> used evs";
   11.88  by (rtac (lemma RS exE) 1);
   11.89  by (rtac someI 1);
   11.90  by (Blast_tac 1);
   11.91 @@ -162,12 +165,12 @@
   11.92  
   11.93  (*** Supply fresh keys for possibility theorems. ***)
   11.94  
   11.95 -Goal "EX K. Key K ~: used evs";
   11.96 +Goal "EX K. Key K \\<notin> used evs";
   11.97  by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
   11.98  by (Blast_tac 1);
   11.99  qed "Key_supply1";
  11.100  
  11.101 -Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
  11.102 +Goal "EX K K'. Key K \\<notin> used evs & Key K' \\<notin> used evs' & K \\<noteq> K'";
  11.103  by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
  11.104  by (etac exE 1);
  11.105  by (cut_inst_tac [("evs","evs'")] 
  11.106 @@ -175,8 +178,8 @@
  11.107  by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
  11.108  qed "Key_supply2";
  11.109  
  11.110 -Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
  11.111 -\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
  11.112 +Goal "EX K K' K''. Key K \\<notin> used evs & Key K' \\<notin> used evs' & \
  11.113 +\                      Key K'' \\<notin> used evs'' & K \\<noteq> K' & K' \\<noteq> K'' & K \\<noteq> K''";
  11.114  by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
  11.115  by (etac exE 1);
  11.116  (*Blast_tac requires instantiation of the keys for some reason*)
  11.117 @@ -188,7 +191,7 @@
  11.118  by (Blast_tac 1);
  11.119  qed "Key_supply3";
  11.120  
  11.121 -Goal "Key (@ K. Key K ~: used evs) ~: used evs";
  11.122 +Goal "Key (@ K. Key K \\<notin> used evs) \\<notin> used evs";
  11.123  by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
  11.124  by (rtac someI 1);
  11.125  by (Blast_tac 1);
  11.126 @@ -197,7 +200,7 @@
  11.127  (*** Tactics for possibility theorems ***)
  11.128  
  11.129  (*Omitting used_Says makes the tactic much faster: it leaves expressions
  11.130 -    such as  Nonce ?N ~: used evs that match Nonce_supply*)
  11.131 +    such as  Nonce ?N \\<notin> used evs that match Nonce_supply*)
  11.132  fun possibility_tac st = st |>
  11.133     (REPEAT 
  11.134      (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
  11.135 @@ -217,7 +220,7 @@
  11.136  
  11.137  (*** Specialized rewriting for analz_insert_freshK ***)
  11.138  
  11.139 -Goal "A <= - (range shrK) ==> shrK x ~: A";
  11.140 +Goal "A <= - (range shrK) ==> shrK x \\<notin> A";
  11.141  by (Blast_tac 1);
  11.142  qed "subset_Compl_range";
  11.143  
    12.1 --- a/src/HOL/Auth/TLS.ML	Wed Mar 28 13:40:06 2001 +0200
    12.2 +++ b/src/HOL/Auth/TLS.ML	Thu Mar 29 10:44:37 2001 +0200
    12.3 @@ -27,21 +27,17 @@
    12.4  AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
    12.5  
    12.6  (* invKey(sessionK x) = sessionK x*)
    12.7 -Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
    12.8 +Addsimps [isSym_sessionK, rewrite_rule [symKeys_def] isSym_sessionK];
    12.9  
   12.10  
   12.11  (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
   12.12  
   12.13  Goal "pubK A \\<noteq> sessionK arg";
   12.14 -by (rtac notI 1);
   12.15 -by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
   12.16 -by (Full_simp_tac 1);
   12.17 +by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1);
   12.18  qed "pubK_neq_sessionK";
   12.19  
   12.20  Goal "priK A \\<noteq> sessionK arg";
   12.21 -by (rtac notI 1);
   12.22 -by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
   12.23 -by (Full_simp_tac 1);
   12.24 +by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1);
   12.25  qed "priK_neq_sessionK";
   12.26  
   12.27  val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
    13.1 --- a/src/HOL/Auth/TLS.thy	Wed Mar 28 13:40:06 2001 +0200
    13.2 +++ b/src/HOL/Auth/TLS.thy	Thu Mar 29 10:44:37 2001 +0200
    13.3 @@ -72,7 +72,7 @@
    13.4    inj_sessionK  "inj sessionK"	
    13.5  
    13.6    (*sessionK makes symmetric keys*)
    13.7 -  isSym_sessionK "isSymKey (sessionK nonces)"
    13.8 +  isSym_sessionK "sessionK nonces \\<in> symKeys"
    13.9  
   13.10  
   13.11  consts    tls :: event list set