src/HOL/Auth/Yahalom.ML
changeset 3519 ab0a9fbed4c0
parent 3516 470626799511
child 3543 82f33248d89d
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -16,14 +16,11 @@
     1.4  HOL_quantifiers := false;
     1.5  Pretty.setdepth 25;
     1.6  
     1.7 -(*Replacing the variable by a constant improves speed*)
     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 X NB K. EX evs: yahalom lost.     \
    1.15 +\        ==> EX X NB K. EX evs: yahalom.     \
    1.16  \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    1.17  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.18  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    1.19 @@ -35,7 +32,7 @@
    1.20  (**** Inductive proofs about yahalom ****)
    1.21  
    1.22  (*Nobody sends themselves messages*)
    1.23 -goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
    1.24 +goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
    1.25  by (etac yahalom.induct 1);
    1.26  by (Auto_tac());
    1.27  qed_spec_mp "not_Says_to_self";
    1.28 @@ -47,8 +44,8 @@
    1.29  
    1.30  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.31  goal thy "!!evs. Says S A {|Crypt (shrK A) Y, 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 "YM4_analz_sees_Spy";
    1.37  
    1.38  bind_thm ("YM4_parts_sees_Spy",
    1.39 @@ -56,45 +53,47 @@
    1.40  
    1.41  (*Relates to both YM4 and Oops*)
    1.42  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    1.43 -\                K : parts (sees lost Spy evs)";
    1.44 +\                K : parts (sees Spy evs)";
    1.45  by (blast_tac (!claset addSEs partsEs
    1.46 -                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
    1.47 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.48  qed "YM4_Key_parts_sees_Spy";
    1.49  
    1.50 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    1.51 -  We instantiate the variable to "lost" since leaving it as a Var would
    1.52 -  interfere with simplification.*)
    1.53 -val parts_sees_tac = 
    1.54 -    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
    1.55 -    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
    1.56 -    prove_simple_subgoals_tac  1;
    1.57 +(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    1.58 +fun parts_sees_tac i = 
    1.59 +    forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
    1.60 +    forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
    1.61 +    prove_simple_subgoals_tac  i;
    1.62  
    1.63 -val parts_induct_tac = 
    1.64 -    etac yahalom.induct 1 THEN parts_sees_tac;
    1.65 +(*Induction for regularity theorems.  If induction formula has the form
    1.66 +   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
    1.67 +   needless information about analz (insert X (sees Spy evs))  *)
    1.68 +fun parts_induct_tac i = 
    1.69 +    etac yahalom.induct i
    1.70 +    THEN 
    1.71 +    REPEAT (FIRSTGOAL analz_mono_contra_tac)
    1.72 +    THEN  parts_sees_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  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.80  goal thy 
    1.81 - "!!evs. evs : yahalom lost \
    1.82 -\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.83 -by parts_induct_tac;
    1.84 + "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    1.85 +by (parts_induct_tac 1);
    1.86  by (Fake_parts_insert_tac 1);
    1.87  by (Blast_tac 1);
    1.88  qed "Spy_see_shrK";
    1.89  Addsimps [Spy_see_shrK];
    1.90  
    1.91  goal thy 
    1.92 - "!!evs. evs : yahalom lost \
    1.93 -\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.94 + "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    1.95  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.96  qed "Spy_analz_shrK";
    1.97  Addsimps [Spy_analz_shrK];
    1.98  
    1.99 -goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   1.100 -\                  evs : yahalom lost |] ==> A:lost";
   1.101 +goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   1.102 +\                  evs : yahalom |] ==> A:lost";
   1.103  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   1.104  qed "Spy_see_shrK_D";
   1.105  
   1.106 @@ -103,9 +102,9 @@
   1.107  
   1.108  
   1.109  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   1.110 -goal thy "!!evs. evs : yahalom lost ==>          \
   1.111 -\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   1.112 -by parts_induct_tac;
   1.113 +goal thy "!!evs. evs : yahalom ==>          \
   1.114 +\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   1.115 +by (parts_induct_tac 1);
   1.116  (*YM4: Key K is not fresh!*)
   1.117  by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   1.118  (*YM3*)
   1.119 @@ -130,7 +129,7 @@
   1.120  goal thy 
   1.121   "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
   1.122  \             : set evs;                                                   \
   1.123 -\           evs : yahalom lost |]                                          \
   1.124 +\           evs : yahalom |]                                          \
   1.125  \        ==> K ~: range shrK";
   1.126  by (etac rev_mp 1);
   1.127  by (etac yahalom.induct 1);
   1.128 @@ -139,18 +138,18 @@
   1.129  qed "Says_Server_message_form";
   1.130  
   1.131  
   1.132 -(*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.133 +(*For proofs involving analz.*)
   1.134  val analz_sees_tac = 
   1.135 -    forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   1.136 -    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.137 +    forward_tac [YM4_analz_sees_Spy] 6 THEN
   1.138 +    forward_tac [Says_Server_message_form] 7 THEN
   1.139      assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   1.140  
   1.141  
   1.142  (****
   1.143   The following is to prove theorems of the form
   1.144  
   1.145 -  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   1.146 -  Key K : analz (sees lost Spy evs)
   1.147 +  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   1.148 +  Key K : analz (sees Spy evs)
   1.149  
   1.150   A more general formula must be proved inductively.
   1.151  ****)
   1.152 @@ -158,10 +157,10 @@
   1.153  (** Session keys are not used to encrypt other session keys **)
   1.154  
   1.155  goal thy  
   1.156 - "!!evs. evs : yahalom lost ==>                                 \
   1.157 + "!!evs. evs : yahalom ==>                                 \
   1.158  \  ALL K KK. KK <= Compl (range shrK) -->                       \
   1.159 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   1.160 -\            (K : KK | Key K : analz (sees lost Spy evs))";
   1.161 +\            (Key K : analz (Key``KK Un (sees Spy evs))) = \
   1.162 +\            (K : KK | Key K : analz (sees Spy evs))";
   1.163  by (etac yahalom.induct 1);
   1.164  by analz_sees_tac;
   1.165  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.166 @@ -174,9 +173,9 @@
   1.167  qed_spec_mp "analz_image_freshK";
   1.168  
   1.169  goal thy
   1.170 - "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   1.171 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
   1.172 -\        (K = KAB | Key K : analz (sees lost Spy evs))";
   1.173 + "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>             \
   1.174 +\        Key K : analz (insert (Key KAB) (sees Spy evs)) =       \
   1.175 +\        (K = KAB | Key K : analz (sees Spy evs))";
   1.176  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.177  qed "analz_insert_freshK";
   1.178  
   1.179 @@ -184,7 +183,7 @@
   1.180  (*** The Key K uniquely identifies the Server's  message. **)
   1.181  
   1.182  goal thy 
   1.183 - "!!evs. evs : yahalom lost ==>                                     \
   1.184 + "!!evs. evs : yahalom ==>                                     \
   1.185  \      EX A' B' na' nb' X'. ALL A B na nb X.                        \
   1.186  \          Says Server A                                            \
   1.187  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   1.188 @@ -209,7 +208,7 @@
   1.189  \          Says Server A'                                           \
   1.190  \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   1.191  \           : set evs;                                              \
   1.192 -\          evs : yahalom lost |]                                    \
   1.193 +\          evs : yahalom |]                                    \
   1.194  \       ==> A=A' & B=B' & na=na' & nb=nb'";
   1.195  by (prove_unique_tac lemma 1);
   1.196  qed "unique_session_keys";
   1.197 @@ -218,13 +217,13 @@
   1.198  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   1.199  
   1.200  goal thy 
   1.201 - "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.202 + "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]         \
   1.203  \        ==> Says Server A                                        \
   1.204  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   1.205  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.206  \             : set evs -->                                       \
   1.207  \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
   1.208 -\            Key K ~: analz (sees lost Spy evs)";
   1.209 +\            Key K ~: analz (sees Spy evs)";
   1.210  by (etac yahalom.induct 1);
   1.211  by analz_sees_tac;
   1.212  by (ALLGOALS
   1.213 @@ -250,37 +249,26 @@
   1.214  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.215  \             : set evs;                                          \
   1.216  \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   1.217 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.218 -\        ==> Key K ~: analz (sees lost Spy evs)";
   1.219 +\           A ~: lost;  B ~: lost;  evs : yahalom |]         \
   1.220 +\        ==> Key K ~: analz (sees Spy evs)";
   1.221  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.222  by (blast_tac (!claset addSEs [lemma]) 1);
   1.223  qed "Spy_not_see_encrypted_key";
   1.224  
   1.225  
   1.226 -(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   1.227 -  It simplifies the proof by discarding needless information about
   1.228 -	analz (insert X (sees lost Spy evs)) 
   1.229 -*)
   1.230 -fun analz_mono_parts_induct_tac i = 
   1.231 -    etac yahalom.induct i
   1.232 -    THEN 
   1.233 -    REPEAT_FIRST analz_mono_contra_tac
   1.234 -    THEN  parts_sees_tac;
   1.235 -
   1.236 -
   1.237  (** Security Guarantee for A upon receiving YM3 **)
   1.238  
   1.239  (*If the encrypted message appears then it originated with the Server*)
   1.240  goal thy
   1.241   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
   1.242 -\            : parts (sees lost Spy evs);                              \
   1.243 -\           A ~: lost;  evs : yahalom lost |]                          \
   1.244 +\            : parts (sees Spy evs);                              \
   1.245 +\           A ~: lost;  evs : yahalom |]                          \
   1.246  \         ==> Says Server A                                            \
   1.247  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   1.248  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   1.249  \             : set evs";
   1.250  by (etac rev_mp 1);
   1.251 -by parts_induct_tac;
   1.252 +by (parts_induct_tac 1);
   1.253  by (Fake_parts_insert_tac 1);
   1.254  qed "A_trusts_YM3";
   1.255  
   1.256 @@ -290,15 +278,15 @@
   1.257  (*B knows, by the first part of A's message, that the Server distributed 
   1.258    the key for A and B.  But this part says nothing about nonces.*)
   1.259  goal thy 
   1.260 - "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
   1.261 -\           B ~: lost;  evs : yahalom lost |]                           \
   1.262 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
   1.263 +\           B ~: lost;  evs : yahalom |]                           \
   1.264  \        ==> EX NA NB. Says Server A                                    \
   1.265  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.266  \                                           Nonce NA, Nonce NB|},       \
   1.267  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.268  \                       : set evs";
   1.269  by (etac rev_mp 1);
   1.270 -by parts_induct_tac;
   1.271 +by (parts_induct_tac 1);
   1.272  by (Fake_parts_insert_tac 1);
   1.273  (*YM3*)
   1.274  by (Blast_tac 1);
   1.275 @@ -308,15 +296,15 @@
   1.276    the key quoting nonce NB.  This part says nothing about agent names. 
   1.277    Secrecy of NB is crucial.*)
   1.278  goal thy 
   1.279 - "!!evs. evs : yahalom lost                                             \
   1.280 -\        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   1.281 -\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   1.282 + "!!evs. evs : yahalom                                             \
   1.283 +\        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
   1.284 +\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   1.285  \            (EX A B NA. Says Server A                                  \
   1.286  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.287  \                                  Nonce NA, Nonce NB|},                \
   1.288  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.289  \                       : set evs)";
   1.290 -by (analz_mono_parts_induct_tac 1);
   1.291 +by (parts_induct_tac 1);
   1.292  (*YM3 & Fake*)
   1.293  by (Blast_tac 2);
   1.294  by (Fake_parts_insert_tac 1);
   1.295 @@ -325,7 +313,7 @@
   1.296  (*A is uncompromised because NB is secure*)
   1.297  by (not_lost_tac "A" 1);
   1.298  (*A's certificate guarantees the existence of the Server message*)
   1.299 -by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
   1.300 +by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   1.301  			      A_trusts_YM3]) 1);
   1.302  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   1.303  
   1.304 @@ -364,7 +352,7 @@
   1.305   "!!evs. [| Says Server A                                                \
   1.306  \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
   1.307  \             : set evs;                                                 \
   1.308 -\           NB ~= NB';  evs : yahalom lost |]                            \
   1.309 +\           NB ~= NB';  evs : yahalom |]                            \
   1.310  \        ==> ~ KeyWithNonce K NB evs";
   1.311  by (blast_tac (!claset addDs [unique_session_keys]) 1);
   1.312  qed "Says_Server_KeyWithNonce";
   1.313 @@ -384,11 +372,11 @@
   1.314  val lemma = result();
   1.315  
   1.316  goal thy 
   1.317 - "!!evs. evs : yahalom lost ==>                                         \
   1.318 + "!!evs. evs : yahalom ==>                                         \
   1.319  \        (ALL KK. KK <= Compl (range shrK) -->                          \
   1.320  \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
   1.321 -\             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =     \
   1.322 -\             (Nonce NB : analz (sees lost Spy evs)))";
   1.323 +\             (Nonce NB : analz (Key``KK Un (sees Spy evs))) =     \
   1.324 +\             (Nonce NB : analz (sees Spy evs)))";
   1.325  by (etac yahalom.induct 1);
   1.326  by analz_sees_tac;
   1.327  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   1.328 @@ -410,7 +398,7 @@
   1.329  by (spy_analz_tac 1);
   1.330  (*YM4*)  (** LEVEL 7 **)
   1.331  by (not_lost_tac "A" 1);
   1.332 -by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.333 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   1.334      THEN REPEAT (assume_tac 1));
   1.335  by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   1.336  qed_spec_mp "Nonce_secrecy";
   1.337 @@ -423,9 +411,9 @@
   1.338   "!!evs. [| Says Server A                                                 \
   1.339  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   1.340  \           : set evs;                                                    \
   1.341 -\           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
   1.342 -\        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
   1.343 -\            (Nonce NB : analz (sees lost Spy evs))";
   1.344 +\           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
   1.345 +\        ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) =  \
   1.346 +\            (Nonce NB : analz (sees Spy evs))";
   1.347  by (asm_simp_tac (analz_image_freshK_ss addsimps 
   1.348  		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   1.349  qed "single_Nonce_secrecy";
   1.350 @@ -434,11 +422,11 @@
   1.351  (*** The Nonce NB uniquely identifies B's message. ***)
   1.352  
   1.353  goal thy 
   1.354 - "!!evs. evs : yahalom lost ==>                                            \
   1.355 + "!!evs. evs : yahalom ==>                                            \
   1.356  \   EX NA' A' B'. ALL NA A B.                                              \
   1.357 -\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees lost Spy evs) \
   1.358 +\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
   1.359  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   1.360 -by parts_induct_tac;
   1.361 +by (parts_induct_tac 1);
   1.362  (*Fake*)
   1.363  by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   1.364      THEN Fake_parts_insert_tac 1);
   1.365 @@ -451,10 +439,10 @@
   1.366  
   1.367  goal thy 
   1.368   "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
   1.369 -\                  : parts (sees lost Spy evs);            \
   1.370 +\                  : parts (sees Spy evs);            \
   1.371  \          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
   1.372 -\                  : parts (sees lost Spy evs);            \
   1.373 -\          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   1.374 +\                  : parts (sees Spy evs);            \
   1.375 +\          evs : yahalom;  B ~: lost;  B' ~: lost |]  \
   1.376  \        ==> NA' = NA & A' = A & B' = B";
   1.377  by (prove_unique_tac lemma 1);
   1.378  qed "unique_NB";
   1.379 @@ -467,29 +455,27 @@
   1.380  \            : set evs;          B ~: lost;                               \
   1.381  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
   1.382  \            : set evs;                                                   \
   1.383 -\          nb ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
   1.384 +\          nb ~: analz (sees Spy evs);  evs : yahalom |]        \
   1.385  \        ==> NA' = NA & A' = A & B' = B";
   1.386  by (not_lost_tac "B'" 1);
   1.387 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.388 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.389                         addSEs [MPair_parts]
   1.390                         addDs  [unique_NB]) 1);
   1.391  qed "Says_unique_NB";
   1.392  
   1.393 -val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
   1.394 -
   1.395  
   1.396  (** A nonce value is never used both as NA and as NB **)
   1.397  
   1.398  goal thy 
   1.399 - "!!evs. [| B ~: lost;  evs : yahalom lost  |]       \
   1.400 -\ ==> Nonce NB ~: analz (sees lost Spy evs) -->      \
   1.401 + "!!evs. [| B ~: lost;  evs : yahalom  |]            \
   1.402 +\ ==> Nonce NB ~: analz (sees Spy evs) -->           \
   1.403  \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
   1.404 -\       : parts(sees lost Spy evs)                   \
   1.405 +\       : parts(sees Spy evs)                        \
   1.406  \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
   1.407 -\       ~: parts(sees lost Spy evs)";
   1.408 -by (analz_mono_parts_induct_tac 1);
   1.409 +\       ~: parts(sees Spy evs)";
   1.410 +by (parts_induct_tac 1);
   1.411  by (Fake_parts_insert_tac 1);
   1.412 -by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
   1.413 +by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   1.414                         addSIs [parts_insertI]
   1.415                         addSEs partsEs) 1);
   1.416  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   1.417 @@ -498,7 +484,7 @@
   1.418  goal thy 
   1.419   "!!evs. [| Says Server A                                                \
   1.420  \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   1.421 -\           evs : yahalom lost |]                                        \
   1.422 +\           evs : yahalom |]                                             \
   1.423  \        ==> EX B'. Says B' Server                                       \
   1.424  \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.425  \                   : set evs";
   1.426 @@ -509,15 +495,14 @@
   1.427  qed "Says_Server_imp_YM2";
   1.428  
   1.429  
   1.430 -(*A vital theorem for B, that nonce NB remains secure from the Spy.
   1.431 -  Unusually, the Fake case requires Spy:lost.*)
   1.432 +(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
   1.433  goal thy 
   1.434 - "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   1.435 + "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]  \
   1.436  \ ==> Says B Server                                                    \
   1.437  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.438  \     : set evs -->                                                    \
   1.439  \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   1.440 -\     Nonce NB ~: analz (sees lost Spy evs)";
   1.441 +\     Nonce NB ~: analz (sees Spy evs)";
   1.442  by (etac yahalom.induct 1);
   1.443  by analz_sees_tac;
   1.444  by (ALLGOALS
   1.445 @@ -526,13 +511,13 @@
   1.446                            analz_insert_freshK] @ pushes)
   1.447                 setloop split_tac [expand_if])));
   1.448  (*Prove YM3 by showing that no NB can also be an NA*)
   1.449 -by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   1.450 +by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   1.451  	               addSEs [MPair_parts]
   1.452 -		       addDs  [no_nonce_YM1_YM2, Says_unique_NB']) 4
   1.453 +		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
   1.454      THEN flexflex_tac);
   1.455  (*YM2: similar freshness reasoning*) 
   1.456  by (blast_tac (!claset addSEs partsEs
   1.457 -		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
   1.458 +		       addDs  [Says_imp_sees_Spy RS analz.Inj,
   1.459  			       impOfSubs analz_subset_parts]) 3);
   1.460  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   1.461  by (blast_tac (!claset addSIs [parts_insertI]
   1.462 @@ -543,12 +528,12 @@
   1.463  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   1.464  by (REPEAT (Safe_step_tac 1));
   1.465  by (not_lost_tac "Aa" 1);
   1.466 -by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.467 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.468  by (forward_tac [Says_Server_message_form] 3);
   1.469  by (forward_tac [Says_Server_imp_YM2] 4);
   1.470  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   1.471 -(*  use Says_unique_NB' to identify message components: Aa=A, Ba=B, NAa=NA *)
   1.472 -by (blast_tac (!claset addDs [Says_unique_NB', Spy_not_see_encrypted_key,
   1.473 +(*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
   1.474 +by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   1.475  			      impOfSubs Fake_analz_insert]) 1);
   1.476  (** LEVEL 14 **)
   1.477  (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   1.478 @@ -558,11 +543,11 @@
   1.479  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.480  by (expand_case_tac "NB = NBa" 1);
   1.481  (*If NB=NBa then all other components of the Oops message agree*)
   1.482 -by (blast_tac (!claset addDs [Says_unique_NB']) 1 THEN flexflex_tac);
   1.483 +by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
   1.484  (*case NB ~= NBa*)
   1.485  by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   1.486  by (blast_tac (!claset addSEs [MPair_parts]
   1.487 -		       addDs  [Says_imp_sees_Spy' RS parts.Inj, 
   1.488 +		       addDs  [Says_imp_sees_Spy RS parts.Inj, 
   1.489  			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   1.490  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.491  
   1.492 @@ -579,20 +564,20 @@
   1.493  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.494  \                       Crypt K (Nonce NB)|} : set evs;                     \
   1.495  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   1.496 -\           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   1.497 +\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   1.498  \         ==> Says Server A                                                 \
   1.499  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   1.500  \                               Nonce NA, Nonce NB|},                       \
   1.501  \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   1.502  \               : set evs";
   1.503  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.504 -by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
   1.505 +by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   1.506      dtac B_trusts_YM4_shrK 1);
   1.507  by (dtac B_trusts_YM4_newK 3);
   1.508  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   1.509  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   1.510  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   1.511 -by (blast_tac (!claset addDs [Says_unique_NB']) 1);
   1.512 +by (blast_tac (!claset addDs [Says_unique_NB]) 1);
   1.513  qed "B_trusts_YM4";
   1.514  
   1.515  
   1.516 @@ -601,19 +586,19 @@
   1.517  
   1.518  (*The encryption in message YM2 tells us it cannot be faked.*)
   1.519  goal thy 
   1.520 - "!!evs. evs : yahalom lost                                            \
   1.521 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
   1.522 -\        : parts (sees lost Spy evs) -->                               \
   1.523 -\      B ~: lost -->                                                   \
   1.524 + "!!evs. evs : yahalom                                            \
   1.525 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                   \
   1.526 +\        : parts (sees Spy evs) -->                               \
   1.527 +\      B ~: lost -->                                              \
   1.528  \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.529  \         : set evs";
   1.530 -by parts_induct_tac;
   1.531 +by (parts_induct_tac 1);
   1.532  by (Fake_parts_insert_tac 1);
   1.533  bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   1.534  
   1.535  (*If the server sends YM3 then B sent YM2*)
   1.536  goal thy 
   1.537 - "!!evs. evs : yahalom lost                                                 \
   1.538 + "!!evs. evs : yahalom                                                      \
   1.539  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.540  \         : set evs -->                                                     \
   1.541  \      B ~: lost -->                                                        \
   1.542 @@ -624,7 +609,7 @@
   1.543  (*YM4*)
   1.544  by (Blast_tac 2);
   1.545  (*YM3*)
   1.546 -by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy' RS parts.Inj]
   1.547 +by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
   1.548  		      addSEs [MPair_parts]) 1);
   1.549  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.550  
   1.551 @@ -632,7 +617,7 @@
   1.552  goal thy
   1.553   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.554  \             : set evs;                                                    \
   1.555 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   1.556 +\           A ~: lost;  B ~: lost;  evs : yahalom |]                        \
   1.557  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.558  \         : set evs";
   1.559  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   1.560 @@ -646,14 +631,14 @@
   1.561    A has said NB.  We can't be sure about the rest of A's message, but only
   1.562    NB matters for freshness.*)  
   1.563  goal thy 
   1.564 - "!!evs. evs : yahalom lost                                             \
   1.565 -\        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   1.566 -\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   1.567 -\            Crypt (shrK B) {|Agent A, Key K|}                          \
   1.568 -\              : parts (sees lost Spy evs) -->                          \
   1.569 -\            B ~: lost -->                                              \
   1.570 + "!!evs. evs : yahalom                                             \
   1.571 +\        ==> Key K ~: analz (sees Spy evs) -->                     \
   1.572 +\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   1.573 +\            Crypt (shrK B) {|Agent A, Key K|}                     \
   1.574 +\              : parts (sees Spy evs) -->                          \
   1.575 +\            B ~: lost -->                                         \
   1.576  \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.577 -by (analz_mono_parts_induct_tac 1);
   1.578 +by (parts_induct_tac 1);
   1.579  (*Fake*)
   1.580  by (Fake_parts_insert_tac 1);
   1.581  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   1.582 @@ -664,7 +649,7 @@
   1.583  by (not_lost_tac "Aa" 1);
   1.584  by (blast_tac (!claset addSEs [MPair_parts]
   1.585                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.586 -		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   1.587 +		       addDs  [Says_imp_sees_Spy RS parts.Inj,
   1.588  			       unique_session_keys]) 1);
   1.589  val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   1.590  
   1.591 @@ -678,14 +663,14 @@
   1.592  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.593  \                       Crypt K (Nonce NB)|} : set evs;                     \
   1.594  \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   1.595 -\           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   1.596 +\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   1.597  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.598  by (dtac B_trusts_YM4 1);
   1.599  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   1.600 -by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   1.601 +by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
   1.602  by (rtac lemma 1);
   1.603  by (rtac Spy_not_see_encrypted_key 2);
   1.604  by (REPEAT_FIRST assume_tac);
   1.605  by (blast_tac (!claset addSEs [MPair_parts]
   1.606 -	       	       addDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   1.607 +	       	       addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.608  qed_spec_mp "YM4_imp_A_Said_YM3";