Simplified proofs using rewrites for f``A where f is injective
authorpaulson
Tue Dec 16 15:17:26 1997 +0100 (1997-12-16)
changeset 442221238c9d363e
parent 4421 88639289be39
child 4423 a129b817b58a
Simplified proofs using rewrites for f``A where f is injective
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Dec 16 15:15:38 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Tue Dec 16 15:17:26 1997 +0100
     1.3 @@ -18,11 +18,19 @@
     1.4  AddIffs atomic.inject;
     1.5  AddIffs msg.inject;
     1.6  
     1.7 -(*Holds because Friend is injective: thus cannot prove for all f*)
     1.8 +(*Equations hold because constructors are injective; cannot prove for all f*)
     1.9  goal thy "(Friend x : Friend``A) = (x:A)";
    1.10  by (Auto_tac());
    1.11  qed "Friend_image_eq";
    1.12 -Addsimps [Friend_image_eq];
    1.13 +
    1.14 +goal thy "(Key x : Key``A) = (x:A)";
    1.15 +by (Auto_tac());
    1.16 +qed "Key_image_eq";
    1.17 +
    1.18 +goal thy "(Nonce x ~: Key``A)";
    1.19 +by (Auto_tac());
    1.20 +qed "Nonce_Key_image_eq";
    1.21 +Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
    1.22  
    1.23  
    1.24  (** Inverse of keys **)
     2.1 --- a/src/HOL/Auth/NS_Public.ML	Tue Dec 16 15:15:38 1997 +0100
     2.2 +++ b/src/HOL/Auth/NS_Public.ML	Tue Dec 16 15:17:26 1997 +0100
     2.3 @@ -57,9 +57,13 @@
     2.4  qed "Spy_see_priK";
     2.5  Addsimps [Spy_see_priK];
     2.6  
     2.7 +AddDs [impOfSubs analz_subset_parts];
     2.8 +AddDs [Says_imp_spies RS parts.Inj];
     2.9 +AddDs [impOfSubs Fake_parts_insert];
    2.10 +
    2.11  goal thy 
    2.12   "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    2.13 -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    2.14 +by (Auto_tac());
    2.15  qed "Spy_analz_priK";
    2.16  Addsimps [Spy_analz_priK];
    2.17  
    2.18 @@ -135,15 +139,12 @@
    2.19  by (etac rev_mp 1);
    2.20  by (analz_induct_tac 1);
    2.21  (*NS3*)
    2.22 -by (blast_tac (claset() addDs  [Says_imp_spies RS parts.Inj]
    2.23 -                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    2.24 +by (blast_tac (claset() addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    2.25  (*NS2*)
    2.26  by (blast_tac (claset() addSEs [MPair_parts]
    2.27 -		       addDs  [Says_imp_spies RS parts.Inj,
    2.28 -			       parts.Body, unique_NA]) 3);
    2.29 +		        addDs  [parts.Body, unique_NA]) 3);
    2.30  (*NS1*)
    2.31 -by (blast_tac (claset() addSEs spies_partsEs
    2.32 -                       addIs  [impOfSubs analz_subset_parts]) 2);
    2.33 +by (blast_tac (claset() addSEs spies_partsEs) 2);
    2.34  (*Fake*)
    2.35  by (spy_analz_tac 1);
    2.36  qed "Spy_not_see_NA";
    2.37 @@ -166,9 +167,7 @@
    2.38  (*NS1*)
    2.39  by (blast_tac (claset() addSEs spies_partsEs) 2);
    2.40  (*Fake*)
    2.41 -by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
    2.42 -                       addDs  [Spy_not_see_NA, 
    2.43 -			       impOfSubs analz_subset_parts]) 1);
    2.44 +by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
    2.45  qed "A_trusts_NS2";
    2.46  
    2.47  (*If the encrypted message appears then it originated with Alice in NS1*)
    2.48 @@ -198,7 +197,8 @@
    2.49  by (etac rev_mp 1);
    2.50  by (parts_induct_tac 1);
    2.51  by (ALLGOALS
    2.52 -    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
    2.53 +    (asm_simp_tac (simpset() addsimps [all_conj_distrib, 
    2.54 +				       parts_insert_spies])));
    2.55  (*NS2*)
    2.56  by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
    2.57  (*Fake*)
    2.58 @@ -228,18 +228,18 @@
    2.59  by (etac rev_mp 1);
    2.60  by (analz_induct_tac 1);
    2.61  (*NS3*)
    2.62 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
    2.63 +by (blast_tac (claset() addDs [unique_NB]) 4);
    2.64  (*NS2: by freshness and unicity of NB*)
    2.65 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
    2.66 -                       addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
    2.67 -                       addEs partsEs
    2.68 -		       addIs [impOfSubs analz_subset_parts]) 3);
    2.69 +by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
    2.70 +                        addEs partsEs) 3);
    2.71  (*NS1*)
    2.72  by (blast_tac (claset() addSEs spies_partsEs) 2);
    2.73  (*Fake*)
    2.74  by (spy_analz_tac 1);
    2.75  qed "Spy_not_see_NB";
    2.76  
    2.77 +AddDs [Spy_not_see_NB];
    2.78 +
    2.79  
    2.80  (*Authentication for B: if he receives message 3 and has used NB
    2.81    in message 2, then A has sent message 3.*)
    2.82 @@ -254,15 +254,12 @@
    2.83  by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
    2.84  by (parts_induct_tac 1);
    2.85  by (ALLGOALS Clarify_tac);
    2.86 -(*NS3: because NB determines A (this use of unique_NB is more robust) *)
    2.87 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Spy_not_see_NB]
    2.88 -			addIs [unique_NB RS conjunct1]) 3);
    2.89 +(*NS3: because NB determines A*)
    2.90 +by (blast_tac (claset() addDs [unique_NB]) 3);
    2.91  (*NS1: by freshness*)
    2.92  by (blast_tac (claset() addSEs spies_partsEs) 2);
    2.93  (*Fake*)
    2.94 -by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
    2.95 -                        addDs  [Spy_not_see_NB, 
    2.96 -			        impOfSubs analz_subset_parts]) 1);
    2.97 +by (Blast_tac 1);
    2.98  qed "B_trusts_NS3";
    2.99  
   2.100  
   2.101 @@ -288,13 +285,10 @@
   2.102  by (ALLGOALS Asm_simp_tac);
   2.103  by (ALLGOALS Clarify_tac);
   2.104  (*NS3: because NB determines A and NA*)
   2.105 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
   2.106 -                               Spy_not_see_NB, unique_NB]) 3);
   2.107 +by (blast_tac (claset() addDs [unique_NB]) 3);
   2.108  (*NS1*)
   2.109  by (blast_tac (claset() addSEs spies_partsEs) 2);
   2.110  (*Fake*)
   2.111 -by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
   2.112 -                        addDs  [Spy_not_see_NB, 
   2.113 -			        impOfSubs analz_subset_parts]) 1);
   2.114 +by (Blast_tac 1);
   2.115  qed "B_trusts_protocol";
   2.116  
     3.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Dec 16 15:15:38 1997 +0100
     3.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Dec 16 15:17:26 1997 +0100
     3.3 @@ -214,9 +214,7 @@
     3.4  (*Takes 9 secs*)
     3.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     3.6  (*Fake*) 
     3.7 -by (spy_analz_tac 2);
     3.8 -(*Base*)
     3.9 -by (Blast_tac 1);
    3.10 +by (spy_analz_tac 1);
    3.11  qed_spec_mp "analz_image_freshK";
    3.12  
    3.13  
     4.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Dec 16 15:15:38 1997 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Dec 16 15:17:26 1997 +0100
     4.3 @@ -173,9 +173,7 @@
     4.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     4.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     4.6  (*Fake*) 
     4.7 -by (spy_analz_tac 2);
     4.8 -(*Base*)
     4.9 -by (Blast_tac 1);
    4.10 +by (spy_analz_tac 1);
    4.11  qed_spec_mp "analz_image_freshK";
    4.12  
    4.13  
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 16 15:15:38 1997 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 16 15:17:26 1997 +0100
     5.3 @@ -165,9 +165,7 @@
     5.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     5.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     5.6  (*Fake*) 
     5.7 -by (spy_analz_tac 2);
     5.8 -(*Base*)
     5.9 -by (Blast_tac 1);
    5.10 +by (spy_analz_tac 1);
    5.11  qed_spec_mp "analz_image_freshK";
    5.12  
    5.13  
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 16 15:15:38 1997 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 16 15:17:26 1997 +0100
     6.3 @@ -176,9 +176,7 @@
     6.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     6.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     6.6  (*Fake*) 
     6.7 -by (spy_analz_tac 2);
     6.8 -(*Base*)
     6.9 -by (Blast_tac 1);
    6.10 +by (spy_analz_tac 1);
    6.11  qed_spec_mp "analz_image_freshK";
    6.12  
    6.13  
     7.1 --- a/src/HOL/Auth/Public.ML	Tue Dec 16 15:15:38 1997 +0100
     7.2 +++ b/src/HOL/Auth/Public.ML	Tue Dec 16 15:17:26 1997 +0100
     7.3 @@ -34,6 +34,24 @@
     7.4  
     7.5  AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
     7.6  
     7.7 +
     7.8 +(** "Image" equations that hold for injective functions **)
     7.9 +
    7.10 +goal thy "(invKey x : invKey``A) = (x:A)";
    7.11 +by (Auto_tac());
    7.12 +qed "invKey_image_eq";
    7.13 +
    7.14 +(*holds because invKey is injective*)
    7.15 +goal thy "(pubK x : pubK``A) = (x:A)";
    7.16 +by (Auto_tac());
    7.17 +qed "pubK_image_eq";
    7.18 +
    7.19 +goal thy "(priK x ~: pubK``A)";
    7.20 +by (Auto_tac());
    7.21 +qed "priK_pubK_image_eq";
    7.22 +Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
    7.23 +
    7.24 +
    7.25  (** Rewrites should not refer to  initState(Friend i) 
    7.26      -- not in normal form! **)
    7.27  
     8.1 --- a/src/HOL/Auth/Recur.ML	Tue Dec 16 15:15:38 1997 +0100
     8.2 +++ b/src/HOL/Auth/Recur.ML	Tue Dec 16 15:17:26 1997 +0100
     8.3 @@ -247,8 +247,6 @@
     8.4  by (ALLGOALS 
     8.5      (asm_simp_tac
     8.6       (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
     8.7 -(*Base*)
     8.8 -by (Blast_tac 1);
     8.9  (*Fake*) 
    8.10  by (spy_analz_tac 1);
    8.11  val raw_analz_image_freshK = result();
     9.1 --- a/src/HOL/Auth/TLS.ML	Tue Dec 16 15:15:38 1997 +0100
     9.2 +++ b/src/HOL/Auth/TLS.ML	Tue Dec 16 15:17:26 1997 +0100
     9.3 @@ -197,14 +197,14 @@
     9.4      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     9.5      ALLGOALS (asm_simp_tac 
     9.6                (simpset() addcongs [if_weak_cong]
     9.7 -                        addsimps (expand_ifs@pushes)
     9.8 -                        addsplits [expand_if]))  THEN
     9.9 +                         addsimps (expand_ifs@pushes)
    9.10 +                         addsplits [expand_if]))  THEN
    9.11      (*Remove instances of pubK B:  the Spy already knows all public keys.
    9.12        Combining the two simplifier calls makes them run extremely slowly.*)
    9.13      ALLGOALS (asm_simp_tac 
    9.14                (simpset() addcongs [if_weak_cong]
    9.15 -			addsimps [insert_absorb]
    9.16 -                        addsplits [expand_if]));
    9.17 +			 addsimps [insert_absorb]
    9.18 +                         addsplits [expand_if]));
    9.19  
    9.20  
    9.21  (*** Properties of items found in Notes ***)
    9.22 @@ -228,7 +228,7 @@
    9.23  by (blast_tac (claset() addIs [parts_insertI]) 1);
    9.24  (*Client, Server Accept*)
    9.25  by (REPEAT (blast_tac (claset() addSEs spies_partsEs
    9.26 -                               addSDs [Notes_Crypt_parts_spies]) 1));
    9.27 +                                addSDs [Notes_Crypt_parts_spies]) 1));
    9.28  qed "Notes_master_imp_Crypt_PMS";
    9.29  
    9.30  (*Compared with the theorem above, both premise and conclusion are stronger*)
    9.31 @@ -380,9 +380,7 @@
    9.32      (asm_simp_tac (analz_image_keys_ss
    9.33  		   addsimps (certificate_def::keys_distinct))));
    9.34  (*Fake*) 
    9.35 -by (spy_analz_tac 2);
    9.36 -(*Base*)
    9.37 -by (Blast_tac 1);
    9.38 +by (spy_analz_tac 1);
    9.39  qed_spec_mp "analz_image_priK";
    9.40  
    9.41  
    9.42 @@ -412,16 +410,14 @@
    9.43  by (ClientKeyExch_tac 7);
    9.44  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    9.45  by (REPEAT_FIRST (rtac analz_image_keys_lemma));
    9.46 -by (ALLGOALS    (*15 seconds*)
    9.47 +by (ALLGOALS    (*18 seconds*)
    9.48      (asm_simp_tac (analz_image_keys_ss 
    9.49  		   addsimps (expand_ifs@pushes)
    9.50  		   addsimps [range_sessionkeys_not_priK, 
    9.51                               analz_image_priK, certificate_def])));
    9.52  by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
    9.53  (*Fake*) 
    9.54 -by (spy_analz_tac 2);
    9.55 -(*Base*)
    9.56 -by (Blast_tac 1);
    9.57 +by (spy_analz_tac 1);
    9.58  qed_spec_mp "analz_image_keys";
    9.59  
    9.60  (*Knowing some session keys is no help in getting new nonces*)
    9.61 @@ -542,7 +538,7 @@
    9.62  by (Blast_tac 3);
    9.63  (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
    9.64  by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
    9.65 -			       Says_imp_spies RS analz.Inj]) 2);
    9.66 +				Says_imp_spies RS analz.Inj]) 2);
    9.67  (*Fake*)
    9.68  by (spy_analz_tac 1);
    9.69  (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
    9.70 @@ -659,7 +655,7 @@
    9.71  \            Notes A {|Agent B, Nonce PMS|} : set evs --> \
    9.72  \            X : parts (spies evs) --> Says B A X : set evs";
    9.73  by (hyp_subst_tac 1);
    9.74 -by (analz_induct_tac 1);        (*22 seconds*)
    9.75 +by (analz_induct_tac 1);        (*26 seconds*)
    9.76  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    9.77  (*proves ServerResume*)
    9.78  by (ALLGOALS Clarify_tac);
    9.79 @@ -668,7 +664,7 @@
    9.80  (*Fake: the Spy doesn't have the critical session key!*)
    9.81  by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
    9.82  by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
    9.83 -				     not_parts_not_analz]) 2);
    9.84 +				      not_parts_not_analz]) 2);
    9.85  by (Fake_parts_insert_tac 1);
    9.86  val lemma = normalize_thm [RSmp] (result());
    9.87  
    9.88 @@ -731,7 +727,7 @@
    9.89  \           evs : tls;  A ~: bad;  B ~: bad |]          \
    9.90  \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
    9.91  by (blast_tac (claset() addIs [lemma]
    9.92 -                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
    9.93 +                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
    9.94  qed_spec_mp "TrustServerMsg";
    9.95  
    9.96  
    9.97 @@ -760,7 +756,7 @@
    9.98  (*Fake: the Spy doesn't have the critical session key!*)
    9.99  by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   9.100  by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   9.101 -				     not_parts_not_analz]) 2);
   9.102 +				      not_parts_not_analz]) 2);
   9.103  by (Fake_parts_insert_tac 1);
   9.104  val lemma = normalize_thm [RSmp] (result());
   9.105  
    10.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Dec 16 15:15:38 1997 +0100
    10.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Dec 16 15:17:26 1997 +0100
    10.3 @@ -165,9 +165,7 @@
    10.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
    10.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    10.6  (*Fake*) 
    10.7 -by (spy_analz_tac 2);
    10.8 -(*Base*)
    10.9 -by (Blast_tac 1);
   10.10 +by (spy_analz_tac 1);
   10.11  qed_spec_mp "analz_image_freshK";
   10.12  
   10.13  goal thy
   10.14 @@ -386,11 +384,9 @@
   10.15  		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
   10.16  		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
   10.17  		 Says_Server_KeyWithNonce])));
   10.18 -(*Base*)
   10.19 -by (Blast_tac 1);
   10.20  (*Fake*) 
   10.21  by (spy_analz_tac 1);
   10.22 -(*YM4*)  (** LEVEL 7 **)
   10.23 +(*YM4*)  (** LEVEL 6 **)
   10.24  by (not_bad_tac "A" 1);
   10.25  by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   10.26      THEN REPEAT (assume_tac 1));
    11.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Dec 16 15:15:38 1997 +0100
    11.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Dec 16 15:17:26 1997 +0100
    11.3 @@ -167,9 +167,7 @@
    11.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
    11.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    11.6  (*Fake*) 
    11.7 -by (spy_analz_tac 2);
    11.8 -(*Base*)
    11.9 -by (Blast_tac 1);
   11.10 +by (spy_analz_tac 1);
   11.11  qed_spec_mp "analz_image_freshK";
   11.12  
   11.13  goal thy