Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
authorpaulson
Tue Nov 18 16:37:25 1997 +0100 (1997-11-18)
changeset 4238679a233fb206
parent 4237 fb01353e363b
child 4239 8c98484ef66f
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
src/HOL/Auth/Shared.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Tue Nov 18 16:36:33 1997 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Tue Nov 18 16:37:25 1997 +0100
     1.3 @@ -28,6 +28,11 @@
     1.4  qed "keysFor_parts_initState";
     1.5  Addsimps [keysFor_parts_initState];
     1.6  
     1.7 +goal thy "!!H. Crypt K X : H ==> K : keysFor H";
     1.8 +by (dtac Crypt_imp_invKey_keysFor 1);
     1.9 +by (Asm_full_simp_tac 1);
    1.10 +qed "Crypt_imp_keysFor";
    1.11 +
    1.12  
    1.13  (*** Function "spies" ***)
    1.14  
     2.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Nov 18 16:36:33 1997 +0100
     2.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Nov 18 16:37:25 1997 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
     2.5  \                K : parts (spies evs)";
     2.6  by (blast_tac (claset() addSEs partsEs
     2.7 -                      addSDs [Says_imp_spies RS parts.Inj]) 1);
     2.8 +                        addSDs [Says_imp_spies RS parts.Inj]) 1);
     2.9  qed "YM4_Key_parts_spies";
    2.10  
    2.11  (*For proving the easier theorems about X ~: parts (spies evs).*)
    2.12 @@ -108,9 +108,9 @@
    2.13  (*Fake*)
    2.14  by (best_tac
    2.15        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    2.16 -               addIs  [impOfSubs analz_subset_parts]
    2.17 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    2.18 -               addss  (simpset())) 1);
    2.19 +                addIs  [impOfSubs analz_subset_parts]
    2.20 +                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    2.21 +                addss  (simpset())) 1);
    2.22  (*YM2-4: Because Key K is not fresh, etc.*)
    2.23  by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
    2.24  qed_spec_mp "new_keys_not_used";
    2.25 @@ -196,7 +196,7 @@
    2.26  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    2.27  (*...we assume X is a recent message and handle this case by contradiction*)
    2.28  by (blast_tac (claset() addSEs spies_partsEs
    2.29 -                       delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    2.30 +                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    2.31  val lemma = result();
    2.32  
    2.33  goal thy 
    2.34 @@ -225,13 +225,13 @@
    2.35  by (ALLGOALS
    2.36      (asm_simp_tac 
    2.37       (simpset() addsimps (expand_ifs@pushes)
    2.38 -	       addsimps [analz_insert_eq, analz_insert_freshK])));
    2.39 +	        addsimps [analz_insert_eq, analz_insert_freshK])));
    2.40  (*Oops*)
    2.41  by (blast_tac (claset() addDs [unique_session_keys]) 3);
    2.42  (*YM3*)
    2.43  by (blast_tac (claset() delrules [impCE]
    2.44 -                       addSEs spies_partsEs
    2.45 -                       addIs [impOfSubs analz_subset_parts]) 2);
    2.46 +                        addSEs spies_partsEs
    2.47 +                        addIs [impOfSubs analz_subset_parts]) 2);
    2.48  (*Fake*) 
    2.49  by (spy_analz_tac 1);
    2.50  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    2.51 @@ -308,7 +308,7 @@
    2.52  by (not_bad_tac "A" 1);
    2.53  (*A's certificate guarantees the existence of the Server message*)
    2.54  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
    2.55 -			      A_trusts_YM3]) 1);
    2.56 +			       A_trusts_YM3]) 1);
    2.57  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
    2.58  
    2.59  
    2.60 @@ -451,8 +451,8 @@
    2.61  \        ==> NA' = NA & A' = A & B' = B";
    2.62  by (not_bad_tac "B'" 1);
    2.63  by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
    2.64 -                       addSEs [MPair_parts]
    2.65 -                       addDs  [unique_NB]) 1);
    2.66 +                        addSEs [MPair_parts]
    2.67 +                        addDs  [unique_NB]) 1);
    2.68  qed "Says_unique_NB";
    2.69  
    2.70  
    2.71 @@ -466,8 +466,8 @@
    2.72  by (parts_induct_tac 1);
    2.73  by (Fake_parts_insert_tac 1);
    2.74  by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
    2.75 -                       addSIs [parts_insertI]
    2.76 -                       addSEs partsEs) 1);
    2.77 +                        addSIs [parts_insertI]
    2.78 +                        addSEs partsEs) 1);
    2.79  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
    2.80  
    2.81  (*The Server sends YM3 only in response to YM2.*)
    2.82 @@ -498,19 +498,19 @@
    2.83  by (ALLGOALS
    2.84      (asm_simp_tac 
    2.85       (simpset() addsimps (expand_ifs@pushes)
    2.86 -	       addsimps [analz_insert_eq, analz_insert_freshK])));
    2.87 +	        addsimps [analz_insert_eq, analz_insert_freshK])));
    2.88  (*Prove YM3 by showing that no NB can also be an NA*)
    2.89  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
    2.90 -	               addSEs [MPair_parts]
    2.91 -		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
    2.92 +	                addSEs [MPair_parts]
    2.93 +		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
    2.94      THEN flexflex_tac);
    2.95  (*YM2: similar freshness reasoning*) 
    2.96  by (blast_tac (claset() addSEs partsEs
    2.97 -		       addDs  [Says_imp_spies RS analz.Inj,
    2.98 -			       impOfSubs analz_subset_parts]) 3);
    2.99 +		        addDs  [Says_imp_spies RS analz.Inj,
   2.100 +				impOfSubs analz_subset_parts]) 3);
   2.101  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   2.102  by (blast_tac (claset() addSIs [parts_insertI]
   2.103 -                       addSEs spies_partsEs) 2);
   2.104 +                        addSEs spies_partsEs) 2);
   2.105  (*Fake*)
   2.106  by (spy_analz_tac 1);
   2.107  (** LEVEL 7: YM4 and Oops remain **)
   2.108 @@ -523,7 +523,7 @@
   2.109  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   2.110  (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
   2.111  by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   2.112 -			      impOfSubs Fake_analz_insert]) 1);
   2.113 +			       impOfSubs Fake_analz_insert]) 1);
   2.114  (** LEVEL 14 **)
   2.115  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   2.116    covered by the quantified Oops assumption.*)
   2.117 @@ -535,8 +535,8 @@
   2.118  (*case NB ~= NBa*)
   2.119  by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
   2.120  by (blast_tac (claset() addSEs [MPair_parts]
   2.121 -		       addDs  [Says_imp_spies RS parts.Inj, 
   2.122 -			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   2.123 +		        addDs  [Says_imp_spies RS parts.Inj, 
   2.124 +			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   2.125  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   2.126  
   2.127  
   2.128 @@ -597,7 +597,7 @@
   2.129  by (Blast_tac 2);
   2.130  (*YM3*)
   2.131  by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   2.132 -		      addSEs [MPair_parts]) 1);
   2.133 +		       addSEs [MPair_parts]) 1);
   2.134  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   2.135  
   2.136  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   2.137 @@ -608,7 +608,7 @@
   2.138  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   2.139  \         : set evs";
   2.140  by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   2.141 -		       addEs spies_partsEs) 1);
   2.142 +		        addEs spies_partsEs) 1);
   2.143  qed "YM3_auth_B_to_A";
   2.144  
   2.145  
   2.146 @@ -628,15 +628,15 @@
   2.147  (*Fake*)
   2.148  by (Fake_parts_insert_tac 1);
   2.149  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   2.150 -by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
   2.151 +by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
   2.152  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   2.153  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   2.154  (*yes: apply unicity of session keys*)
   2.155  by (not_bad_tac "Aa" 1);
   2.156  by (blast_tac (claset() addSEs [MPair_parts]
   2.157 -                       addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   2.158 -		       addDs  [Says_imp_spies RS parts.Inj,
   2.159 -			       unique_session_keys]) 1);
   2.160 +                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   2.161 +		        addDs  [Says_imp_spies RS parts.Inj,
   2.162 +				unique_session_keys]) 1);
   2.163  val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   2.164  
   2.165  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   2.166 @@ -658,5 +658,5 @@
   2.167  by (rtac Spy_not_see_encrypted_key 2);
   2.168  by (REPEAT_FIRST assume_tac);
   2.169  by (blast_tac (claset() addSEs [MPair_parts]
   2.170 -	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
   2.171 +	       	        addDs [Says_imp_spies RS parts.Inj]) 1);
   2.172  qed_spec_mp "YM4_imp_A_Said_YM3";
     3.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Nov 18 16:36:33 1997 +0100
     3.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Nov 18 16:37:25 1997 +0100
     3.3 @@ -55,7 +55,7 @@
     3.4  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
     3.5  \                K : parts (spies evs)";
     3.6  by (blast_tac (claset() addSEs partsEs
     3.7 -                       addSDs [Says_imp_spies RS parts.Inj]) 1);
     3.8 +                        addSDs [Says_imp_spies RS parts.Inj]) 1);
     3.9  qed "YM4_Key_parts_spies";
    3.10  
    3.11  (*For proving the easier theorems about X ~: parts (spies evs).*)
    3.12 @@ -378,7 +378,7 @@
    3.13  (*Fake*)
    3.14  by (Fake_parts_insert_tac 1);
    3.15  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
    3.16 -by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
    3.17 +by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
    3.18  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
    3.19  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
    3.20  (*yes: apply unicity of session keys*)