src/HOL/Auth/Yahalom.ML
changeset 3683 aafe719dff14
parent 3679 8df171ccdbd8
child 3708 56facaebf3e3
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -44,42 +44,42 @@
     1.4  
     1.5  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
     1.6  goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
     1.7 -\                X : analz (sees Spy evs)";
     1.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.9 -qed "YM4_analz_sees_Spy";
    1.10 +\                X : analz (spies evs)";
    1.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.12 +qed "YM4_analz_spies";
    1.13  
    1.14 -bind_thm ("YM4_parts_sees_Spy",
    1.15 -          YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.16 +bind_thm ("YM4_parts_spies",
    1.17 +          YM4_analz_spies RS (impOfSubs analz_subset_parts));
    1.18  
    1.19  (*Relates to both YM4 and Oops*)
    1.20  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    1.21 -\                K : parts (sees Spy evs)";
    1.22 +\                K : parts (spies evs)";
    1.23  by (blast_tac (!claset addSEs partsEs
    1.24 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.25 -qed "YM4_Key_parts_sees_Spy";
    1.26 +                      addSDs [Says_imp_spies RS parts.Inj]) 1);
    1.27 +qed "YM4_Key_parts_spies";
    1.28  
    1.29 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    1.30 -fun parts_sees_tac i = 
    1.31 -    forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
    1.32 -    forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
    1.33 +(*For proving the easier theorems about X ~: parts (spies evs).*)
    1.34 +fun parts_spies_tac i = 
    1.35 +    forward_tac [YM4_Key_parts_spies] (i+6) THEN
    1.36 +    forward_tac [YM4_parts_spies] (i+5)     THEN
    1.37      prove_simple_subgoals_tac  i;
    1.38  
    1.39  (*Induction for regularity theorems.  If induction formula has the form
    1.40 -   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
    1.41 -   needless information about analz (insert X (sees Spy evs))  *)
    1.42 +   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    1.43 +   needless information about analz (insert X (spies evs))  *)
    1.44  fun parts_induct_tac i = 
    1.45      etac yahalom.induct i
    1.46      THEN 
    1.47      REPEAT (FIRSTGOAL analz_mono_contra_tac)
    1.48 -    THEN  parts_sees_tac i;
    1.49 +    THEN  parts_spies_tac i;
    1.50  
    1.51  
    1.52 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    1.53 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.54      sends messages containing X! **)
    1.55  
    1.56 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.57 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.58  goal thy 
    1.59 - "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    1.60 + "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.61  by (parts_induct_tac 1);
    1.62  by (Fake_parts_insert_tac 1);
    1.63  by (Blast_tac 1);
    1.64 @@ -87,13 +87,13 @@
    1.65  Addsimps [Spy_see_shrK];
    1.66  
    1.67  goal thy 
    1.68 - "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    1.69 + "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.70  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.71  qed "Spy_analz_shrK";
    1.72  Addsimps [Spy_analz_shrK];
    1.73  
    1.74 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
    1.75 -\                  evs : yahalom |] ==> A:lost";
    1.76 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    1.77 +\                  evs : yahalom |] ==> A:bad";
    1.78  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.79  qed "Spy_see_shrK_D";
    1.80  
    1.81 @@ -103,10 +103,10 @@
    1.82  
    1.83  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
    1.84  goal thy "!!evs. evs : yahalom ==>          \
    1.85 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
    1.86 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    1.87  by (parts_induct_tac 1);
    1.88  (*YM4: Key K is not fresh!*)
    1.89 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
    1.90 +by (blast_tac (!claset addSEs spies_partsEs) 3);
    1.91  (*YM3*)
    1.92  by (Blast_tac 2);
    1.93  (*Fake*)
    1.94 @@ -139,8 +139,8 @@
    1.95  
    1.96  
    1.97  (*For proofs involving analz.*)
    1.98 -val analz_sees_tac = 
    1.99 -    forward_tac [YM4_analz_sees_Spy] 6 THEN
   1.100 +val analz_spies_tac = 
   1.101 +    forward_tac [YM4_analz_spies] 6 THEN
   1.102      forward_tac [Says_Server_message_form] 7 THEN
   1.103      assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   1.104  
   1.105 @@ -148,8 +148,8 @@
   1.106  (****
   1.107   The following is to prove theorems of the form
   1.108  
   1.109 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   1.110 -  Key K : analz (sees Spy evs)
   1.111 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
   1.112 +  Key K : analz (spies evs)
   1.113  
   1.114   A more general formula must be proved inductively.
   1.115  ****)
   1.116 @@ -159,10 +159,10 @@
   1.117  goal thy  
   1.118   "!!evs. evs : yahalom ==>                                 \
   1.119  \  ALL K KK. KK <= Compl (range shrK) -->                       \
   1.120 -\            (Key K : analz (Key``KK Un (sees Spy evs))) = \
   1.121 -\            (K : KK | Key K : analz (sees Spy evs))";
   1.122 +\            (Key K : analz (Key``KK Un (spies evs))) = \
   1.123 +\            (K : KK | Key K : analz (spies evs))";
   1.124  by (etac yahalom.induct 1);
   1.125 -by analz_sees_tac;
   1.126 +by analz_spies_tac;
   1.127  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.128  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   1.129  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.130 @@ -174,8 +174,8 @@
   1.131  
   1.132  goal thy
   1.133   "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>             \
   1.134 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =       \
   1.135 -\        (K = KAB | Key K : analz (sees Spy evs))";
   1.136 +\        Key K : analz (insert (Key KAB) (spies evs)) =       \
   1.137 +\        (K = KAB | Key K : analz (spies evs))";
   1.138  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.139  qed "analz_insert_freshK";
   1.140  
   1.141 @@ -197,17 +197,15 @@
   1.142  by (expand_case_tac "K = ?y" 1);
   1.143  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.144  (*...we assume X is a recent message and handle this case by contradiction*)
   1.145 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   1.146 +by (blast_tac (!claset addSEs spies_partsEs
   1.147                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   1.148  val lemma = result();
   1.149  
   1.150  goal thy 
   1.151 -"!!evs. [| Says Server A                                            \
   1.152 -\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   1.153 -\           : set evs;                                              \
   1.154 -\          Says Server A'                                           \
   1.155 -\           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   1.156 -\           : set evs;                                              \
   1.157 +"!!evs. [| Says Server A                                                 \
   1.158 +\            {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
   1.159 +\          Says Server A'                                                \
   1.160 +\            {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
   1.161  \          evs : yahalom |]                                    \
   1.162  \       ==> A=A' & B=B' & na=na' & nb=nb'";
   1.163  by (prove_unique_tac lemma 1);
   1.164 @@ -217,15 +215,15 @@
   1.165  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   1.166  
   1.167  goal thy 
   1.168 - "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]         \
   1.169 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]         \
   1.170  \        ==> Says Server A                                        \
   1.171  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   1.172  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.173  \             : set evs -->                                       \
   1.174  \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
   1.175 -\            Key K ~: analz (sees Spy evs)";
   1.176 +\            Key K ~: analz (spies evs)";
   1.177  by (etac yahalom.induct 1);
   1.178 -by analz_sees_tac;
   1.179 +by analz_spies_tac;
   1.180  by (ALLGOALS
   1.181      (asm_simp_tac 
   1.182       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
   1.183 @@ -234,7 +232,7 @@
   1.184  by (blast_tac (!claset addDs [unique_session_keys]) 3);
   1.185  (*YM3*)
   1.186  by (blast_tac (!claset delrules [impCE]
   1.187 -                       addSEs sees_Spy_partsEs
   1.188 +                       addSEs spies_partsEs
   1.189                         addIs [impOfSubs analz_subset_parts]) 2);
   1.190  (*Fake*) 
   1.191  by (spy_analz_tac 1);
   1.192 @@ -248,8 +246,8 @@
   1.193  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.194  \             : set evs;                                          \
   1.195  \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   1.196 -\           A ~: lost;  B ~: lost;  evs : yahalom |]         \
   1.197 -\        ==> Key K ~: analz (sees Spy evs)";
   1.198 +\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
   1.199 +\        ==> Key K ~: analz (spies evs)";
   1.200  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.201  by (blast_tac (!claset addSEs [lemma]) 1);
   1.202  qed "Spy_not_see_encrypted_key";
   1.203 @@ -259,9 +257,8 @@
   1.204  
   1.205  (*If the encrypted message appears then it originated with the Server*)
   1.206  goal thy
   1.207 - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
   1.208 -\            : parts (sees Spy evs);                              \
   1.209 -\           A ~: lost;  evs : yahalom |]                          \
   1.210 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
   1.211 +\           A ~: bad;  evs : yahalom |]                          \
   1.212  \         ==> Says Server A                                            \
   1.213  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   1.214  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   1.215 @@ -277,8 +274,8 @@
   1.216  (*B knows, by the first part of A's message, that the Server distributed 
   1.217    the key for A and B.  But this part says nothing about nonces.*)
   1.218  goal thy 
   1.219 - "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs);   \
   1.220 -\           B ~: lost;  evs : yahalom |]                                \
   1.221 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);   \
   1.222 +\           B ~: bad;  evs : yahalom |]                                \
   1.223  \        ==> EX NA NB. Says Server A                                    \
   1.224  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.225  \                                           Nonce NA, Nonce NB|},       \
   1.226 @@ -296,8 +293,8 @@
   1.227    Secrecy of NB is crucial.*)
   1.228  goal thy 
   1.229   "!!evs. evs : yahalom                                             \
   1.230 -\        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
   1.231 -\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   1.232 +\        ==> Nonce NB ~: analz (spies evs) -->                  \
   1.233 +\            Crypt K (Nonce NB) : parts (spies evs) -->         \
   1.234  \            (EX A B NA. Says Server A                             \
   1.235  \                        {|Crypt (shrK A) {|Agent B, Key K,        \
   1.236  \                                  Nonce NA, Nonce NB|},           \
   1.237 @@ -310,9 +307,9 @@
   1.238  (*YM4*)
   1.239  by (Step_tac 1);
   1.240  (*A is uncompromised because NB is secure*)
   1.241 -by (not_lost_tac "A" 1);
   1.242 +by (not_bad_tac "A" 1);
   1.243  (*A's certificate guarantees the existence of the Server message*)
   1.244 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   1.245 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
   1.246  			      A_trusts_YM3]) 1);
   1.247  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   1.248  
   1.249 @@ -342,7 +339,7 @@
   1.250    (with respect to a given trace). *)
   1.251  goalw thy [KeyWithNonce_def]
   1.252   "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   1.253 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.254 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.255  qed "fresh_not_KeyWithNonce";
   1.256  
   1.257  (*The Server message associates K with NB' and therefore not with any 
   1.258 @@ -374,10 +371,10 @@
   1.259   "!!evs. evs : yahalom ==>                                         \
   1.260  \        (ALL KK. KK <= Compl (range shrK) -->                          \
   1.261  \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
   1.262 -\             (Nonce NB : analz (Key``KK Un (sees Spy evs))) =     \
   1.263 -\             (Nonce NB : analz (sees Spy evs)))";
   1.264 +\             (Nonce NB : analz (Key``KK Un (spies evs))) =     \
   1.265 +\             (Nonce NB : analz (spies evs)))";
   1.266  by (etac yahalom.induct 1);
   1.267 -by analz_sees_tac;
   1.268 +by analz_spies_tac;
   1.269  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   1.270  by (REPEAT_FIRST (rtac lemma));
   1.271  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   1.272 @@ -395,8 +392,8 @@
   1.273  (*Fake*) 
   1.274  by (spy_analz_tac 1);
   1.275  (*YM4*)  (** LEVEL 7 **)
   1.276 -by (not_lost_tac "A" 1);
   1.277 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.278 +by (not_bad_tac "A" 1);
   1.279 +by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.280      THEN REPEAT (assume_tac 1));
   1.281  by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   1.282  qed_spec_mp "Nonce_secrecy";
   1.283 @@ -410,8 +407,8 @@
   1.284  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   1.285  \           : set evs;                                                    \
   1.286  \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
   1.287 -\        ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) =  \
   1.288 -\            (Nonce NB : analz (sees Spy evs))";
   1.289 +\        ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =  \
   1.290 +\            (Nonce NB : analz (spies evs))";
   1.291  by (asm_simp_tac (analz_image_freshK_ss addsimps 
   1.292  		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   1.293  qed "single_Nonce_secrecy";
   1.294 @@ -422,8 +419,8 @@
   1.295  goal thy 
   1.296   "!!evs. evs : yahalom ==>                                            \
   1.297  \   EX NA' A' B'. ALL NA A B.                                              \
   1.298 -\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
   1.299 -\      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   1.300 +\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
   1.301 +\      --> B ~: bad --> NA = NA' & A = A' & B = B'";
   1.302  by (parts_induct_tac 1);
   1.303  (*Fake*)
   1.304  by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   1.305 @@ -432,31 +429,29 @@
   1.306  (*YM2: creation of new Nonce.  Move assertion into global context*)
   1.307  by (expand_case_tac "nb = ?y" 1);
   1.308  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   1.309 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.310 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.311  val lemma = result();
   1.312  
   1.313  goal thy 
   1.314 - "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
   1.315 -\                  : parts (sees Spy evs);            \
   1.316 -\          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
   1.317 -\                  : parts (sees Spy evs);            \
   1.318 -\          evs : yahalom;  B ~: lost;  B' ~: lost |]  \
   1.319 + "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \
   1.320 +\          Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
   1.321 +\          evs : yahalom;  B ~: bad;  B' ~: bad |]  \
   1.322  \        ==> NA' = NA & A' = A & B' = B";
   1.323  by (prove_unique_tac lemma 1);
   1.324  qed "unique_NB";
   1.325  
   1.326  
   1.327  (*Variant useful for proving secrecy of NB: the Says... form allows 
   1.328 -  not_lost_tac to remove the assumption B' ~: lost.*)
   1.329 +  not_bad_tac to remove the assumption B' ~: bad.*)
   1.330  goal thy 
   1.331   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   1.332 -\            : set evs;          B ~: lost;                               \
   1.333 +\            : set evs;          B ~: bad;                               \
   1.334  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
   1.335  \            : set evs;                                                   \
   1.336 -\          nb ~: analz (sees Spy evs);  evs : yahalom |]        \
   1.337 +\          nb ~: analz (spies evs);  evs : yahalom |]        \
   1.338  \        ==> NA' = NA & A' = A & B' = B";
   1.339 -by (not_lost_tac "B'" 1);
   1.340 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.341 +by (not_bad_tac "B'" 1);
   1.342 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   1.343                         addSEs [MPair_parts]
   1.344                         addDs  [unique_NB]) 1);
   1.345  qed "Says_unique_NB";
   1.346 @@ -465,15 +460,13 @@
   1.347  (** A nonce value is never used both as NA and as NB **)
   1.348  
   1.349  goal thy 
   1.350 - "!!evs. [| B ~: lost;  evs : yahalom  |]            \
   1.351 -\ ==> Nonce NB ~: analz (sees Spy evs) -->           \
   1.352 -\     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
   1.353 -\       : parts(sees Spy evs)                        \
   1.354 -\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
   1.355 -\       ~: parts(sees Spy evs)";
   1.356 + "!!evs. [| B ~: bad;  evs : yahalom  |]            \
   1.357 +\ ==> Nonce NB ~: analz (spies evs) -->           \
   1.358 +\     Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
   1.359 +\     Crypt (shrK B)  {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)";
   1.360  by (parts_induct_tac 1);
   1.361  by (Fake_parts_insert_tac 1);
   1.362 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   1.363 +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]
   1.364                         addSIs [parts_insertI]
   1.365                         addSEs partsEs) 1);
   1.366  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   1.367 @@ -495,37 +488,37 @@
   1.368  
   1.369  (*A vital theorem for B, that nonce NB remains secure from the Spy.*)
   1.370  goal thy 
   1.371 - "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]  \
   1.372 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]  \
   1.373  \ ==> Says B Server                                                    \
   1.374  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.375  \     : set evs -->                                                    \
   1.376  \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   1.377 -\     Nonce NB ~: analz (sees Spy evs)";
   1.378 +\     Nonce NB ~: analz (spies evs)";
   1.379  by (etac yahalom.induct 1);
   1.380 -by analz_sees_tac;
   1.381 +by analz_spies_tac;
   1.382  by (ALLGOALS
   1.383      (asm_simp_tac 
   1.384       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
   1.385                 setloop split_tac [expand_if])));
   1.386  (*Prove YM3 by showing that no NB can also be an NA*)
   1.387 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   1.388 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
   1.389  	               addSEs [MPair_parts]
   1.390  		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
   1.391      THEN flexflex_tac);
   1.392  (*YM2: similar freshness reasoning*) 
   1.393  by (blast_tac (!claset addSEs partsEs
   1.394 -		       addDs  [Says_imp_sees_Spy RS analz.Inj,
   1.395 +		       addDs  [Says_imp_spies RS analz.Inj,
   1.396  			       impOfSubs analz_subset_parts]) 3);
   1.397  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.398  by (blast_tac (!claset addSIs [parts_insertI]
   1.399 -                       addSEs sees_Spy_partsEs) 2);
   1.400 +                       addSEs spies_partsEs) 2);
   1.401  (*Fake*)
   1.402  by (spy_analz_tac 1);
   1.403  (** LEVEL 7: YM4 and Oops remain **)
   1.404  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   1.405  by (REPEAT (Safe_step_tac 1));
   1.406 -by (not_lost_tac "Aa" 1);
   1.407 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.408 +by (not_bad_tac "Aa" 1);
   1.409 +by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.410  by (forward_tac [Says_Server_message_form] 3);
   1.411  by (forward_tac [Says_Server_imp_YM2] 4);
   1.412  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   1.413 @@ -544,7 +537,7 @@
   1.414  (*case NB ~= NBa*)
   1.415  by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   1.416  by (blast_tac (!claset addSEs [MPair_parts]
   1.417 -		       addDs  [Says_imp_sees_Spy RS parts.Inj, 
   1.418 +		       addDs  [Says_imp_spies RS parts.Inj, 
   1.419  			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.420  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.421  
   1.422 @@ -561,14 +554,14 @@
   1.423  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.424  \                       Crypt K (Nonce NB)|} : set evs;                     \
   1.425  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   1.426 -\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   1.427 +\           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   1.428  \         ==> Says Server A                                                 \
   1.429  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   1.430  \                               Nonce NA, Nonce NB|},                       \
   1.431  \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   1.432  \               : set evs";
   1.433  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.434 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   1.435 +by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
   1.436      dtac B_trusts_YM4_shrK 1);
   1.437  by (dtac B_trusts_YM4_newK 3);
   1.438  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.439 @@ -584,9 +577,8 @@
   1.440  (*The encryption in message YM2 tells us it cannot be faked.*)
   1.441  goal thy 
   1.442   "!!evs. evs : yahalom                                            \
   1.443 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                   \
   1.444 -\        : parts (sees Spy evs) -->                               \
   1.445 -\      B ~: lost -->                                              \
   1.446 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
   1.447 +\      B ~: bad -->                                              \
   1.448  \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.449  \         : set evs";
   1.450  by (parts_induct_tac 1);
   1.451 @@ -598,7 +590,7 @@
   1.452   "!!evs. evs : yahalom                                                      \
   1.453  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.454  \         : set evs -->                                                     \
   1.455 -\      B ~: lost -->                                                        \
   1.456 +\      B ~: bad -->                                                        \
   1.457  \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.458  \                 : set evs";
   1.459  by (etac yahalom.induct 1);
   1.460 @@ -606,7 +598,7 @@
   1.461  (*YM4*)
   1.462  by (Blast_tac 2);
   1.463  (*YM3*)
   1.464 -by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
   1.465 +by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   1.466  		      addSEs [MPair_parts]) 1);
   1.467  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.468  
   1.469 @@ -614,11 +606,11 @@
   1.470  goal thy
   1.471   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.472  \             : set evs;                                                    \
   1.473 -\           A ~: lost;  B ~: lost;  evs : yahalom |]                        \
   1.474 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                        \
   1.475  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.476  \         : set evs";
   1.477  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   1.478 -		       addEs sees_Spy_partsEs) 1);
   1.479 +		       addEs spies_partsEs) 1);
   1.480  qed "YM3_auth_B_to_A";
   1.481  
   1.482  
   1.483 @@ -629,12 +621,11 @@
   1.484    NB matters for freshness.*)  
   1.485  goal thy 
   1.486   "!!evs. evs : yahalom                                             \
   1.487 -\        ==> Key K ~: analz (sees Spy evs) -->                     \
   1.488 -\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   1.489 -\            Crypt (shrK B) {|Agent A, Key K|}                     \
   1.490 -\              : parts (sees Spy evs) -->                          \
   1.491 -\            B ~: lost -->                                         \
   1.492 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.493 +\        ==> Key K ~: analz (spies evs) -->                     \
   1.494 +\            Crypt K (Nonce NB) : parts (spies evs) -->         \
   1.495 +\            Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
   1.496 +\            B ~: bad -->                                         \
   1.497 +\            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.498  by (parts_induct_tac 1);
   1.499  (*Fake*)
   1.500  by (Fake_parts_insert_tac 1);
   1.501 @@ -643,10 +634,10 @@
   1.502  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   1.503  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.504  (*yes: apply unicity of session keys*)
   1.505 -by (not_lost_tac "Aa" 1);
   1.506 +by (not_bad_tac "Aa" 1);
   1.507  by (blast_tac (!claset addSEs [MPair_parts]
   1.508                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.509 -		       addDs  [Says_imp_sees_Spy RS parts.Inj,
   1.510 +		       addDs  [Says_imp_spies RS parts.Inj,
   1.511  			       unique_session_keys]) 1);
   1.512  val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   1.513  
   1.514 @@ -660,14 +651,14 @@
   1.515  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.516  \                       Crypt K (Nonce NB)|} : set evs;                     \
   1.517  \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   1.518 -\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   1.519 +\           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   1.520  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.521  by (dtac B_trusts_YM4 1);
   1.522  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   1.523 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
   1.524 +by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   1.525  by (rtac lemma 1);
   1.526  by (rtac Spy_not_see_encrypted_key 2);
   1.527  by (REPEAT_FIRST assume_tac);
   1.528  by (blast_tac (!claset addSEs [MPair_parts]
   1.529 -	       	       addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.530 +	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
   1.531  qed_spec_mp "YM4_imp_A_Said_YM3";