src/HOL/Auth/Yahalom.ML
changeset 4238 679a233fb206
parent 4091 771b1f6422a8
child 4422 21238c9d363e
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Nov 18 16:36:33 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Nov 18 16:37:25 1997 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
     1.5  \                K : parts (spies evs)";
     1.6  by (blast_tac (claset() addSEs partsEs
     1.7 -                      addSDs [Says_imp_spies RS parts.Inj]) 1);
     1.8 +                        addSDs [Says_imp_spies RS parts.Inj]) 1);
     1.9  qed "YM4_Key_parts_spies";
    1.10  
    1.11  (*For proving the easier theorems about X ~: parts (spies evs).*)
    1.12 @@ -108,9 +108,9 @@
    1.13  (*Fake*)
    1.14  by (best_tac
    1.15        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.16 -               addIs  [impOfSubs analz_subset_parts]
    1.17 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.18 -               addss  (simpset())) 1);
    1.19 +                addIs  [impOfSubs analz_subset_parts]
    1.20 +                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.21 +                addss  (simpset())) 1);
    1.22  (*YM2-4: Because Key K is not fresh, etc.*)
    1.23  by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
    1.24  qed_spec_mp "new_keys_not_used";
    1.25 @@ -196,7 +196,7 @@
    1.26  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.27  (*...we assume X is a recent message and handle this case by contradiction*)
    1.28  by (blast_tac (claset() addSEs spies_partsEs
    1.29 -                       delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    1.30 +                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
    1.31  val lemma = result();
    1.32  
    1.33  goal thy 
    1.34 @@ -225,13 +225,13 @@
    1.35  by (ALLGOALS
    1.36      (asm_simp_tac 
    1.37       (simpset() addsimps (expand_ifs@pushes)
    1.38 -	       addsimps [analz_insert_eq, analz_insert_freshK])));
    1.39 +	        addsimps [analz_insert_eq, analz_insert_freshK])));
    1.40  (*Oops*)
    1.41  by (blast_tac (claset() addDs [unique_session_keys]) 3);
    1.42  (*YM3*)
    1.43  by (blast_tac (claset() delrules [impCE]
    1.44 -                       addSEs spies_partsEs
    1.45 -                       addIs [impOfSubs analz_subset_parts]) 2);
    1.46 +                        addSEs spies_partsEs
    1.47 +                        addIs [impOfSubs analz_subset_parts]) 2);
    1.48  (*Fake*) 
    1.49  by (spy_analz_tac 1);
    1.50  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.51 @@ -308,7 +308,7 @@
    1.52  by (not_bad_tac "A" 1);
    1.53  (*A's certificate guarantees the existence of the Server message*)
    1.54  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
    1.55 -			      A_trusts_YM3]) 1);
    1.56 +			       A_trusts_YM3]) 1);
    1.57  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
    1.58  
    1.59  
    1.60 @@ -451,8 +451,8 @@
    1.61  \        ==> NA' = NA & A' = A & B' = B";
    1.62  by (not_bad_tac "B'" 1);
    1.63  by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
    1.64 -                       addSEs [MPair_parts]
    1.65 -                       addDs  [unique_NB]) 1);
    1.66 +                        addSEs [MPair_parts]
    1.67 +                        addDs  [unique_NB]) 1);
    1.68  qed "Says_unique_NB";
    1.69  
    1.70  
    1.71 @@ -466,8 +466,8 @@
    1.72  by (parts_induct_tac 1);
    1.73  by (Fake_parts_insert_tac 1);
    1.74  by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
    1.75 -                       addSIs [parts_insertI]
    1.76 -                       addSEs partsEs) 1);
    1.77 +                        addSIs [parts_insertI]
    1.78 +                        addSEs partsEs) 1);
    1.79  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
    1.80  
    1.81  (*The Server sends YM3 only in response to YM2.*)
    1.82 @@ -498,19 +498,19 @@
    1.83  by (ALLGOALS
    1.84      (asm_simp_tac 
    1.85       (simpset() addsimps (expand_ifs@pushes)
    1.86 -	       addsimps [analz_insert_eq, analz_insert_freshK])));
    1.87 +	        addsimps [analz_insert_eq, analz_insert_freshK])));
    1.88  (*Prove YM3 by showing that no NB can also be an NA*)
    1.89  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
    1.90 -	               addSEs [MPair_parts]
    1.91 -		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
    1.92 +	                addSEs [MPair_parts]
    1.93 +		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
    1.94      THEN flexflex_tac);
    1.95  (*YM2: similar freshness reasoning*) 
    1.96  by (blast_tac (claset() addSEs partsEs
    1.97 -		       addDs  [Says_imp_spies RS analz.Inj,
    1.98 -			       impOfSubs analz_subset_parts]) 3);
    1.99 +		        addDs  [Says_imp_spies RS analz.Inj,
   1.100 +				impOfSubs analz_subset_parts]) 3);
   1.101  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.102  by (blast_tac (claset() addSIs [parts_insertI]
   1.103 -                       addSEs spies_partsEs) 2);
   1.104 +                        addSEs spies_partsEs) 2);
   1.105  (*Fake*)
   1.106  by (spy_analz_tac 1);
   1.107  (** LEVEL 7: YM4 and Oops remain **)
   1.108 @@ -523,7 +523,7 @@
   1.109  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   1.110  (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
   1.111  by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   1.112 -			      impOfSubs Fake_analz_insert]) 1);
   1.113 +			       impOfSubs Fake_analz_insert]) 1);
   1.114  (** LEVEL 14 **)
   1.115  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   1.116    covered by the quantified Oops assumption.*)
   1.117 @@ -535,8 +535,8 @@
   1.118  (*case NB ~= NBa*)
   1.119  by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
   1.120  by (blast_tac (claset() addSEs [MPair_parts]
   1.121 -		       addDs  [Says_imp_spies RS parts.Inj, 
   1.122 -			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.123 +		        addDs  [Says_imp_spies RS parts.Inj, 
   1.124 +			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.125  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.126  
   1.127  
   1.128 @@ -597,7 +597,7 @@
   1.129  by (Blast_tac 2);
   1.130  (*YM3*)
   1.131  by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   1.132 -		      addSEs [MPair_parts]) 1);
   1.133 +		       addSEs [MPair_parts]) 1);
   1.134  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.135  
   1.136  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.137 @@ -608,7 +608,7 @@
   1.138  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.139  \         : set evs";
   1.140  by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   1.141 -		       addEs spies_partsEs) 1);
   1.142 +		        addEs spies_partsEs) 1);
   1.143  qed "YM3_auth_B_to_A";
   1.144  
   1.145  
   1.146 @@ -628,15 +628,15 @@
   1.147  (*Fake*)
   1.148  by (Fake_parts_insert_tac 1);
   1.149  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   1.150 -by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
   1.151 +by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
   1.152  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   1.153  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   1.154  (*yes: apply unicity of session keys*)
   1.155  by (not_bad_tac "Aa" 1);
   1.156  by (blast_tac (claset() addSEs [MPair_parts]
   1.157 -                       addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.158 -		       addDs  [Says_imp_spies RS parts.Inj,
   1.159 -			       unique_session_keys]) 1);
   1.160 +                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.161 +		        addDs  [Says_imp_spies RS parts.Inj,
   1.162 +				unique_session_keys]) 1);
   1.163  val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   1.164  
   1.165  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   1.166 @@ -658,5 +658,5 @@
   1.167  by (rtac Spy_not_see_encrypted_key 2);
   1.168  by (REPEAT_FIRST assume_tac);
   1.169  by (blast_tac (claset() addSEs [MPair_parts]
   1.170 -	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
   1.171 +	       	        addDs [Says_imp_spies RS parts.Inj]) 1);
   1.172  qed_spec_mp "YM4_imp_A_Said_YM3";