src/HOL/Auth/OtwayRees.ML
changeset 3683 aafe719dff14
parent 3674 65ec38fbb265
child 3730 6933d20f335f
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -44,46 +44,46 @@
     1.4  (** For reasoning about the encrypted portion of messages **)
     1.5  
     1.6  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, 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 "OR2_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 "OR2_analz_spies";
    1.13  
    1.14  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    1.15 -\                ==> X : analz (sees Spy evs)";
    1.16 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.17 -qed "OR4_analz_sees_Spy";
    1.18 +\                ==> X : analz (spies evs)";
    1.19 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.20 +qed "OR4_analz_spies";
    1.21  
    1.22  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    1.23 -\                 ==> K : parts (sees Spy evs)";
    1.24 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.25 -qed "Oops_parts_sees_Spy";
    1.26 +\                 ==> K : parts (spies evs)";
    1.27 +by (blast_tac (!claset addSEs spies_partsEs) 1);
    1.28 +qed "Oops_parts_spies";
    1.29  
    1.30  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.31    argument as for the Fake case.  This is possible for most, but not all,
    1.32    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.33    messages originate from the Spy. *)
    1.34  
    1.35 -bind_thm ("OR2_parts_sees_Spy",
    1.36 -          OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.37 -bind_thm ("OR4_parts_sees_Spy",
    1.38 -          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.39 +bind_thm ("OR2_parts_spies",
    1.40 +          OR2_analz_spies RS (impOfSubs analz_subset_parts));
    1.41 +bind_thm ("OR4_parts_spies",
    1.42 +          OR4_analz_spies RS (impOfSubs analz_subset_parts));
    1.43  
    1.44 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    1.45 +(*For proving the easier theorems about X ~: parts (spies evs).*)
    1.46  fun parts_induct_tac i = 
    1.47      etac otway.induct i			THEN 
    1.48 -    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
    1.49 -    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
    1.50 -    forward_tac [OR2_parts_sees_Spy]  (i+3) THEN 
    1.51 +    forward_tac [Oops_parts_spies] (i+6) THEN
    1.52 +    forward_tac [OR4_parts_spies]  (i+5) THEN
    1.53 +    forward_tac [OR2_parts_spies]  (i+3) THEN 
    1.54      prove_simple_subgoals_tac  i;
    1.55  
    1.56  
    1.57 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    1.58 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.59      sends messages containing X! **)
    1.60  
    1.61  
    1.62 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.63 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.64  goal thy 
    1.65 - "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    1.66 + "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.67  by (parts_induct_tac 1);
    1.68  by (Fake_parts_insert_tac 1);
    1.69  by (Blast_tac 1);
    1.70 @@ -91,13 +91,12 @@
    1.71  Addsimps [Spy_see_shrK];
    1.72  
    1.73  goal thy 
    1.74 - "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    1.75 + "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.76  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.77  qed "Spy_analz_shrK";
    1.78  Addsimps [Spy_analz_shrK];
    1.79  
    1.80 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
    1.81 -\                  evs : otway |] ==> A:lost";
    1.82 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
    1.83  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.84  qed "Spy_see_shrK_D";
    1.85  
    1.86 @@ -107,7 +106,7 @@
    1.87  
    1.88  (*Nobody can have used non-existent keys!*)
    1.89  goal thy "!!evs. evs : otway ==>          \
    1.90 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
    1.91 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    1.92  by (parts_induct_tac 1);
    1.93  (*Fake*)
    1.94  by (best_tac
    1.95 @@ -142,9 +141,9 @@
    1.96  
    1.97  
    1.98  (*For proofs involving analz.*)
    1.99 -val analz_sees_tac = 
   1.100 -    dtac OR2_analz_sees_Spy 4 THEN 
   1.101 -    dtac OR4_analz_sees_Spy 6 THEN
   1.102 +val analz_spies_tac = 
   1.103 +    dtac OR2_analz_spies 4 THEN 
   1.104 +    dtac OR4_analz_spies 6 THEN
   1.105      forward_tac [Says_Server_message_form] 7 THEN
   1.106      assume_tac 7 THEN
   1.107      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   1.108 @@ -153,8 +152,8 @@
   1.109  (****
   1.110   The following is to prove theorems of the form
   1.111  
   1.112 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   1.113 -  Key K : analz (sees Spy evs)
   1.114 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
   1.115 +  Key K : analz (spies evs)
   1.116  
   1.117   A more general formula must be proved inductively.
   1.118  ****)
   1.119 @@ -166,10 +165,10 @@
   1.120  goal thy  
   1.121   "!!evs. evs : otway ==>                                    \
   1.122  \  ALL K KK. KK <= Compl (range shrK) -->                   \
   1.123 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
   1.124 -\            (K : KK | Key K : analz (sees Spy evs))";
   1.125 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
   1.126 +\            (K : KK | Key K : analz (spies evs))";
   1.127  by (etac otway.induct 1);
   1.128 -by analz_sees_tac;
   1.129 +by analz_spies_tac;
   1.130  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.131  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   1.132  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   1.133 @@ -182,8 +181,8 @@
   1.134  
   1.135  goal thy
   1.136   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
   1.137 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
   1.138 -\        (K = KAB | Key K : analz (sees Spy evs))";
   1.139 +\        Key K : analz (insert (Key KAB) (spies evs)) =  \
   1.140 +\        (K = KAB | Key K : analz (spies evs))";
   1.141  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.142  qed "analz_insert_freshK";
   1.143  
   1.144 @@ -204,7 +203,7 @@
   1.145  by (expand_case_tac "K = ?y" 1);
   1.146  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.147  (*...we assume X is a recent message, and handle this case by contradiction*)
   1.148 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   1.149 +by (blast_tac (!claset addSEs spies_partsEs
   1.150                         delrules [conjI] (*no split-up into 4 subgoals*)) 1);
   1.151  val lemma = result();
   1.152  
   1.153 @@ -221,9 +220,8 @@
   1.154  
   1.155  (*Only OR1 can have caused such a part of a message to appear.*)
   1.156  goal thy 
   1.157 - "!!evs. [| A ~: lost;  evs : otway |]                             \
   1.158 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
   1.159 -\             : parts (sees Spy evs) -->                           \
   1.160 + "!!evs. [| A ~: bad;  evs : otway |]                             \
   1.161 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   1.162  \            Says A B {|NA, Agent A, Agent B,                      \
   1.163  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   1.164  \             : set evs";
   1.165 @@ -235,22 +233,22 @@
   1.166  (** The Nonce NA uniquely identifies A's message. **)
   1.167  
   1.168  goal thy 
   1.169 - "!!evs. [| evs : otway; A ~: lost |]               \
   1.170 + "!!evs. [| evs : otway; A ~: bad |]               \
   1.171  \ ==> EX B'. ALL B.                                 \
   1.172 -\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
   1.173 +\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   1.174  \        --> B = B'";
   1.175  by (parts_induct_tac 1);
   1.176  by (Fake_parts_insert_tac 1);
   1.177  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.178  (*OR1: creation of new Nonce.  Move assertion into global context*)
   1.179  by (expand_case_tac "NA = ?y" 1);
   1.180 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.181 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.182  val lemma = result();
   1.183  
   1.184  goal thy 
   1.185 - "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \
   1.186 -\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \
   1.187 -\          evs : otway;  A ~: lost |]                                     \
   1.188 + "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   1.189 +\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   1.190 +\          evs : otway;  A ~: bad |]                                   \
   1.191  \        ==> B = C";
   1.192  by (prove_unique_tac lemma 1);
   1.193  qed "unique_NA";
   1.194 @@ -260,14 +258,13 @@
   1.195    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   1.196    over-simplified version of this protocol: see OtwayRees_Bad.*)
   1.197  goal thy 
   1.198 - "!!evs. [| A ~: lost;  evs : otway |]                      \
   1.199 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}        \
   1.200 -\             : parts (sees Spy evs) -->                    \
   1.201 + "!!evs. [| A ~: bad;  evs : otway |]                      \
   1.202 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   1.203  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   1.204 -\             ~: parts (sees Spy evs)";
   1.205 +\             ~: parts (spies evs)";
   1.206  by (parts_induct_tac 1);
   1.207  by (Fake_parts_insert_tac 1);
   1.208 -by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   1.209 +by (REPEAT (blast_tac (!claset addSEs spies_partsEs
   1.210                                 addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   1.211  qed_spec_mp"no_nonce_OR1_OR2";
   1.212  
   1.213 @@ -275,8 +272,8 @@
   1.214  (*Crucial property: If the encrypted message appears, and A has used NA
   1.215    to start a run, then it originated with the Server!*)
   1.216  goal thy 
   1.217 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                      \
   1.218 -\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)           \
   1.219 + "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                      \
   1.220 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   1.221  \        --> Says A B {|NA, Agent A, Agent B,                          \
   1.222  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   1.223  \             : set evs -->                                            \
   1.224 @@ -288,21 +285,21 @@
   1.225  by (parts_induct_tac 1);
   1.226  by (Fake_parts_insert_tac 1);
   1.227  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.228 -by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.229 +by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
   1.230  (*OR3 and OR4*) 
   1.231  (*OR4*)
   1.232  by (REPEAT (Safe_step_tac 2));
   1.233  by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
   1.234  by (blast_tac (!claset addSIs [Crypt_imp_OR1]
   1.235 -                       addEs  sees_Spy_partsEs) 2);
   1.236 +                       addEs  spies_partsEs) 2);
   1.237  (*OR3*)  (** LEVEL 5 **)
   1.238  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.239  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.240  by (blast_tac (!claset addSEs [MPair_parts]
   1.241 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.242 +                      addSDs [Says_imp_spies RS parts.Inj]
   1.243                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.244                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   1.245 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.246 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   1.247                        addSEs [MPair_parts]
   1.248                        addIs  [unique_NA]) 1);
   1.249  qed_spec_mp "NA_Crypt_imp_Server_msg";
   1.250 @@ -313,19 +310,17 @@
   1.251    bad form of this protocol, even though we can prove
   1.252    Spy_not_see_encrypted_key*)
   1.253  goal thy 
   1.254 - "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   1.255 -\            : set evs;                                            \
   1.256 -\           Says A B {|NA, Agent A, Agent B,                       \
   1.257 -\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   1.258 -\            : set evs;                                            \
   1.259 -\           A ~: lost;  A ~= Spy;  evs : otway |]                  \
   1.260 + "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   1.261 +\           Says A  B {|NA, Agent A, Agent B,                       \
   1.262 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   1.263 +\           A ~: bad;  A ~= Spy;  evs : otway |]                  \
   1.264  \        ==> EX NB. Says Server B                                  \
   1.265  \                     {|NA,                                        \
   1.266  \                       Crypt (shrK A) {|NA, Key K|},              \
   1.267  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   1.268  \                       : set evs";
   1.269  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.270 -                       addEs  sees_Spy_partsEs) 1);
   1.271 +                       addEs  spies_partsEs) 1);
   1.272  qed "A_trusts_OR4";
   1.273  
   1.274  
   1.275 @@ -334,14 +329,14 @@
   1.276      the premises, e.g. by having A=Spy **)
   1.277  
   1.278  goal thy 
   1.279 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
   1.280 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
   1.281  \        ==> Says Server B                                            \
   1.282  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.283  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   1.284  \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   1.285 -\            Key K ~: analz (sees Spy evs)";
   1.286 +\            Key K ~: analz (spies evs)";
   1.287  by (etac otway.induct 1);
   1.288 -by analz_sees_tac;
   1.289 +by analz_spies_tac;
   1.290  by (ALLGOALS
   1.291      (asm_simp_tac (!simpset addcongs [conj_cong] 
   1.292                              addsimps [analz_insert_eq, analz_insert_freshK]
   1.293 @@ -351,7 +346,7 @@
   1.294  (*OR4*) 
   1.295  by (Blast_tac 3);
   1.296  (*OR3*)
   1.297 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   1.298 +by (blast_tac (!claset addSEs spies_partsEs
   1.299                         addIs [impOfSubs analz_subset_parts]) 2);
   1.300  (*Fake*) 
   1.301  by (spy_analz_tac 1);
   1.302 @@ -362,8 +357,8 @@
   1.303  \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.304  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   1.305  \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   1.306 -\           A ~: lost;  B ~: lost;  evs : otway |]                  \
   1.307 -\        ==> Key K ~: analz (sees Spy evs)";
   1.308 +\           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.309 +\        ==> Key K ~: analz (spies evs)";
   1.310  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.311  by (blast_tac (!claset addSEs [lemma]) 1);
   1.312  qed "Spy_not_see_encrypted_key";
   1.313 @@ -374,9 +369,9 @@
   1.314  (*Only OR2 can have caused such a part of a message to appear.  We do not
   1.315    know anything about X: it does NOT have to have the right form.*)
   1.316  goal thy 
   1.317 - "!!evs. [| B ~: lost;  evs : otway |]                         \
   1.318 + "!!evs. [| B ~: bad;  evs : otway |]                         \
   1.319  \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   1.320 -\             : parts (sees Spy evs) -->                       \
   1.321 +\             : parts (spies evs) -->                       \
   1.322  \            (EX X. Says B Server                              \
   1.323  \             {|NA, Agent A, Agent B, X,                       \
   1.324  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.325 @@ -390,24 +385,22 @@
   1.326  (** The Nonce NB uniquely identifies B's  message. **)
   1.327  
   1.328  goal thy 
   1.329 - "!!evs. [| evs : otway; B ~: lost |]                    \
   1.330 + "!!evs. [| evs : otway; B ~: bad |]                    \
   1.331  \ ==> EX NA' A'. ALL NA A.                               \
   1.332 -\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
   1.333 +\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
   1.334  \      --> NA = NA' & A = A'";
   1.335  by (parts_induct_tac 1);
   1.336  by (Fake_parts_insert_tac 1);
   1.337  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.338  (*OR2: creation of new Nonce.  Move assertion into global context*)
   1.339  by (expand_case_tac "NB = ?y" 1);
   1.340 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.341 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.342  val lemma = result();
   1.343  
   1.344  goal thy 
   1.345 - "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   1.346 -\                  : parts(sees Spy evs);         \
   1.347 -\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   1.348 -\                  : parts(sees Spy evs);         \
   1.349 -\          evs : otway;  B ~: lost |]             \
   1.350 + "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   1.351 +\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   1.352 +\          evs : otway;  B ~: bad |]             \
   1.353  \        ==> NC = NA & C = A";
   1.354  by (prove_unique_tac lemma 1);
   1.355  qed "unique_NB";
   1.356 @@ -416,8 +409,8 @@
   1.357  (*If the encrypted message appears, and B has used Nonce NB,
   1.358    then it originated with the Server!*)
   1.359  goal thy 
   1.360 - "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway |]                        \
   1.361 -\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs)             \
   1.362 + "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway |]                        \
   1.363 +\    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)             \
   1.364  \        --> (ALL X'. Says B Server                                      \
   1.365  \                       {|NA, Agent A, Agent B, X',                      \
   1.366  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.367 @@ -429,17 +422,17 @@
   1.368  by (parts_induct_tac 1);
   1.369  by (Fake_parts_insert_tac 1);
   1.370  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.371 -by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.372 +by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
   1.373  (*OR4*)
   1.374  by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   1.375  (*OR3*)
   1.376  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.377  by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   1.378 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.379 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   1.380                         addSEs [MPair_parts]
   1.381                         addDs  [unique_NB]) 2);
   1.382  by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.383 -                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.384 +                       addSDs [Says_imp_spies RS parts.Inj]
   1.385                         delrules [conjI, impCE] (*stop split-up*)) 1);
   1.386  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.387  
   1.388 @@ -447,9 +440,8 @@
   1.389  (*Guarantee for B: if it gets a message with matching NB then the Server
   1.390    has sent the correct message.*)
   1.391  goal thy 
   1.392 - "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway;                    \
   1.393 -\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   1.394 -\            : set evs;                                            \
   1.395 + "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway;                    \
   1.396 +\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
   1.397  \           Says B Server {|NA, Agent A, Agent B, X',              \
   1.398  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   1.399  \            : set evs |]                                          \
   1.400 @@ -459,7 +451,7 @@
   1.401  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   1.402  \                   : set evs";
   1.403  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.404 -                       addSEs sees_Spy_partsEs) 1);
   1.405 +                       addSEs spies_partsEs) 1);
   1.406  qed "B_trusts_OR3";
   1.407  
   1.408  
   1.409 @@ -467,7 +459,7 @@
   1.410  
   1.411  
   1.412  goal thy 
   1.413 - "!!evs. [| B ~: lost;  evs : otway |]                           \
   1.414 + "!!evs. [| B ~: bad;  evs : otway |]                           \
   1.415  \        ==> Says Server B                                       \
   1.416  \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   1.417  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
   1.418 @@ -476,7 +468,7 @@
   1.419  \            : set evs)";
   1.420  by (etac otway.induct 1);
   1.421  by (ALLGOALS Asm_simp_tac);
   1.422 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   1.423 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
   1.424  		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   1.425  by (ALLGOALS Blast_tac);
   1.426  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.427 @@ -489,7 +481,7 @@
   1.428   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   1.429  \           Says A B {|NA, Agent A, Agent B,                                \
   1.430  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   1.431 -\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway |]               \
   1.432 +\           A ~: bad;  A ~= Spy;  B ~: bad;  evs : otway |]               \
   1.433  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   1.434  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   1.435  \            : set evs";