src/HOL/Auth/Yahalom.ML
changeset 6335 7e4bffaa2a3e
parent 5932 737559a43e71
child 7499 23e090051cb8
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Mar 10 10:42:40 1999 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Mar 10 10:42:57 1999 +0100
     1.3 @@ -18,11 +18,28 @@
     1.4  \     ==> EX X NB K. EX evs: yahalom.          \
     1.5  \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
     1.6  by (REPEAT (resolve_tac [exI,bexI] 1));
     1.7 -by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
     1.8 -          yahalom.YM4) 2);
     1.9 +by (rtac (yahalom.Nil RS 
    1.10 +          yahalom.YM1 RS yahalom.Reception RS
    1.11 +          yahalom.YM2 RS yahalom.Reception RS 
    1.12 +          yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
    1.13  by possibility_tac;
    1.14  result();
    1.15  
    1.16 +Goal "[| Gets B X : set evs; evs : yahalom |] ==> EX A. Says A B X : set evs";
    1.17 +by (etac rev_mp 1);
    1.18 +by (etac yahalom.induct 1);
    1.19 +by Auto_tac;
    1.20 +qed "Gets_imp_Says";
    1.21 +
    1.22 +(*Must be proved separately for each protocol*)
    1.23 +Goal "[| Gets B X : set evs; evs : yahalom |]  ==> X : knows Spy evs";
    1.24 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    1.25 +qed"Gets_imp_knows_Spy";
    1.26 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    1.27 +
    1.28 +fun g_not_bad_tac s = 
    1.29 +  forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s;
    1.30 +
    1.31  
    1.32  (**** Inductive proofs about yahalom ****)
    1.33  
    1.34 @@ -30,49 +47,50 @@
    1.35  (** For reasoning about the encrypted portion of messages **)
    1.36  
    1.37  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.38 -Goal "Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
    1.39 -\             X : analz (spies evs)";
    1.40 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.41 -qed "YM4_analz_spies";
    1.42 +Goal "[| Gets A {|Crypt (shrK A) Y, X|} : set evs;  evs : yahalom |]  \
    1.43 +\     ==> X : analz (knows Spy evs)";
    1.44 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    1.45 +qed "YM4_analz_knows_Spy";
    1.46  
    1.47 -bind_thm ("YM4_parts_spies",
    1.48 -          YM4_analz_spies RS (impOfSubs analz_subset_parts));
    1.49 +bind_thm ("YM4_parts_knows_Spy",
    1.50 +          YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    1.51  
    1.52 -(*Relates to both YM4 and Oops*)
    1.53 -Goal "Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    1.54 -\             K : parts (spies evs)";
    1.55 +(*For Oops*)
    1.56 +Goal "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs \
    1.57 +\     ==> K : parts (knows Spy evs)";
    1.58  by (blast_tac (claset() addSEs partsEs
    1.59 -                        addSDs [Says_imp_spies RS parts.Inj]) 1);
    1.60 -qed "YM4_Key_parts_spies";
    1.61 +                        addSDs [Says_imp_knows_Spy RS parts.Inj]) 1);
    1.62 +qed "YM4_Key_parts_knows_Spy";
    1.63  
    1.64 -(*For proving the easier theorems about X ~: parts (spies evs).*)
    1.65 -fun parts_spies_tac i = 
    1.66 -    forward_tac [YM4_Key_parts_spies] (i+6) THEN
    1.67 -    forward_tac [YM4_parts_spies] (i+5)     THEN
    1.68 -    prove_simple_subgoals_tac  i;
    1.69 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    1.70 +fun parts_knows_Spy_tac i = 
    1.71 +  EVERY
    1.72 +   [forward_tac [YM4_Key_parts_knows_Spy] (i+7),
    1.73 +    forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
    1.74 +    prove_simple_subgoals_tac i];
    1.75  
    1.76  (*Induction for regularity theorems.  If induction formula has the form
    1.77 -   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    1.78 -   needless information about analz (insert X (spies evs))  *)
    1.79 +   X ~: analz (knows Spy evs) --> ... then it shortens the proof by discarding
    1.80 +   needless information about analz (insert X (knows Spy evs))  *)
    1.81  fun parts_induct_tac i = 
    1.82      etac yahalom.induct i
    1.83      THEN 
    1.84      REPEAT (FIRSTGOAL analz_mono_contra_tac)
    1.85 -    THEN  parts_spies_tac i;
    1.86 +    THEN  parts_knows_Spy_tac i;
    1.87  
    1.88  
    1.89 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.90 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    1.91      sends messages containing X! **)
    1.92  
    1.93  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.94 -Goal "evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.95 +Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
    1.96  by (parts_induct_tac 1);
    1.97  by (Fake_parts_insert_tac 1);
    1.98  by (ALLGOALS Blast_tac);
    1.99  qed "Spy_see_shrK";
   1.100  Addsimps [Spy_see_shrK];
   1.101  
   1.102 -Goal "evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   1.103 +Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
   1.104  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   1.105  qed "Spy_analz_shrK";
   1.106  Addsimps [Spy_analz_shrK];
   1.107 @@ -83,12 +101,12 @@
   1.108  
   1.109  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   1.110  Goal "evs : yahalom ==>          \
   1.111 -\      Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   1.112 +\      Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
   1.113  by (parts_induct_tac 1);
   1.114  (*Fake*)
   1.115  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   1.116  (*YM2-4: Because Key K is not fresh, etc.*)
   1.117 -by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
   1.118 +by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
   1.119  qed_spec_mp "new_keys_not_used";
   1.120  
   1.121  bind_thm ("new_keys_not_analzd",
   1.122 @@ -113,13 +131,14 @@
   1.123  
   1.124  
   1.125  (*For proofs involving analz.*)
   1.126 -val analz_spies_tac = forward_tac [YM4_analz_spies] 6;
   1.127 +val analz_knows_Spy_tac = 
   1.128 +    forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7;
   1.129  
   1.130  (****
   1.131   The following is to prove theorems of the form
   1.132  
   1.133 -  Key K : analz (insert (Key KAB) (spies evs)) ==>
   1.134 -  Key K : analz (spies evs)
   1.135 +  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   1.136 +  Key K : analz (knows Spy evs)
   1.137  
   1.138   A more general formula must be proved inductively.
   1.139  ****)
   1.140 @@ -128,10 +147,10 @@
   1.141  
   1.142  Goal "evs : yahalom ==>                              \
   1.143  \  ALL K KK. KK <= - (range shrK) -->                \
   1.144 -\         (Key K : analz (Key``KK Un (spies evs))) = \
   1.145 -\         (K : KK | Key K : analz (spies evs))";
   1.146 +\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
   1.147 +\         (K : KK | Key K : analz (knows Spy evs))";
   1.148  by (etac yahalom.induct 1);
   1.149 -by analz_spies_tac;
   1.150 +by analz_knows_Spy_tac;
   1.151  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.152  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   1.153  by (ALLGOALS (asm_simp_tac
   1.154 @@ -141,8 +160,8 @@
   1.155  qed_spec_mp "analz_image_freshK";
   1.156  
   1.157  Goal "[| evs : yahalom;  KAB ~: range shrK |]              \
   1.158 -\      ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
   1.159 -\          (K = KAB | Key K : analz (spies evs))";
   1.160 +\      ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   1.161 +\          (K = KAB | Key K : analz (knows Spy evs))";
   1.162  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.163  qed "analz_insert_freshK";
   1.164  
   1.165 @@ -163,7 +182,7 @@
   1.166  by (expand_case_tac "K = ?y" 1);
   1.167  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.168  (*...we assume X is a recent message and handle this case by contradiction*)
   1.169 -by (blast_tac (claset() addSEs spies_partsEs
   1.170 +by (blast_tac (claset() addSEs knows_Spy_partsEs
   1.171                          delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   1.172  val lemma = result();
   1.173  
   1.174 @@ -185,9 +204,9 @@
   1.175  \             Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.176  \          : set evs -->                                       \
   1.177  \         Notes Spy {|na, nb, Key K|} ~: set evs -->           \
   1.178 -\         Key K ~: analz (spies evs)";
   1.179 +\         Key K ~: analz (knows Spy evs)";
   1.180  by (etac yahalom.induct 1);
   1.181 -by analz_spies_tac;
   1.182 +by analz_knows_Spy_tac;
   1.183  by (ALLGOALS
   1.184      (asm_simp_tac 
   1.185       (simpset() addsimps split_ifs @ pushes @
   1.186 @@ -196,7 +215,7 @@
   1.187  by (blast_tac (claset() addDs [unique_session_keys]) 3);
   1.188  (*YM3*)
   1.189  by (blast_tac (claset() delrules [impCE]
   1.190 -                        addSEs spies_partsEs
   1.191 +                        addSEs knows_Spy_partsEs
   1.192                          addIs [impOfSubs analz_subset_parts]) 2);
   1.193  (*Fake*) 
   1.194  by (spy_analz_tac 1);
   1.195 @@ -210,7 +229,7 @@
   1.196  \          : set evs;                                          \
   1.197  \        Notes Spy {|na, nb, Key K|} ~: set evs;               \
   1.198  \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.199 -\     ==> Key K ~: analz (spies evs)";
   1.200 +\     ==> Key K ~: analz (knows Spy evs)";
   1.201  by (blast_tac (claset() addSEs [lemma]) 1);
   1.202  qed "Spy_not_see_encrypted_key";
   1.203  
   1.204 @@ -218,7 +237,7 @@
   1.205  (** Security Guarantee for A upon receiving YM3 **)
   1.206  
   1.207  (*If the encrypted message appears then it originated with the Server*)
   1.208 -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
   1.209 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   1.210  \        A ~: bad;  evs : yahalom |]                          \
   1.211  \      ==> Says Server A                                            \
   1.212  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   1.213 @@ -230,10 +249,10 @@
   1.214  qed "A_trusts_YM3";
   1.215  
   1.216  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   1.217 -Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
   1.218 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   1.219  \        Notes Spy {|na, nb, Key K|} ~: set evs;               \
   1.220  \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.221 -\     ==> Key K ~: analz (spies evs)";
   1.222 +\     ==> Key K ~: analz (knows Spy evs)";
   1.223  by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
   1.224  qed "A_gets_good_key";
   1.225  
   1.226 @@ -241,7 +260,7 @@
   1.227  
   1.228  (*B knows, by the first part of A's message, that the Server distributed 
   1.229    the key for A and B.  But this part says nothing about nonces.*)
   1.230 -Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);      \
   1.231 +Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs);      \
   1.232  \        B ~: bad;  evs : yahalom |]                                 \
   1.233  \     ==> EX NA NB. Says Server A                                    \
   1.234  \                     {|Crypt (shrK A) {|Agent B, Key K,             \
   1.235 @@ -257,11 +276,11 @@
   1.236  
   1.237  (*B knows, by the second part of A's message, that the Server distributed 
   1.238    the key quoting nonce NB.  This part says nothing about agent names. 
   1.239 -  Secrecy of NB is crucial.  Note that  Nonce NB  ~: analz (spies evs)  must
   1.240 +  Secrecy of NB is crucial.  Note that  Nonce NB ~: analz(knows Spy evs)  must
   1.241    be the FIRST antecedent of the induction formula.*)
   1.242  Goal "evs : yahalom                                          \
   1.243 -\     ==> Nonce NB ~: analz (spies evs) -->                  \
   1.244 -\         Crypt K (Nonce NB) : parts (spies evs) -->         \
   1.245 +\     ==> Nonce NB ~: analz (knows Spy evs) -->                  \
   1.246 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->         \
   1.247  \         (EX A B NA. Says Server A                          \
   1.248  \                     {|Crypt (shrK A) {|Agent B, Key K,     \
   1.249  \                               Nonce NA, Nonce NB|},        \
   1.250 @@ -274,9 +293,9 @@
   1.251  by (Fake_parts_insert_tac 1);
   1.252  (*YM4*)
   1.253  (*A is uncompromised because NB is secure*)
   1.254 -by (not_bad_tac "A" 1);
   1.255 +by (g_not_bad_tac "A" 1);
   1.256  (*A's certificate guarantees the existence of the Server message*)
   1.257 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
   1.258 +by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj RS parts.Fst RS
   1.259  			       A_trusts_YM3]) 1);
   1.260  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   1.261  
   1.262 @@ -308,11 +327,17 @@
   1.263  qed "KeyWithNonce_Notes";
   1.264  Addsimps [KeyWithNonce_Notes];
   1.265  
   1.266 +Goalw [KeyWithNonce_def]
   1.267 +   "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs";
   1.268 +by (Simp_tac 1);
   1.269 +qed "KeyWithNonce_Gets";
   1.270 +Addsimps [KeyWithNonce_Gets];
   1.271 +
   1.272  (*A fresh key cannot be associated with any nonce 
   1.273    (with respect to a given trace). *)
   1.274  Goalw [KeyWithNonce_def]
   1.275   "Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   1.276 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.277 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   1.278  qed "fresh_not_KeyWithNonce";
   1.279  
   1.280  (*The Server message associates K with NB' and therefore not with any 
   1.281 @@ -342,10 +367,10 @@
   1.282  Goal "evs : yahalom ==>                                      \
   1.283  \     (ALL KK. KK <= - (range shrK) -->                      \
   1.284  \          (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
   1.285 -\          (Nonce NB : analz (Key``KK Un (spies evs))) =     \
   1.286 -\          (Nonce NB : analz (spies evs)))";
   1.287 +\          (Nonce NB : analz (Key``KK Un (knows Spy evs))) =     \
   1.288 +\          (Nonce NB : analz (knows Spy evs)))";
   1.289  by (etac yahalom.induct 1);
   1.290 -by analz_spies_tac;
   1.291 +by analz_knows_Spy_tac;
   1.292  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   1.293  by (REPEAT_FIRST (rtac Nonce_secrecy_lemma));
   1.294  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   1.295 @@ -356,15 +381,15 @@
   1.296       (analz_image_freshK_ss 
   1.297         addsimps split_ifs
   1.298         addsimps [all_conj_distrib, analz_image_freshK,
   1.299 -		 KeyWithNonce_Says, KeyWithNonce_Notes,
   1.300 +		 KeyWithNonce_Says, KeyWithNonce_Notes, KeyWithNonce_Gets,
   1.301  		 fresh_not_KeyWithNonce, Says_Server_not_range,
   1.302  		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
   1.303  		 Says_Server_KeyWithNonce])));
   1.304  (*Fake*) 
   1.305  by (spy_analz_tac 1);
   1.306  (*YM4*)  (** LEVEL 6 **)
   1.307 -by (not_bad_tac "A" 1);
   1.308 -by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.309 +by (g_not_bad_tac "A" 1);
   1.310 +by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.311      THEN REPEAT (assume_tac 1));
   1.312  by (blast_tac (claset() addIs [KeyWithNonceI]) 1);
   1.313  qed_spec_mp "Nonce_secrecy";
   1.314 @@ -377,8 +402,8 @@
   1.315  \         {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}  \
   1.316  \        : set evs;                                                  \
   1.317  \        NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]            \
   1.318 -\     ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =        \
   1.319 -\         (Nonce NB : analz (spies evs))";
   1.320 +\     ==> (Nonce NB : analz (insert (Key KAB) (knows Spy evs))) =        \
   1.321 +\         (Nonce NB : analz (knows Spy evs))";
   1.322  by (asm_simp_tac (analz_image_freshK_ss addsimps 
   1.323  		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   1.324  qed "single_Nonce_secrecy";
   1.325 @@ -388,7 +413,7 @@
   1.326  
   1.327  Goal "evs : yahalom ==>                                         \
   1.328  \EX NA' A' B'. ALL NA A B.                                      \
   1.329 -\   Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
   1.330 +\   Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(knows Spy evs) \
   1.331  \   --> B ~: bad --> NA = NA' & A = A' & B = B'";
   1.332  by (parts_induct_tac 1);
   1.333  (*Fake*)
   1.334 @@ -398,11 +423,11 @@
   1.335  (*YM2: creation of new Nonce.  Move assertion into global context*)
   1.336  by (expand_case_tac "nb = ?y" 1);
   1.337  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   1.338 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.339 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   1.340  val lemma = result();
   1.341  
   1.342 -Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs);    \
   1.343 -\       Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
   1.344 +Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (knows Spy evs);    \
   1.345 +\        Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (knows Spy evs); \
   1.346  \       evs : yahalom;  B ~: bad;  B' ~: bad |]  \
   1.347  \     ==> NA' = NA & A' = A & B' = B";
   1.348  by (prove_unique_tac lemma 1);
   1.349 @@ -411,14 +436,14 @@
   1.350  
   1.351  (*Variant useful for proving secrecy of NB: the Says... form allows 
   1.352    not_bad_tac to remove the assumption B' ~: bad.*)
   1.353 -Goal "[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   1.354 -\         : set evs;          B ~: bad;                                \
   1.355 -\       Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
   1.356 -\         : set evs;                                                   \
   1.357 -\       nb ~: analz (spies evs);  evs : yahalom |]                     \
   1.358 +Goal "[| Says C S   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   1.359 +\          : set evs;          B ~: bad;                                \
   1.360 +\        Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}    \
   1.361 +\          : set evs;                                                   \
   1.362 +\        nb ~: analz (knows Spy evs);  evs : yahalom |]                 \
   1.363  \     ==> NA' = NA & A' = A & B' = B";
   1.364 -by (not_bad_tac "B'" 1);
   1.365 -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
   1.366 +by (g_not_bad_tac "B'" 1);
   1.367 +by (blast_tac (claset() addSDs [Says_imp_knows_Spy RS parts.Inj]
   1.368                          addSEs [MPair_parts]
   1.369                          addDs  [unique_NB]) 1);
   1.370  qed "Says_unique_NB";
   1.371 @@ -427,12 +452,12 @@
   1.372  (** A nonce value is never used both as NA and as NB **)
   1.373  
   1.374  Goal "evs : yahalom                     \
   1.375 -\ ==> Nonce NB ~: analz (spies evs) -->    \
   1.376 -\  Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
   1.377 -\  Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(spies evs)";
   1.378 +\ ==> Nonce NB ~: analz (knows Spy evs) -->    \
   1.379 +\  Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(knows Spy evs) --> \
   1.380 +\  Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(knows Spy evs)";
   1.381  by (parts_induct_tac 1);
   1.382  by (Fake_parts_insert_tac 1);
   1.383 -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
   1.384 +by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj]
   1.385                          addSIs [parts_insertI]
   1.386                          addSEs partsEs) 1);
   1.387  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   1.388 @@ -444,9 +469,8 @@
   1.389  Goal "[| Says Server A                                                \
   1.390  \         {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   1.391  \        evs : yahalom |]                                             \
   1.392 -\     ==> EX B'. Says B' Server                                       \
   1.393 -\                   {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.394 -\                : set evs";
   1.395 +\     ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.396 +\            : set evs";
   1.397  by (etac rev_mp 1);
   1.398  by (etac yahalom.induct 1);
   1.399  by Auto_tac;
   1.400 @@ -459,40 +483,44 @@
   1.401  \       {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.402  \  : set evs -->                                                    \
   1.403  \  (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->      \
   1.404 -\  Nonce NB ~: analz (spies evs)";
   1.405 +\  Nonce NB ~: analz (knows Spy evs)";
   1.406  by (etac yahalom.induct 1);
   1.407 -by analz_spies_tac;
   1.408 +by analz_knows_Spy_tac;
   1.409  by (ALLGOALS
   1.410      (asm_simp_tac 
   1.411       (simpset() addsimps split_ifs @ pushes @
   1.412  	                 [analz_insert_eq, analz_insert_freshK])));
   1.413  (*Prove YM3 by showing that no NB can also be an NA*)
   1.414 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
   1.415 +by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj]
   1.416  	                addSEs [MPair_parts]
   1.417 -		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4);
   1.418 +		        addDs  [no_nonce_YM1_YM2, Gets_imp_Says,
   1.419 +				Says_unique_NB]) 4);
   1.420  (*YM2: similar freshness reasoning*) 
   1.421  by (blast_tac (claset() addSEs partsEs
   1.422 -		        addDs  [Says_imp_spies RS analz.Inj,
   1.423 +		        addDs  [Gets_imp_Says,
   1.424 +				Says_imp_knows_Spy RS analz.Inj,
   1.425  				impOfSubs analz_subset_parts]) 3);
   1.426  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.427  by (blast_tac (claset() addSIs [parts_insertI]
   1.428 -                        addSEs spies_partsEs) 2);
   1.429 +                        addSEs knows_Spy_partsEs) 2);
   1.430  (*Fake*)
   1.431  by (spy_analz_tac 1);
   1.432  (** LEVEL 7: YM4 and Oops remain **)
   1.433  by (ALLGOALS (Clarify_tac THEN' 
   1.434  	      full_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.435  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   1.436 -by (not_bad_tac "Aa" 1);
   1.437 -by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.438 +by (g_not_bad_tac "Aa" 1);
   1.439 +by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.440 +    THEN assume_tac 1);
   1.441  by (forward_tac [Says_Server_imp_YM2] 3);
   1.442  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.443  (*  use Says_unique_NB to identify message components: Aa=A, Ba=B*)
   1.444 -by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key]) 1);
   1.445 +by (blast_tac (claset() addDs [Says_unique_NB, 
   1.446 +			       Spy_not_see_encrypted_key]) 1);
   1.447  (** LEVEL 13 **)
   1.448  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   1.449    covered by the quantified Oops assumption.*)
   1.450 -by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.451 +by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.452  by (expand_case_tac "NB = NBa" 1);
   1.453  (*If NB=NBa then all other components of the Oops message agree*)
   1.454  by (blast_tac (claset() addDs [Says_unique_NB]) 1);
   1.455 @@ -500,7 +528,7 @@
   1.456  by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
   1.457  by (Clarify_tac 1);
   1.458  by (blast_tac (claset() addSEs [MPair_parts]
   1.459 -		        addDs  [Says_imp_spies RS parts.Inj, 
   1.460 +		        addDs  [Says_imp_knows_Spy RS parts.Inj, 
   1.461  			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.462  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.463  
   1.464 @@ -510,7 +538,7 @@
   1.465    assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   1.466    If this run is broken and the spy substitutes a certificate containing an
   1.467    old key, B has no means of telling.*)
   1.468 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.469 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.470  \                    Crypt K (Nonce NB)|} : set evs;                     \
   1.471  \        Says B Server                                                   \
   1.472  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.473 @@ -523,8 +551,8 @@
   1.474  \                    Crypt (shrK B) {|Agent A, Key K|}|}                 \
   1.475  \            : set evs";
   1.476  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.477 -by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
   1.478 -    dtac B_trusts_YM4_shrK 1);
   1.479 +by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN
   1.480 +    assume_tac 1 THEN dtac B_trusts_YM4_shrK 1);
   1.481  by (dtac B_trusts_YM4_newK 3);
   1.482  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.483  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.484 @@ -534,14 +562,14 @@
   1.485  
   1.486  
   1.487  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   1.488 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.489 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.490  \                    Crypt K (Nonce NB)|} : set evs;                     \
   1.491  \        Says B Server                                                   \
   1.492  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.493  \          : set evs;                                                    \
   1.494  \        ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
   1.495  \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.496 -\     ==> Key K ~: analz (spies evs)";
   1.497 +\     ==> Key K ~: analz (knows Spy evs)";
   1.498  by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
   1.499  qed "B_gets_good_key";
   1.500  
   1.501 @@ -550,7 +578,7 @@
   1.502  
   1.503  (*The encryption in message YM2 tells us it cannot be faked.*)
   1.504  Goal "evs : yahalom                                            \
   1.505 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
   1.506 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (knows Spy evs) --> \
   1.507  \   B ~: bad -->                                              \
   1.508  \   Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.509  \      : set evs";
   1.510 @@ -570,18 +598,18 @@
   1.511  (*YM4*)
   1.512  by (Blast_tac 2);
   1.513  (*YM3 [blast_tac is 50% slower] *)
   1.514 -by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   1.515 +by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_knows_Spy RS parts.Inj]
   1.516  		       addSEs [MPair_parts]) 1);
   1.517  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.518  
   1.519  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.520 -Goal "[| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.521 +Goal "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.522  \          : set evs;                                                    \
   1.523  \        A ~: bad;  B ~: bad;  evs : yahalom |]                        \
   1.524  \==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.525  \      : set evs";
   1.526  by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   1.527 -		        addEs spies_partsEs) 1);
   1.528 +		        addEs knows_Spy_partsEs) 1);
   1.529  qed "YM3_auth_B_to_A";
   1.530  
   1.531  
   1.532 @@ -591,9 +619,9 @@
   1.533    A has said NB.  We can't be sure about the rest of A's message, but only
   1.534    NB matters for freshness.*)  
   1.535  Goal "evs : yahalom                                             \
   1.536 -\     ==> Key K ~: analz (spies evs) -->                     \
   1.537 -\         Crypt K (Nonce NB) : parts (spies evs) -->         \
   1.538 -\         Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
   1.539 +\     ==> Key K ~: analz (knows Spy evs) -->                     \
   1.540 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->         \
   1.541 +\         Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs) --> \
   1.542  \         B ~: bad -->                                         \
   1.543  \         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.544  by (parts_induct_tac 1);
   1.545 @@ -604,18 +632,18 @@
   1.546  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   1.547  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   1.548  (*yes: apply unicity of session keys*)
   1.549 -by (not_bad_tac "Aa" 1);
   1.550 +by (g_not_bad_tac "Aa" 1);
   1.551  by (blast_tac (claset() addSEs [MPair_parts]
   1.552                          addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.553 -		        addDs  [Says_imp_spies RS parts.Inj,
   1.554 +		        addDs  [Says_imp_knows_Spy RS parts.Inj,
   1.555  				unique_session_keys]) 1);
   1.556 -val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   1.557 +qed_spec_mp "A_Said_YM3_lemma";
   1.558  
   1.559  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   1.560    Moreover, A associates K with NB (thus is talking about the same run).
   1.561    Other premises guarantee secrecy of K.*)
   1.562 -Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.563 -\                    Crypt K (Nonce NB)|} : set evs;                     \
   1.564 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.565 +\                 Crypt K (Nonce NB)|} : set evs;                     \
   1.566  \        Says B Server                                                   \
   1.567  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.568  \          : set evs;                                                    \
   1.569 @@ -624,10 +652,10 @@
   1.570  \     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.571  by (forward_tac [B_trusts_YM4] 1);
   1.572  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   1.573 -by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   1.574 -by (rtac lemma 1);
   1.575 +by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);
   1.576 +by (rtac A_Said_YM3_lemma 1);
   1.577  by (rtac Spy_not_see_encrypted_key 2);
   1.578  by (REPEAT_FIRST assume_tac);
   1.579  by (blast_tac (claset() addSEs [MPair_parts]
   1.580 -	       	        addDs [Says_imp_spies RS parts.Inj]) 1);
   1.581 +	       	        addDs [Says_imp_knows_Spy RS parts.Inj]) 1);
   1.582  qed_spec_mp "YM4_imp_A_Said_YM3";