New guarantees for each line of protocol
authorpaulson
Tue Oct 08 10:26:23 1996 +0200 (1996-10-08)
changeset 207084f4572a6b20
parent 2069 a1c623f70407
child 2071 0debdc018d26
New guarantees for each line of protocol
src/HOL/Auth/NS_Shared.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Oct 08 10:21:04 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Oct 08 10:26:23 1996 +0200
     1.3 @@ -55,8 +55,28 @@
     1.4                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
     1.5  qed "NS3_msg_in_parts_sees_Spy";
     1.6                                
     1.7 +goal thy
     1.8 +    "!!evs. Says S A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs ==> \
     1.9 +\                K : parts (sees lost Spy evs)";
    1.10 +by (fast_tac (!claset addSEs partsEs
    1.11 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.12 +qed "Reveal_parts_sees_Spy";
    1.13 +
    1.14  val parts_Fake_tac = 
    1.15 -    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5;
    1.16 +    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
    1.17 +    forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 8;
    1.18 +
    1.19 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.20 +fun parts_induct_tac i = SELECT_GOAL
    1.21 +    (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN
    1.22 +	     (*Fake message*)
    1.23 +	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.24 +					   impOfSubs Fake_parts_insert]
    1.25 +                                    addss (!simpset)) 2)) THEN
    1.26 +     (*Base case*)
    1.27 +     fast_tac (!claset addss (!simpset)) 1 THEN
    1.28 +     ALLGOALS Asm_simp_tac) i;
    1.29 +
    1.30  
    1.31  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.32      sends messages containing X! **)
    1.33 @@ -65,12 +85,8 @@
    1.34  goal thy 
    1.35   "!!evs. [| evs : ns_shared lost; A ~: lost |]    \
    1.36  \        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.37 -by (etac ns_shared.induct 1);
    1.38 -by parts_Fake_tac;
    1.39 +by (parts_induct_tac 1);
    1.40  by (Auto_tac());
    1.41 -(*Deals with Fake message*)
    1.42 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.43 -                             impOfSubs Fake_parts_insert]) 1);
    1.44  qed "Spy_not_see_shrK";
    1.45  
    1.46  bind_thm ("Spy_not_analz_shrK",
    1.47 @@ -107,6 +123,7 @@
    1.48  Addsimps [shrK_mem_analz];
    1.49  
    1.50  
    1.51 +
    1.52  (*** Future keys can't be seen or used! ***)
    1.53  
    1.54  (*Nobody can have SEEN keys that will be generated in the future.
    1.55 @@ -118,10 +135,7 @@
    1.56  goal thy "!!evs. evs : ns_shared lost ==> \
    1.57  \                length evs <= length evs' --> \
    1.58  \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    1.59 -by (etac ns_shared.induct 1);
    1.60 -by parts_Fake_tac;
    1.61 -(*auto_tac does not work here, as it performs safe_tac first*)
    1.62 -by (ALLGOALS Asm_simp_tac);
    1.63 +by (parts_induct_tac 1);
    1.64  by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.65                                         impOfSubs parts_insert_subset_Un,
    1.66                                         Suc_leD]
    1.67 @@ -149,28 +163,68 @@
    1.68  qed "Says_imp_old_keys";
    1.69  
    1.70  
    1.71 +
    1.72 +(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
    1.73 +
    1.74 +goal thy "!!evs. evs : ns_shared lost ==> \
    1.75 +\                length evs <= length evt --> \
    1.76 +\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
    1.77 +by (etac ns_shared.induct 1);
    1.78 +(*auto_tac does not work here, as it performs safe_tac first*)
    1.79 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
    1.80 +                                     addcongs [disj_cong])));
    1.81 +by (REPEAT_FIRST (fast_tac (!claset 
    1.82 +                              addSEs partsEs
    1.83 +                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.84 +                              addDs  [impOfSubs analz_subset_parts,
    1.85 +                                      impOfSubs parts_insert_subset_Un,
    1.86 +                                      Suc_leD]
    1.87 +                              addss (!simpset))));
    1.88 +val lemma = result();
    1.89 +
    1.90 +(*Variant needed below*)
    1.91 +goal thy 
    1.92 + "!!evs. [| evs : ns_shared lost;  length evs <= length evs' |]    \
    1.93 +\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
    1.94 +by (fast_tac (!claset addDs [lemma]) 1);
    1.95 +qed "new_nonces_not_seen";
    1.96 +Addsimps [new_nonces_not_seen];
    1.97 +
    1.98 +(*Another variant: old messages must contain old nonces!*)
    1.99 +goal thy 
   1.100 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.101 +\           Nonce (newN evt) : parts {X};    \
   1.102 +\           evs : ns_shared lost                 \
   1.103 +\        |] ==> length evt < length evs";
   1.104 +by (rtac ccontr 1);
   1.105 +by (dtac leI 1);
   1.106 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   1.107 +                      addIs  [impOfSubs parts_mono]) 1);
   1.108 +qed "Says_imp_old_nonces";
   1.109 +
   1.110 +
   1.111  (*Nobody can have USED keys that will be generated in the future.
   1.112    ...very like new_keys_not_seen*)
   1.113  goal thy "!!evs. evs : ns_shared lost ==> \
   1.114  \                length evs <= length evs' --> \
   1.115  \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   1.116 -by (etac ns_shared.induct 1);
   1.117 -by parts_Fake_tac;
   1.118 -by (ALLGOALS Asm_simp_tac);
   1.119 +by (parts_induct_tac 1);
   1.120  (*NS1 and NS2*)
   1.121 -map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
   1.122 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]));
   1.123  (*Fake and NS3*)
   1.124 -map (by o best_tac
   1.125 -     (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.126 -                     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.127 -                     Suc_leD]
   1.128 -              addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.129 -              addss (!simpset)))
   1.130 -    [2,1];
   1.131 +by (EVERY 
   1.132 +    (map
   1.133 +     (best_tac
   1.134 +      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.135 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.136 +                      Suc_leD]
   1.137 +               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.138 +               addss (!simpset)))
   1.139 +     [2,1]));
   1.140  (*NS4 and NS5: nonce exchange*)
   1.141  by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
   1.142                                    addIs  [less_SucI, impOfSubs keysFor_mono]
   1.143 -                                  addss (!simpset addsimps [le_def])) 0));
   1.144 +                                  addss (!simpset addsimps [le_def])) 1));
   1.145  val lemma = result();
   1.146  
   1.147  goal thy 
   1.148 @@ -202,16 +256,17 @@
   1.149  qed "Says_Server_message_form";
   1.150  
   1.151  
   1.152 -(*Describes the form of X when the following message is sent.  The use of
   1.153 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.154 -  assumptions on A are needed to prevent its being a Faked message.*)
   1.155 +(*If the encrypted message appears then it originated with the Server*)
   1.156  goal thy
   1.157 - "!!evs. evs : ns_shared lost ==>                                         \
   1.158 -\            Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)               \
   1.159 -\               : parts (sees lost Spy evs) &                           \
   1.160 -\            A ~: lost -->                                                \
   1.161 -\          (EX evt: ns_shared lost. K = newK evt & \
   1.162 -\                             X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.163 + "!!evs. [| Crypt {|NA, Agent B, Key K, X|} (shrK A)                   \
   1.164 +\            : parts (sees lost Spy evs);                              \
   1.165 +\           A ~: lost;  evs : ns_shared lost |]                        \
   1.166 +\         ==> X = (Crypt {|Key K, Agent A|} (shrK B)) &                \
   1.167 +\             Says Server A                                            \
   1.168 +\              (Crypt {|NA, Agent B, Key K,                            \
   1.169 +\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
   1.170 +\             : set_of_list evs";
   1.171 +by (etac rev_mp 1);
   1.172  by (etac ns_shared.induct 1);
   1.173  by parts_Fake_tac;
   1.174  (*Fake case*)
   1.175 @@ -219,30 +274,27 @@
   1.176                        addDs  [impOfSubs analz_subset_parts]
   1.177                        addss  (!simpset)) 2);
   1.178  by (Auto_tac());
   1.179 -val lemma = result() RS mp;
   1.180 -
   1.181 -
   1.182 -(*The following theorem is proved by cases.  If the message was sent with a
   1.183 -  bad key then the Spy reads it -- even if he didn't send it in the first
   1.184 -  place.*)
   1.185 +qed "A_trust_NS2";
   1.186  
   1.187  
   1.188  (*EITHER describes the form of X when the following message is sent, 
   1.189    OR     reduces it to the Fake case.
   1.190    Use Says_Server_message_form if applicable.*)
   1.191  goal thy 
   1.192 - "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))    \
   1.193 -\            : set_of_list evs;  evs : ns_shared lost |]                      \
   1.194 -\        ==> (EX evt: ns_shared lost. K = newK evt & length evt < length evs & \
   1.195 -\                               X = (Crypt {|Key K, Agent A|} (shrK B))) | \
   1.196 -\            X : analz (sees lost Spy evs)";
   1.197 + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))      \
   1.198 +\            : set_of_list evs;  evs : ns_shared lost |]                   \
   1.199 +\        ==> (EX evt: ns_shared lost. K = newK evt &                       \
   1.200 +\                               length evt < length evs &                  \
   1.201 +\                               X = (Crypt {|Key K, Agent A|} (shrK B)))   \
   1.202 +\          | X : analz (sees lost Spy evs)";
   1.203  by (excluded_middle_tac "A : lost" 1);
   1.204  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.205                        addss (!simpset)) 2);
   1.206 -by (forward_tac [lemma] 1);
   1.207 +by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
   1.208  by (fast_tac (!claset addEs  partsEs
   1.209 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.210 -by (fast_tac (!claset addIs [Says_imp_old_keys] addss (!simpset)) 1);
   1.211 +                      addSDs [A_trust_NS2, Says_Server_message_form]
   1.212 +		      addIs [Says_imp_old_keys]
   1.213 +                      addss (!simpset)) 1);
   1.214  qed "Says_S_message_form";
   1.215  
   1.216  
   1.217 @@ -267,7 +319,7 @@
   1.218  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   1.219  by (etac ns_shared.induct 1);
   1.220  by parts_Fake_tac;
   1.221 -by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.222 +by (ALLGOALS Asm_simp_tac);
   1.223  (*Deals with Faked messages*)
   1.224  by (best_tac (!claset addSEs partsEs
   1.225                        addDs [impOfSubs parts_insert_subset_Un]
   1.226 @@ -279,6 +331,36 @@
   1.227  
   1.228  (** Session keys are not used to encrypt other session keys **)
   1.229  
   1.230 +(*Describes the form of Key K when the following message is sent.  The use of
   1.231 +  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.232 +  assumption A ~: lost prevents its being a Faked message. *)
   1.233 +goal thy
   1.234 + "!!evs. evs: ns_shared lost ==>                                           \
   1.235 +\        Crypt {|NA, Agent B, Key K, X|} (shrK A)          \
   1.236 +\          : parts (sees lost Spy evs)   &   A ~: lost              \
   1.237 +\        --> (EX evt: ns_shared lost. K = newK evt)";
   1.238 +by (parts_induct_tac 1);
   1.239 +by (Auto_tac());
   1.240 +val lemma = result() RS mp;
   1.241 +
   1.242 +
   1.243 +(*EITHER describes the form of Key K when the following message is sent, 
   1.244 +  OR     reduces it to the Fake case.*)
   1.245 +goal thy 
   1.246 + "!!evs. [| Says S A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
   1.247 +\           : set_of_list evs;  \
   1.248 +\           evs : ns_shared lost |]                      \
   1.249 +\        ==> (EX evt: ns_shared lost. K = newK evt)          \
   1.250 +\          | Key K : analz (sees lost Spy evs)";
   1.251 +by (excluded_middle_tac "A : lost" 1);
   1.252 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.253 +                      addss (!simpset)) 2);
   1.254 +by (forward_tac [lemma] 1);
   1.255 +by (fast_tac (!claset addEs  partsEs
   1.256 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.257 +by (Fast_tac 1);
   1.258 +qed "Reveal_message_form";
   1.259 +
   1.260  (*The equality makes the induction hypothesis easier to apply*)
   1.261  goal thy  
   1.262   "!!evs. evs : ns_shared lost ==> \
   1.263 @@ -286,22 +368,20 @@
   1.264  \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.265  by (etac ns_shared.induct 1);
   1.266  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.267 -by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
   1.268 +by (dtac Reveal_message_form 8);
   1.269 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac));
   1.270  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   1.271  by (ALLGOALS 
   1.272      (asm_simp_tac 
   1.273       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.274                           @ pushes)
   1.275                 setloop split_tac [expand_if])));
   1.276 -(** LEVEL 5 **)
   1.277 -(*NS3, Fake subcase*)
   1.278 -by (spy_analz_tac 5);
   1.279 -(*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   1.280 +(** LEVEL 6 **)
   1.281 +(*Reveal case 2, NS3, Fake*) 
   1.282 +by (EVERY (map spy_analz_tac [7,5,2]));
   1.283 +by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.284 +(*NS3, NS2, Base*)
   1.285  by (REPEAT (Fast_tac 3));
   1.286 -(*Fake case*) (** LEVEL 7 **)
   1.287 -by (spy_analz_tac 2);
   1.288 -(*Base case*)
   1.289 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.290  qed_spec_mp "analz_image_newK";
   1.291  
   1.292  
   1.293 @@ -321,63 +401,59 @@
   1.294  fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.295  
   1.296  goal thy 
   1.297 - "!!evs. evs : ns_shared lost ==>                             \
   1.298 -\      EX X'. ALL A X N B.                               \
   1.299 -\       A ~: lost -->                                     \
   1.300 -\       Crypt {|N, Agent B, Key K, X|} (shrK A) : parts (sees lost Spy evs) --> \
   1.301 -\       X=X'";
   1.302 -by (Simp_tac 1);        (*Miniscoping*)
   1.303 + "!!evs. evs : ns_shared lost ==>                                            \
   1.304 +\      EX A' NA' B' X'. ALL A NA B X.                                        \
   1.305 +\       Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))         \
   1.306 +\       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
   1.307  by (etac ns_shared.induct 1);
   1.308  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.309 -by (ALLGOALS 
   1.310 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   1.311 -                                      imp_conj_distrib, parts_insert_sees])));
   1.312 -by (REPEAT_FIRST (eresolve_tac [exE,disjE]));
   1.313 -(*NS2: Cextraction of K = newK evsa to global context...*) 
   1.314 -(** LEVEL 5 **)
   1.315 -by (excluded_middle_tac "K = newK evsa" 3);
   1.316 -by (Asm_simp_tac 3);
   1.317 -by (etac exI 3);
   1.318 -(*...we assume X is a very new message, and handle this case by contradiction*)
   1.319 -by (fast_tac (!claset addSEs partsEs
   1.320 -                      addEs [Says_imp_old_keys RS less_irrefl]
   1.321 -                      addss (!simpset)) 3);
   1.322 -(*Base, Fake, NS3*) (** LEVEL 9 **)
   1.323 -by (REPEAT_FIRST ex_strip_tac);
   1.324 -by (dtac synth.Inj 4);
   1.325 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   1.326 -                                    addss (!simpset))));
   1.327 +by (REPEAT_FIRST (eresolve_tac [conjE, bexE, disjE] ORELSE' hyp_subst_tac));
   1.328 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.329 +by (step_tac (!claset delrules [conjI]) 1);
   1.330 +(*NS3*)
   1.331 +by (ex_strip_tac 2);
   1.332 +by (Fast_tac 2);
   1.333 +(*NS2: it can't be a new key*)
   1.334 +by (expand_case_tac "K = ?y" 1);
   1.335 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.336 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.337 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.338 +                      addss (!simpset addsimps [parts_insertI])) 1);
   1.339  val lemma = result();
   1.340  
   1.341  (*In messages of this form, the session key uniquely identifies the rest*)
   1.342  goal thy 
   1.343 - "!!evs. [| Says S A          \
   1.344 -\             (Crypt {|N, Agent B, Key K, X|} (shrK C))     \
   1.345 -\                  : set_of_list evs; \ 
   1.346 -\           Says S' A'                                         \
   1.347 -\             (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
   1.348 -\                  : set_of_list evs;                         \
   1.349 -\           evs : ns_shared lost;  C ~: lost;  C' ~: lost |] ==> X = X'";
   1.350 + "!!evs. [| Says Server A                                    \
   1.351 +\             (Crypt {|NA, Agent B, Key K, X|} (shrK A))     \
   1.352 +\                  : set_of_list evs;                        \ 
   1.353 +\           Says Server A'                                   \
   1.354 +\             (Crypt {|NA', Agent B', Key K, X'|} (shrK A')) \
   1.355 +\                  : set_of_list evs;                        \
   1.356 +\           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
   1.357  by (dtac lemma 1);
   1.358 -by (etac exE 1);
   1.359 +by (REPEAT (etac exE 1));
   1.360  (*Duplicate the assumption*)
   1.361 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.362 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.363 +by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1);
   1.364 +by (fast_tac (!claset addSDs [ spec] 
   1.365 +	              delrules [conjI] addss (!simpset)) 1);
   1.366  qed "unique_session_keys";
   1.367  
   1.368  
   1.369 -
   1.370  (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   1.371  
   1.372  goal thy 
   1.373   "!!evs. [| A ~: lost;  B ~: lost;  \
   1.374  \           evs : ns_shared lost;  evt: ns_shared lost |]  \
   1.375  \        ==> Says Server A                                             \
   1.376 -\              (Crypt {|N, Agent B, Key K,                     \
   1.377 -\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \
   1.378 -\             : set_of_list evs --> \
   1.379 +\              (Crypt {|NA, Agent B, Key K,                            \
   1.380 +\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
   1.381 +\             : set_of_list evs -->                                    \
   1.382 +\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
   1.383  \        Key K ~: analz (sees lost Spy evs)";
   1.384  by (etac ns_shared.induct 1);
   1.385 +by (forward_tac [Reveal_message_form] 8);
   1.386 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.387 +by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.388  by (ALLGOALS 
   1.389      (asm_simp_tac 
   1.390       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.391 @@ -387,48 +463,117 @@
   1.392  by (fast_tac (!claset addIs [parts_insertI]
   1.393                        addEs [Says_imp_old_keys RS less_irrefl]
   1.394                        addss (!simpset)) 2);
   1.395 -(*Fake case*)
   1.396 -by (spy_analz_tac 1);
   1.397 -(*NS3: that message from the Server was sent earlier*)
   1.398 -by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
   1.399 -by (Step_tac 1);
   1.400 -by (REPEAT_FIRST assume_tac);
   1.401 -by (spy_analz_tac 2);           (*Prove the Fake subcase*)
   1.402 -by (asm_full_simp_tac
   1.403 -    (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   1.404 -by (Step_tac 1);
   1.405 -(**LEVEL 10 **)
   1.406 -by (excluded_middle_tac "Aa : lost" 1);
   1.407 -(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
   1.408 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   1.409 -by (fast_tac (!claset addSDs [analz.Decrypt]
   1.410 -                      addss (!simpset)) 2);
   1.411 -(*So now we have  Aa ~: lost *)
   1.412 -by (dtac unique_session_keys 1);
   1.413 -by (Auto_tac ());
   1.414 -val lemma = result() RS mp RSN(2,rev_notE);
   1.415 +(*Revl case 2, OR4, OR2, Fake*) 
   1.416 +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.417 +(*NS3 and Revl subcases*) (**LEVEL 7 **)
   1.418 +by (step_tac (!claset delrules [impCE]) 1);
   1.419 +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.420 +be conjE 2;
   1.421 +by (mp_tac 2);
   1.422 +(**LEVEL 11 **)
   1.423 +by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 2);
   1.424 +ba 3;
   1.425 +by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2);
   1.426 +by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
   1.427 +(*NS3*)
   1.428 +by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 1);
   1.429 +ba 2;
   1.430 +by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
   1.431 +by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.432 +val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.433  
   1.434  
   1.435  (*Final version: Server's message in the most abstract form*)
   1.436  goal thy 
   1.437 - "!!evs. [| Says Server A                                                \
   1.438 -\            (Crypt {|N, Agent B, K, X|} K') : set_of_list evs;          \
   1.439 -\           A ~: lost;  B ~: lost;  evs : ns_shared lost                        \
   1.440 -\        |] ==>                                                          \
   1.441 -\     K ~: analz (sees lost Spy evs)";
   1.442 + "!!evs. [| Says Server A                                               \
   1.443 +\            (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs;        \
   1.444 +\           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
   1.445 +\           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   1.446 +\        |] ==> K ~: analz (sees lost Spy evs)";
   1.447  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.448  by (fast_tac (!claset addSEs [lemma]) 1);
   1.449  qed "Spy_not_see_encrypted_key";
   1.450  
   1.451  
   1.452  goal thy 
   1.453 - "!!evs. [| C ~: {A,B,Server}; \
   1.454 -\           Says Server A                                                \
   1.455 -\            (Crypt {|N, Agent B, K, X|} K') : set_of_list evs;          \
   1.456 -\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]                  \
   1.457 + "!!evs. [| C ~: {A,B,Server};                                          \
   1.458 +\           Says Server A                                               \
   1.459 +\            (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs;        \
   1.460 +\           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
   1.461 +\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   1.462  \        ==> K ~: analz (sees lost C evs)";
   1.463  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.464  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.465  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.466  by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   1.467  qed "Agent_not_see_encrypted_key";
   1.468 +
   1.469 +
   1.470 +
   1.471 +(**** Guarantees available at various stages of protocol ***)
   1.472 +
   1.473 +A_trust_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
   1.474 +
   1.475 +
   1.476 +(*If the encrypted message appears then it originated with the Server*)
   1.477 +goal thy
   1.478 + "!!evs. [| Crypt {|Key K, Agent A|} (shrK B) : parts (sees lost Spy evs); \
   1.479 +\           B ~: lost;  evs : ns_shared lost |]                        \
   1.480 +\         ==> EX NA. Says Server A                                     \
   1.481 +\              (Crypt {|NA, Agent B, Key K,                            \
   1.482 +\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
   1.483 +\             : set_of_list evs";
   1.484 +by (etac rev_mp 1);
   1.485 +by (etac ns_shared.induct 1);
   1.486 +by parts_Fake_tac;
   1.487 +(*Fake case*)
   1.488 +by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   1.489 +                      addDs  [impOfSubs analz_subset_parts]
   1.490 +                      addss  (!simpset)) 2);
   1.491 +by (Auto_tac());
   1.492 +qed "B_trust_NS3";
   1.493 +
   1.494 +
   1.495 +goal thy
   1.496 + "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs);            \
   1.497 +\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
   1.498 +\        ==> Says Server A                                             \
   1.499 +\              (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
   1.500 +\             : set_of_list evs \
   1.501 +\            --> (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) \
   1.502 +\                 --> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
   1.503 +by (etac rev_mp 1);
   1.504 +by (etac ns_shared.induct 1);
   1.505 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.506 +by parts_Fake_tac;
   1.507 +by (ALLGOALS
   1.508 +    (asm_simp_tac (!simpset addsimps [de_Morgan_disj, all_conj_distrib])));
   1.509 +(**LEVEL 5**)
   1.510 +by (REPEAT_FIRST (rtac impI));
   1.511 +by (subgoal_tac "Key K ~: analz (sees lost Spy evsa)" 1);
   1.512 +by (fast_tac (!claset addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 2);
   1.513 +by (best_tac (!claset addSDs [Crypt_Fake_parts_insert]
   1.514 +                      addSIs  [disjI2,
   1.515 +			       impOfSubs (sees_subset_sees_Says RS analz_mono)]
   1.516 +                      addss  (!simpset)) 1);
   1.517 +by (fast_tac (!claset addSIs  [impOfSubs (sees_subset_sees_Says RS analz_mono)]
   1.518 +                      addss  (!simpset)) 2);
   1.519 +(**LEVEL 10**)
   1.520 +(*Contradiction from the assumption   
   1.521 +   Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *)
   1.522 +bd Crypt_imp_invKey_keysFor 1;
   1.523 +by (Asm_full_simp_tac 1);
   1.524 +
   1.525 +fr disjI1;
   1.526 +by (REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac));
   1.527 +by (thin_tac "?PP-->?QQ" 1);
   1.528 +by (subgoal_tac "Key K ~: analz (sees lost Spy evsa)" 1);
   1.529 +by (fast_tac (!claset addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 2);
   1.530 +by (case_tac "Ba : lost" 1);
   1.531 +by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
   1.532 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trust_NS3) 1 THEN 
   1.533 +    REPEAT (assume_tac 1));
   1.534 +be exE 1;
   1.535 +by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   1.536 +by (Fast_tac 1);
   1.537 +qed "A_trust_NS4";