src/HOL/Auth/OtwayRees.ML
changeset 3519 ab0a9fbed4c0
parent 3516 470626799511
child 3543 82f33248d89d
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -17,14 +17,11 @@
     1.4  proof_timing:=true;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 -(*Replacing the variable by a constant improves search speed by 50%!*)
     1.8 -val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
     1.9 -
    1.10  
    1.11  (*A "possibility property": there are traces that reach the end*)
    1.12  goal thy 
    1.13   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.14 -\        ==> EX K. EX NA. EX evs: otway lost.          \
    1.15 +\        ==> EX K. EX NA. EX evs: otway.          \
    1.16  \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    1.17  \                 : set evs";
    1.18  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.19 @@ -36,7 +33,7 @@
    1.20  (**** Inductive proofs about otway ****)
    1.21  
    1.22  (*Nobody sends themselves messages*)
    1.23 -goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    1.24 +goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    1.25  by (etac otway.induct 1);
    1.26  by (Auto_tac());
    1.27  qed_spec_mp "not_Says_to_self";
    1.28 @@ -47,17 +44,17 @@
    1.29  (** For reasoning about the encrypted portion of messages **)
    1.30  
    1.31  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    1.32 -\                ==> X : analz (sees lost Spy evs)";
    1.33 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    1.34 +\                ==> X : analz (sees Spy evs)";
    1.35 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.36  qed "OR2_analz_sees_Spy";
    1.37  
    1.38  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    1.39 -\                ==> X : analz (sees lost Spy evs)";
    1.40 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    1.41 +\                ==> X : analz (sees Spy evs)";
    1.42 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.43  qed "OR4_analz_sees_Spy";
    1.44  
    1.45  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    1.46 -\                 ==> K : parts (sees lost Spy evs)";
    1.47 +\                 ==> K : parts (sees Spy evs)";
    1.48  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.49  qed "Oops_parts_sees_Spy";
    1.50  
    1.51 @@ -71,42 +68,36 @@
    1.52  bind_thm ("OR4_parts_sees_Spy",
    1.53            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.54  
    1.55 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    1.56 -  We instantiate the variable to "lost" since leaving it as a Var would
    1.57 -  interfere with simplification.*)
    1.58 -val parts_induct_tac = 
    1.59 -    let val tac = forw_inst_tac [("lost","lost")] 
    1.60 -    in  etac otway.induct	   1 THEN 
    1.61 -	tac OR2_parts_sees_Spy     4 THEN 
    1.62 -        tac OR4_parts_sees_Spy     6 THEN
    1.63 -        tac Oops_parts_sees_Spy    7 THEN
    1.64 -	prove_simple_subgoals_tac  1
    1.65 -    end;
    1.66 +(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    1.67 +fun parts_induct_tac i = 
    1.68 +    etac otway.induct i			THEN 
    1.69 +    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
    1.70 +    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
    1.71 +    forward_tac [OR2_parts_sees_Spy]  (i+3) THEN 
    1.72 +    prove_simple_subgoals_tac  i;
    1.73  
    1.74  
    1.75 -(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.76 +(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    1.77      sends messages containing X! **)
    1.78  
    1.79  
    1.80  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.81  goal thy 
    1.82 - "!!evs. evs : otway lost \
    1.83 -\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.84 -by parts_induct_tac;
    1.85 + "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    1.86 +by (parts_induct_tac 1);
    1.87  by (Fake_parts_insert_tac 1);
    1.88  by (Blast_tac 1);
    1.89  qed "Spy_see_shrK";
    1.90  Addsimps [Spy_see_shrK];
    1.91  
    1.92  goal thy 
    1.93 - "!!evs. evs : otway lost \
    1.94 -\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.95 + "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    1.96  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.97  qed "Spy_analz_shrK";
    1.98  Addsimps [Spy_analz_shrK];
    1.99  
   1.100 -goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   1.101 -\                  evs : otway lost |] ==> A:lost";
   1.102 +goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   1.103 +\                  evs : otway |] ==> A:lost";
   1.104  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   1.105  qed "Spy_see_shrK_D";
   1.106  
   1.107 @@ -115,9 +106,9 @@
   1.108  
   1.109  
   1.110  (*Nobody can have used non-existent keys!*)
   1.111 -goal thy "!!evs. evs : otway lost ==>          \
   1.112 -\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   1.113 -by parts_induct_tac;
   1.114 +goal thy "!!evs. evs : otway ==>          \
   1.115 +\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   1.116 +by (parts_induct_tac 1);
   1.117  (*Fake*)
   1.118  by (best_tac
   1.119        (!claset addIs [impOfSubs analz_subset_parts]
   1.120 @@ -140,9 +131,8 @@
   1.121  (*Describes the form of K and NA when the Server sends this message.  Also
   1.122    for Oops case.*)
   1.123  goal thy 
   1.124 - "!!evs. [| Says Server B                                                 \
   1.125 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
   1.126 -\           evs : otway lost |]                                           \
   1.127 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
   1.128 +\           evs : otway |]                                           \
   1.129  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   1.130  by (etac rev_mp 1);
   1.131  by (etac otway.induct 1);
   1.132 @@ -151,11 +141,11 @@
   1.133  qed "Says_Server_message_form";
   1.134  
   1.135  
   1.136 -(*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.137 +(*For proofs involving analz.*)
   1.138  val analz_sees_tac = 
   1.139 -    dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
   1.140 -    dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   1.141 -    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.142 +    dtac OR2_analz_sees_Spy 4 THEN 
   1.143 +    dtac OR4_analz_sees_Spy 6 THEN
   1.144 +    forward_tac [Says_Server_message_form] 7 THEN
   1.145      assume_tac 7 THEN
   1.146      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   1.147  
   1.148 @@ -163,8 +153,8 @@
   1.149  (****
   1.150   The following is to prove theorems of the form
   1.151  
   1.152 -  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   1.153 -  Key K : analz (sees lost Spy evs)
   1.154 +  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   1.155 +  Key K : analz (sees Spy evs)
   1.156  
   1.157   A more general formula must be proved inductively.
   1.158  ****)
   1.159 @@ -174,10 +164,10 @@
   1.160  
   1.161  (*The equality makes the induction hypothesis easier to apply*)
   1.162  goal thy  
   1.163 - "!!evs. evs : otway lost ==>                                    \
   1.164 -\  ALL K KK. KK <= Compl (range shrK) -->                        \
   1.165 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
   1.166 -\            (K : KK | Key K : analz (sees lost Spy evs))";
   1.167 + "!!evs. evs : otway ==>                                    \
   1.168 +\  ALL K KK. KK <= Compl (range shrK) -->                   \
   1.169 +\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
   1.170 +\            (K : KK | Key K : analz (sees Spy evs))";
   1.171  by (etac otway.induct 1);
   1.172  by analz_sees_tac;
   1.173  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.174 @@ -191,9 +181,9 @@
   1.175  
   1.176  
   1.177  goal thy
   1.178 - "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
   1.179 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
   1.180 -\        (K = KAB | Key K : analz (sees lost Spy evs))";
   1.181 + "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
   1.182 +\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
   1.183 +\        (K = KAB | Key K : analz (sees Spy evs))";
   1.184  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.185  qed "analz_insert_freshK";
   1.186  
   1.187 @@ -201,7 +191,7 @@
   1.188  (*** The Key K uniquely identifies the Server's  message. **)
   1.189  
   1.190  goal thy 
   1.191 - "!!evs. evs : otway lost ==>                                             \
   1.192 + "!!evs. evs : otway ==>                                                  \
   1.193  \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
   1.194  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
   1.195  \     B=B' & NA=NA' & NB=NB' & X=X'";
   1.196 @@ -223,7 +213,7 @@
   1.197  \            : set evs;                                            \ 
   1.198  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
   1.199  \            : set evs;                                            \
   1.200 -\           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   1.201 +\           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   1.202  by (prove_unique_tac lemma 1);
   1.203  qed "unique_session_keys";
   1.204  
   1.205 @@ -233,13 +223,13 @@
   1.206  
   1.207  (*Only OR1 can have caused such a part of a message to appear.*)
   1.208  goal thy 
   1.209 - "!!evs. [| A ~: lost;  evs : otway lost |]                        \
   1.210 + "!!evs. [| A ~: lost;  evs : otway |]                             \
   1.211  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
   1.212 -\             : parts (sees lost Spy evs) -->                      \
   1.213 +\             : parts (sees Spy evs) -->                           \
   1.214  \            Says A B {|NA, Agent A, Agent B,                      \
   1.215  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   1.216  \             : set evs";
   1.217 -by parts_induct_tac;
   1.218 +by (parts_induct_tac 1);
   1.219  by (Fake_parts_insert_tac 1);
   1.220  qed_spec_mp "Crypt_imp_OR1";
   1.221  
   1.222 @@ -247,11 +237,11 @@
   1.223  (** The Nonce NA uniquely identifies A's message. **)
   1.224  
   1.225  goal thy 
   1.226 - "!!evs. [| evs : otway lost; A ~: lost |]               \
   1.227 -\ ==> EX B'. ALL B.                                      \
   1.228 -\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
   1.229 + "!!evs. [| evs : otway; A ~: lost |]               \
   1.230 +\ ==> EX B'. ALL B.                                 \
   1.231 +\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
   1.232  \        --> B = B'";
   1.233 -by parts_induct_tac;
   1.234 +by (parts_induct_tac 1);
   1.235  by (Fake_parts_insert_tac 1);
   1.236  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.237  (*OR1: creation of new Nonce.  Move assertion into global context*)
   1.238 @@ -260,9 +250,9 @@
   1.239  val lemma = result();
   1.240  
   1.241  goal thy 
   1.242 - "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
   1.243 -\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
   1.244 -\          evs : otway lost;  A ~: lost |]                                    \
   1.245 + "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \
   1.246 +\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \
   1.247 +\          evs : otway;  A ~: lost |]                                     \
   1.248  \        ==> B = C";
   1.249  by (prove_unique_tac lemma 1);
   1.250  qed "unique_NA";
   1.251 @@ -272,12 +262,12 @@
   1.252    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   1.253    over-simplified version of this protocol: see OtwayRees_Bad.*)
   1.254  goal thy 
   1.255 - "!!evs. [| A ~: lost;  evs : otway lost |]                      \
   1.256 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
   1.257 -\             : parts (sees lost Spy evs) -->                    \
   1.258 -\            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   1.259 -\             ~: parts (sees lost Spy evs)";
   1.260 -by parts_induct_tac;
   1.261 + "!!evs. [| A ~: lost;  evs : otway |]                      \
   1.262 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}        \
   1.263 +\             : parts (sees Spy evs) -->                    \
   1.264 +\            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   1.265 +\             ~: parts (sees Spy evs)";
   1.266 +by (parts_induct_tac 1);
   1.267  by (Fake_parts_insert_tac 1);
   1.268  by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   1.269                                 addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   1.270 @@ -287,8 +277,8 @@
   1.271  (*Crucial property: If the encrypted message appears, and A has used NA
   1.272    to start a run, then it originated with the Server!*)
   1.273  goal thy 
   1.274 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   1.275 -\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
   1.276 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                 \
   1.277 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)      \
   1.278  \        --> Says A B {|NA, Agent A, Agent B,                          \
   1.279  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   1.280  \             : set evs -->                                            \
   1.281 @@ -297,7 +287,7 @@
   1.282  \                   Crypt (shrK A) {|NA, Key K|},                      \
   1.283  \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   1.284  \                   : set evs)";
   1.285 -by parts_induct_tac;
   1.286 +by (parts_induct_tac 1);
   1.287  by (Fake_parts_insert_tac 1);
   1.288  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.289  by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.290 @@ -311,10 +301,10 @@
   1.291  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   1.292  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.293  by (blast_tac (!claset addSEs [MPair_parts]
   1.294 -                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.295 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.296                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.297                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   1.298 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.299 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.300                        addSEs [MPair_parts]
   1.301                        addIs  [unique_NA]) 1);
   1.302  qed_spec_mp "NA_Crypt_imp_Server_msg";
   1.303 @@ -330,7 +320,7 @@
   1.304  \           Says A B {|NA, Agent A, Agent B,                       \
   1.305  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   1.306  \            : set evs;                                            \
   1.307 -\           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   1.308 +\           A ~: lost;  A ~= Spy;  evs : otway |]                  \
   1.309  \        ==> EX NB. Says Server B                                  \
   1.310  \                     {|NA,                                        \
   1.311  \                       Crypt (shrK A) {|NA, Key K|},              \
   1.312 @@ -346,12 +336,12 @@
   1.313      the premises, e.g. by having A=Spy **)
   1.314  
   1.315  goal thy 
   1.316 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   1.317 -\        ==> Says Server B                                                 \
   1.318 -\              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   1.319 -\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->              \
   1.320 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
   1.321 -\            Key K ~: analz (sees lost Spy evs)";
   1.322 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
   1.323 +\        ==> Says Server B                                            \
   1.324 +\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.325 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   1.326 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   1.327 +\            Key K ~: analz (sees Spy evs)";
   1.328  by (etac otway.induct 1);
   1.329  by analz_sees_tac;
   1.330  by (ALLGOALS
   1.331 @@ -371,12 +361,12 @@
   1.332  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.333  
   1.334  goal thy 
   1.335 - "!!evs. [| Says Server B                                                \
   1.336 -\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   1.337 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
   1.338 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
   1.339 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.340 -\        ==> Key K ~: analz (sees lost Spy evs)";
   1.341 + "!!evs. [| Says Server B                                           \
   1.342 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.343 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   1.344 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   1.345 +\           A ~: lost;  B ~: lost;  evs : otway |]                  \
   1.346 +\        ==> Key K ~: analz (sees Spy evs)";
   1.347  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.348  by (blast_tac (!claset addSEs [lemma]) 1);
   1.349  qed "Spy_not_see_encrypted_key";
   1.350 @@ -387,14 +377,14 @@
   1.351  (*Only OR2 can have caused such a part of a message to appear.  We do not
   1.352    know anything about X: it does NOT have to have the right form.*)
   1.353  goal thy 
   1.354 - "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   1.355 + "!!evs. [| B ~: lost;  evs : otway |]                         \
   1.356  \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   1.357 -\             : parts (sees lost Spy evs) -->                  \
   1.358 +\             : parts (sees Spy evs) -->                       \
   1.359  \            (EX X. Says B Server                              \
   1.360  \             {|NA, Agent A, Agent B, X,                       \
   1.361  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.362  \             : set evs)";
   1.363 -by parts_induct_tac;
   1.364 +by (parts_induct_tac 1);
   1.365  by (Fake_parts_insert_tac 1);
   1.366  by (ALLGOALS Blast_tac);
   1.367  bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.368 @@ -403,11 +393,11 @@
   1.369  (** The Nonce NB uniquely identifies B's  message. **)
   1.370  
   1.371  goal thy 
   1.372 - "!!evs. [| evs : otway lost; B ~: lost |]               \
   1.373 + "!!evs. [| evs : otway; B ~: lost |]                    \
   1.374  \ ==> EX NA' A'. ALL NA A.                               \
   1.375 -\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   1.376 +\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
   1.377  \      --> NA = NA' & A = A'";
   1.378 -by parts_induct_tac;
   1.379 +by (parts_induct_tac 1);
   1.380  by (Fake_parts_insert_tac 1);
   1.381  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.382  (*OR2: creation of new Nonce.  Move assertion into global context*)
   1.383 @@ -417,10 +407,10 @@
   1.384  
   1.385  goal thy 
   1.386   "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   1.387 -\                  : parts(sees lost Spy evs);         \
   1.388 +\                  : parts(sees Spy evs);         \
   1.389  \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   1.390 -\                  : parts(sees lost Spy evs);         \
   1.391 -\          evs : otway lost;  B ~: lost |]             \
   1.392 +\                  : parts(sees Spy evs);         \
   1.393 +\          evs : otway;  B ~: lost |]             \
   1.394  \        ==> NC = NA & C = A";
   1.395  by (prove_unique_tac lemma 1);
   1.396  qed "unique_NB";
   1.397 @@ -429,8 +419,8 @@
   1.398  (*If the encrypted message appears, and B has used Nonce NB,
   1.399    then it originated with the Server!*)
   1.400  goal thy 
   1.401 - "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   1.402 -\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
   1.403 + "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway |]                        \
   1.404 +\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs)             \
   1.405  \        --> (ALL X'. Says B Server                                      \
   1.406  \                       {|NA, Agent A, Agent B, X',                      \
   1.407  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.408 @@ -439,7 +429,7 @@
   1.409  \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   1.410  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   1.411  \                   : set evs)";
   1.412 -by parts_induct_tac;
   1.413 +by (parts_induct_tac 1);
   1.414  by (Fake_parts_insert_tac 1);
   1.415  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.416  by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.417 @@ -448,11 +438,11 @@
   1.418  (*OR3*)
   1.419  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.420  by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   1.421 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.422 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.423                         addSEs [MPair_parts]
   1.424                         addDs  [unique_NB]) 2);
   1.425  by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.426 -                       addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.427 +                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.428                         delrules [conjI, impCE] (*stop split-up*)) 1);
   1.429  qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.430  
   1.431 @@ -460,7 +450,7 @@
   1.432  (*Guarantee for B: if it gets a message with matching NB then the Server
   1.433    has sent the correct message.*)
   1.434  goal thy 
   1.435 - "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   1.436 + "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway;                    \
   1.437  \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   1.438  \            : set evs;                                            \
   1.439  \           Says B Server {|NA, Agent A, Agent B, X',              \
   1.440 @@ -480,16 +470,16 @@
   1.441  
   1.442  
   1.443  goal thy 
   1.444 - "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   1.445 -\        ==> Says Server B                                            \
   1.446 -\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.447 -\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   1.448 -\            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   1.449 + "!!evs. [| B ~: lost;  evs : otway |]                           \
   1.450 +\        ==> Says Server B                                       \
   1.451 +\              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   1.452 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
   1.453 +\            (EX X. Says B Server {|NA, Agent A, Agent B, X,     \
   1.454  \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   1.455  \            : set evs)";
   1.456  by (etac otway.induct 1);
   1.457  by (ALLGOALS Asm_simp_tac);
   1.458 -by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   1.459 +by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   1.460  		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   1.461  by (ALLGOALS Blast_tac);
   1.462  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.463 @@ -502,7 +492,7 @@
   1.464   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   1.465  \           Says A B {|NA, Agent A, Agent B,                                \
   1.466  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   1.467 -\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |]          \
   1.468 +\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway |]               \
   1.469  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   1.470  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   1.471  \            : set evs";