New version of Yahalom, as recommended on p 259 of BAN paper
authorpaulson
Fri Oct 18 11:43:14 1996 +0200 (1996-10-18)
changeset 211181c8d46edfa3
parent 2110 d01151e66cd4
child 2112 3902e9af752f
New version of Yahalom, as recommended on p 259 of BAN paper
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Oct 18 11:43:14 1996 +0200
     1.3 @@ -0,0 +1,456 @@
     1.4 +(*  Title:      HOL/Auth/Yahalom2
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
    1.10 +
    1.11 +This version trades encryption of NB for additional explicitness in YM3.
    1.12 +
    1.13 +From page 259 of
    1.14 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.15 +  Proc. Royal Soc. 426 (1989)
    1.16 +*)
    1.17 +
    1.18 +open Yahalom2;
    1.19 +
    1.20 +proof_timing:=true;
    1.21 +HOL_quantifiers := false;
    1.22 +
    1.23 +
    1.24 +(*Weak liveness: there are traces that reach the end*)
    1.25 +
    1.26 +goal thy 
    1.27 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.28 +\        ==> EX X NB K. EX evs: yahalom lost.          \
    1.29 +\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    1.30 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.31 +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    1.32 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.33 +by (ALLGOALS Fast_tac);
    1.34 +result();
    1.35 +
    1.36 +
    1.37 +(**** Inductive proofs about yahalom ****)
    1.38 +
    1.39 +(*Monotonicity*)
    1.40 +goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    1.41 +by (rtac subsetI 1);
    1.42 +by (etac yahalom.induct 1);
    1.43 +by (REPEAT_FIRST
    1.44 +    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    1.45 +                              :: yahalom.intrs))));
    1.46 +qed "yahalom_mono";
    1.47 +
    1.48 +
    1.49 +(*Nobody sends themselves messages*)
    1.50 +goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.51 +by (etac yahalom.induct 1);
    1.52 +by (Auto_tac());
    1.53 +qed_spec_mp "not_Says_to_self";
    1.54 +Addsimps [not_Says_to_self];
    1.55 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.56 +
    1.57 +
    1.58 +(** For reasoning about the encrypted portion of messages **)
    1.59 +
    1.60 +(*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.61 +goal thy "!!evs. Says S A {|NB, Crypt Y (shrK A), X|} : set_of_list evs ==> \
    1.62 +\                X : analz (sees lost Spy evs)";
    1.63 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.64 +qed "YM4_analz_sees_Spy";
    1.65 +
    1.66 +bind_thm ("YM4_parts_sees_Spy",
    1.67 +          YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.68 +
    1.69 +(*Relates to both YM4 and Revl*)
    1.70 +goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
    1.71 +\                  : set_of_list evs ==> \
    1.72 +\                K : parts (sees lost Spy evs)";
    1.73 +by (fast_tac (!claset addSEs partsEs
    1.74 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.75 +qed "YM4_Key_parts_sees_Spy";
    1.76 +
    1.77 +(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    1.78 +  harder: the simplifier does less.*)
    1.79 +val parts_Fake_tac = 
    1.80 +    forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
    1.81 +    forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
    1.82 +
    1.83 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.84 +fun parts_induct_tac i = SELECT_GOAL
    1.85 +    (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
    1.86 +	     (*Fake message*)
    1.87 +	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.88 +					   impOfSubs Fake_parts_insert]
    1.89 +                                    addss (!simpset)) 2)) THEN
    1.90 +     (*Base case*)
    1.91 +     fast_tac (!claset addss (!simpset)) 1 THEN
    1.92 +     ALLGOALS Asm_simp_tac) i;
    1.93 +
    1.94 +
    1.95 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.96 +    sends messages containing X! **)
    1.97 +
    1.98 +(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
    1.99 +goal thy 
   1.100 + "!!evs. [| evs : yahalom lost;  A ~: lost |]    \
   1.101 +\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
   1.102 +by (parts_induct_tac 1);
   1.103 +by (Auto_tac());
   1.104 +qed "Spy_not_see_shrK";
   1.105 +
   1.106 +bind_thm ("Spy_not_analz_shrK",
   1.107 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   1.108 +
   1.109 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   1.110 +
   1.111 +(*We go to some trouble to preserve R in the 3rd and 4th subgoals
   1.112 +  As usual fast_tac cannot be used because it uses the equalities too soon*)
   1.113 +val major::prems = 
   1.114 +goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   1.115 +\             evs : yahalom lost;                               \
   1.116 +\             A:lost ==> R                                  \
   1.117 +\           |] ==> R";
   1.118 +by (rtac ccontr 1);
   1.119 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   1.120 +by (swap_res_tac prems 2);
   1.121 +by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.122 +qed "Spy_see_shrK_E";
   1.123 +
   1.124 +bind_thm ("Spy_analz_shrK_E", 
   1.125 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   1.126 +
   1.127 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   1.128 +
   1.129 +
   1.130 +(*** Future keys can't be seen or used! ***)
   1.131 +
   1.132 +(*Nobody can have SEEN keys that will be generated in the future.
   1.133 +  This has to be proved anew for each protocol description,
   1.134 +  but should go by similar reasoning every time.  Hardest case is the
   1.135 +  standard Fake rule.  
   1.136 +      The Union over C is essential for the induction! *)
   1.137 +goal thy "!!evs. evs : yahalom lost ==> \
   1.138 +\                length evs <= length evs' --> \
   1.139 +\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   1.140 +by (parts_induct_tac 1);
   1.141 +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.142 +                                           impOfSubs parts_insert_subset_Un,
   1.143 +                                           Suc_leD]
   1.144 +                                    addss (!simpset))));
   1.145 +val lemma = result();
   1.146 +
   1.147 +(*Variant needed for the main theorem below*)
   1.148 +goal thy 
   1.149 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   1.150 +\        ==> Key (newK evs') ~: parts (sees lost C evs)";
   1.151 +by (fast_tac (!claset addDs [lemma]) 1);
   1.152 +qed "new_keys_not_seen";
   1.153 +Addsimps [new_keys_not_seen];
   1.154 +
   1.155 +(*Another variant: old messages must contain old keys!*)
   1.156 +goal thy 
   1.157 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.158 +\           Key (newK evt) : parts {X};    \
   1.159 +\           evs : yahalom lost                 \
   1.160 +\        |] ==> length evt < length evs";
   1.161 +by (rtac ccontr 1);
   1.162 +by (dtac leI 1);
   1.163 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   1.164 +                      addIs  [impOfSubs parts_mono]) 1);
   1.165 +qed "Says_imp_old_keys";
   1.166 +
   1.167 +
   1.168 +(*Nobody can have USED keys that will be generated in the future.
   1.169 +  ...very like new_keys_not_seen*)
   1.170 +goal thy "!!evs. evs : yahalom lost ==> \
   1.171 +\                length evs <= length evs' --> \
   1.172 +\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   1.173 +by (parts_induct_tac 1);
   1.174 +by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
   1.175 +
   1.176 +(*YM1, YM2 and YM3*)
   1.177 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   1.178 +(*Fake and YM4: these messages send unknown (X) components*)
   1.179 +by (stac insert_commute 2);
   1.180 +by (Simp_tac 2);
   1.181 +(*YM4: the only way K could have been used is if it had been seen,
   1.182 +  contradicting new_keys_not_seen*)
   1.183 +by (REPEAT
   1.184 +     (best_tac
   1.185 +      (!claset addDs [impOfSubs analz_subset_parts,
   1.186 +                      impOfSubs (analz_subset_parts RS keysFor_mono),
   1.187 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.188 +                      Suc_leD]
   1.189 +               addEs [new_keys_not_seen RSN(2,rev_notE)]
   1.190 +               addss (!simpset)) 1));
   1.191 +val lemma = result();
   1.192 +
   1.193 +goal thy 
   1.194 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   1.195 +\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   1.196 +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.197 +qed "new_keys_not_used";
   1.198 +
   1.199 +bind_thm ("new_keys_not_analzd",
   1.200 +          [analz_subset_parts RS keysFor_mono,
   1.201 +           new_keys_not_used] MRS contra_subsetD);
   1.202 +
   1.203 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.204 +
   1.205 +
   1.206 +(*Describes the form of Key K when the following message is sent.  The use of
   1.207 +  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.208 +  assumption A ~: lost prevents its being a Faked message.  (Based
   1.209 +  on NS_Shared/Says_S_message_form) *)
   1.210 +goal thy
   1.211 + "!!evs. evs: yahalom lost ==>                                        \
   1.212 +\        Crypt {|B, Key K, NA|} (shrK A) : parts (sees lost Spy evs)  \
   1.213 +\        --> A ~: lost --> (EX evt: yahalom lost. K = newK evt)";
   1.214 +by (parts_induct_tac 1);
   1.215 +by (Auto_tac());
   1.216 +qed_spec_mp "Reveal_message_lemma";
   1.217 +
   1.218 +(*EITHER describes the form of Key K when the following message is sent, 
   1.219 +  OR     reduces it to the Fake case.*)
   1.220 +
   1.221 +goal thy 
   1.222 + "!!evs. [| Says S A {|NB, Crypt {|B, Key K, NA|} (shrK A), X|} \
   1.223 +\           : set_of_list evs;                                  \
   1.224 +\           evs : yahalom lost |]                               \
   1.225 +\        ==> (EX evt: yahalom lost. K = newK evt)               \
   1.226 +\          | Key K : analz (sees lost Spy evs)";
   1.227 +br (Reveal_message_lemma RS disjCI) 1;
   1.228 +ba 1;
   1.229 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.230 +                      addDs [impOfSubs analz_subset_parts]) 1);
   1.231 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.232 +                      addss (!simpset)) 1);
   1.233 +qed "Reveal_message_form";
   1.234 +
   1.235 +
   1.236 +(*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.237 +val analz_Fake_tac = 
   1.238 +    dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   1.239 +    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   1.240 +
   1.241 +
   1.242 +(****
   1.243 + The following is to prove theorems of the form
   1.244 +
   1.245 +          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   1.246 +          Key K : analz (sees lost Spy evs)
   1.247 +
   1.248 + A more general formula must be proved inductively.
   1.249 +
   1.250 +****)
   1.251 +
   1.252 +(** Session keys are not used to encrypt other session keys **)
   1.253 +
   1.254 +goal thy  
   1.255 + "!!evs. evs : yahalom lost ==> \
   1.256 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.257 +\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.258 +by (etac yahalom.induct 1);
   1.259 +by analz_Fake_tac;
   1.260 +by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   1.261 +by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 8));
   1.262 +by (ALLGOALS  (*Takes 26 secs*)
   1.263 +    (asm_simp_tac 
   1.264 +     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.265 +                         @ pushes)
   1.266 +               setloop split_tac [expand_if])));
   1.267 +(** LEVEL 5 **)
   1.268 +(*Reveal case 2, YM4, Fake*) 
   1.269 +by (EVERY (map spy_analz_tac [6, 4, 2]));
   1.270 +(*Reveal case 1, YM3, Base*)
   1.271 +by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.272 +qed_spec_mp "analz_image_newK";
   1.273 +
   1.274 +goal thy
   1.275 + "!!evs. evs : yahalom lost ==>                               \
   1.276 +\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   1.277 +\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   1.278 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.279 +                                   insert_Key_singleton]) 1);
   1.280 +by (Fast_tac 1);
   1.281 +qed "analz_insert_Key_newK";
   1.282 +
   1.283 +
   1.284 +(*** The Key K uniquely identifies the Server's  message. **)
   1.285 +
   1.286 +goal thy 
   1.287 + "!!evs. evs : yahalom lost ==>                                     \
   1.288 +\      EX A' B' NA' NB'. ALL A B NA NB.                             \
   1.289 +\          Says Server A                                            \
   1.290 +\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),            \
   1.291 +\                 Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}           \
   1.292 +\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB'";
   1.293 +by (etac yahalom.induct 1);
   1.294 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.295 +by (Step_tac 1);
   1.296 +(*Remaining case: YM3*)
   1.297 +by (expand_case_tac "K = ?y" 1);
   1.298 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.299 +(*...we assume X is a very new message, and handle this case by contradiction*)
   1.300 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.301 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.302 +                      addss (!simpset addsimps [parts_insertI])) 1);
   1.303 +val lemma = result();
   1.304 +
   1.305 +goal thy 
   1.306 +"!!evs. [| Says Server A                                            \
   1.307 +\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),            \
   1.308 +\                 Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}           \
   1.309 +\           : set_of_list evs;                                      \
   1.310 +\          Says Server A'                                           \
   1.311 +\           {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'),        \
   1.312 +\                  Crypt {|Agent A', Key K, NB', NB'|} (shrK B')|}       \
   1.313 +\           : set_of_list evs;                                      \
   1.314 +\          evs : yahalom lost |]                                    \
   1.315 +\       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.316 +by (dtac lemma 1);
   1.317 +by (REPEAT (etac exE 1));
   1.318 +(*Duplicate the assumption*)
   1.319 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.320 +by (fast_tac (!claset addSDs [spec]) 1);
   1.321 +qed "unique_session_keys";
   1.322 +
   1.323 +
   1.324 +(*If the encrypted message appears then it originated with the Server*)
   1.325 +goal thy
   1.326 + "!!evs. [| Crypt {|Agent B, Key K, Nonce NA|} (shrK A)                \
   1.327 +\            : parts (sees lost Spy evs);                              \
   1.328 +\           A ~: lost;  evs : yahalom lost |]                          \
   1.329 +\         ==> EX NB. Says Server A                                            \
   1.330 +\              {|NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),            \
   1.331 +\                    Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}           \
   1.332 +\             : set_of_list evs";
   1.333 +by (etac rev_mp 1);
   1.334 +by (parts_induct_tac 1);
   1.335 +by (Fast_tac 1);
   1.336 +qed "A_trust_YM3";
   1.337 +
   1.338 +
   1.339 +(*Describes the form of K when the Server sends this message.*)
   1.340 +goal thy 
   1.341 + "!!evs. [| Says Server A                                           \
   1.342 +\            {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   1.343 +\                  Crypt {|Agent A, K, NB, NB|} (shrK B)|}          \
   1.344 +\            : set_of_list evs;   \
   1.345 +\           evs : yahalom lost |]                                   \
   1.346 +\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   1.347 +by (etac rev_mp 1);
   1.348 +by (etac yahalom.induct 1);
   1.349 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.350 +qed "Says_Server_message_form";
   1.351 +
   1.352 +
   1.353 +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   1.354 +
   1.355 +goal thy 
   1.356 + "!!evs. [| A ~: lost;  B ~: lost;                                \
   1.357 +\           evs : yahalom lost;  evt : yahalom lost |]            \
   1.358 +\        ==> Says Server A                                           \
   1.359 +\              {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),           \
   1.360 +\                    Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}          \
   1.361 +\             : set_of_list evs -->                               \
   1.362 +\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->  \
   1.363 +\            Key K ~: analz (sees lost Spy evs)";
   1.364 +by (etac yahalom.induct 1);
   1.365 +by analz_Fake_tac;
   1.366 +by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.367 +by (ALLGOALS
   1.368 +    (asm_simp_tac 
   1.369 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.370 +                          analz_insert_Key_newK] @ pushes)
   1.371 +               setloop split_tac [expand_if])));
   1.372 +(*YM3*)
   1.373 +by (fast_tac (!claset addIs [parts_insertI]
   1.374 +                      addEs [Says_imp_old_keys RS less_irrefl]
   1.375 +                      addss (!simpset)) 2);
   1.376 +(*Reveal case 2, OR4, Fake*) 
   1.377 +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.378 +(*Reveal case 1*) (** LEVEL 6 **)
   1.379 +by (case_tac "Aa : lost" 1);
   1.380 +(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.381 +by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.382 +by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.383 +(*So now we have  Aa ~: lost *)
   1.384 +bd (Says_imp_sees_Spy RS parts.Inj) 1;
   1.385 +by (fast_tac (!claset delrules [disjE] 
   1.386 +	              addSEs [MPair_parts]
   1.387 +		      addDs [A_trust_YM3, unique_session_keys]
   1.388 +	              addss (!simpset)) 1);
   1.389 +val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.390 +
   1.391 +
   1.392 +(*Final version: Server's message in the most abstract form*)
   1.393 +goal thy 
   1.394 + "!!evs. [| Says Server A                                         \
   1.395 +\              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   1.396 +\                    Crypt {|Agent A, K, NB, NB|} (shrK B)|}      \
   1.397 +\           : set_of_list evs;                                    \
   1.398 +\           Says A Spy {|NA, K|} ~: set_of_list evs;          \
   1.399 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>     \
   1.400 +\     K ~: analz (sees lost Spy evs)";
   1.401 +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.402 +by (fast_tac (!claset addSEs [lemma]) 1);
   1.403 +qed "Spy_not_see_encrypted_key";
   1.404 +
   1.405 +
   1.406 +goal thy 
   1.407 + "!!evs. [| C ~: {A,B,Server};                                          \
   1.408 +\           Says Server A                                         \
   1.409 +\              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   1.410 +\                    Crypt {|Agent A, K, NB, NB|} (shrK B)|}          \
   1.411 +\           : set_of_list evs;                                    \
   1.412 +\           Says A Spy {|NA, K|} ~: set_of_list evs;                \
   1.413 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.414 +\     K ~: analz (sees lost C evs)";
   1.415 +by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.416 +by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.417 +by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.418 +by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
   1.419 +qed "Agent_not_see_encrypted_key";
   1.420 +
   1.421 +
   1.422 +(*** Security Guarantee for B upon receiving YM4 ***)
   1.423 +
   1.424 +(*B knows, by the first part of A's message, that the Server distributed 
   1.425 +  the key for A and B.  But this part says nothing about nonces.*)
   1.426 +goal thy 
   1.427 + "!!evs. [| Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)    \
   1.428 +\            : parts (sees lost Spy evs); \
   1.429 +\           B ~: lost;  evs : yahalom lost |]                           \
   1.430 +\        ==> EX NA. Says Server A                                    \
   1.431 +\                    {|Nonce NB,                                   \
   1.432 +\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
   1.433 +\                      Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)|}\
   1.434 +\                       : set_of_list evs";
   1.435 +by (etac rev_mp 1);
   1.436 +by (parts_induct_tac 1);
   1.437 +(*YM3*)
   1.438 +by (Fast_tac 1);
   1.439 +qed "B_trusts_YM4_shrK";
   1.440 +
   1.441 +(*With this variant we don't bother to use the 2nd part of YM4 at all, since
   1.442 +  Nonce NB is available in the first part.  However the 2nd part does assure B
   1.443 +  of A's existence.*)
   1.444 +
   1.445 +(*What can B deduce from receipt of YM4?  Note how the two components of
   1.446 +  the message contribute to a single conclusion about the Server's message.*)
   1.447 +goal thy 
   1.448 + "!!evs. [| Says A' B {|Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B),              \
   1.449 +\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   1.450 +\           ALL N N'. Says A Spy {|N,N', Key K|} ~: set_of_list evs;    \
   1.451 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   1.452 +\        ==> EX NA. Says Server A                                       \
   1.453 +\                    {|Nonce NB,                                   \
   1.454 +\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
   1.455 +\                      Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)|}\
   1.456 +\                   : set_of_list evs";
   1.457 +be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
   1.458 +by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
   1.459 +qed "B_trust_YM4";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Oct 18 11:43:14 1996 +0200
     2.3 @@ -0,0 +1,72 @@
     2.4 +(*  Title:      HOL/Auth/Yahalom
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
    2.10 +
    2.11 +This version trades encryption of NB for additional explicitness in YM3.
    2.12 +
    2.13 +From page 259 of
    2.14 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    2.15 +  Proc. Royal Soc. 426 (1989)
    2.16 +*)
    2.17 +
    2.18 +Yahalom2 = Shared + 
    2.19 +
    2.20 +consts  yahalom   :: "agent set => event list set"
    2.21 +inductive "yahalom lost"
    2.22 +  intrs 
    2.23 +         (*Initial trace is empty*)
    2.24 +    Nil  "[]: yahalom lost"
    2.25 +
    2.26 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    2.27 +           invent new nonces here, but he can also use NS1.  Common to
    2.28 +           all similar protocols.*)
    2.29 +    Fake "[| evs: yahalom lost;  B ~= Spy;  
    2.30 +             X: synth (analz (sees lost Spy evs)) |]
    2.31 +          ==> Says Spy B X  # evs : yahalom lost"
    2.32 +
    2.33 +         (*Alice initiates a protocol run*)
    2.34 +    YM1  "[| evs: yahalom lost;  A ~= B |]
    2.35 +          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
    2.36 +
    2.37 +         (*Bob's response to Alice's message.  Bob doesn't know who 
    2.38 +	   the sender is, hence the A' in the sender field.*)
    2.39 +    YM2  "[| evs: yahalom lost;  B ~= Server;
    2.40 +             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    2.41 +          ==> Says B Server 
    2.42 +                  {|Agent B, Nonce (newN evs), 
    2.43 +                    Crypt {|Agent A, Nonce NA|} (shrK B)|}
    2.44 +                 # evs : yahalom lost"
    2.45 +
    2.46 +         (*The Server receives Bob's message.  He responds by sending a
    2.47 +            new session key to Alice, with a packet for forwarding to Bob.*)
    2.48 +    YM3  "[| evs: yahalom lost;  A ~= Server;
    2.49 +             Says B' Server 
    2.50 +                  {|Agent B, Nonce NB, Crypt {|Agent A, Nonce NA|} (shrK B)|}
    2.51 +               : set_of_list evs |]
    2.52 +          ==> Says Server A
    2.53 +               {|Nonce NB, 
    2.54 +                 Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
    2.55 +                 Crypt {|Agent A, Key (newK evs), Nonce NB, Nonce NB|} (shrK B)|}
    2.56 +                 # evs : yahalom lost"
    2.57 +
    2.58 +         (*Alice receives the Server's (?) message, checks her Nonce, and
    2.59 +           uses the new session key to send Bob his Nonce.*)
    2.60 +    YM4  "[| evs: yahalom lost;  A ~= B;  
    2.61 +             Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    2.62 +                        X|}
    2.63 +               : set_of_list evs;
    2.64 +             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    2.65 +          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
    2.66 +
    2.67 +         (*This message models possible leaks of session keys.  The Nonce NA
    2.68 +           identifies the protocol run.  We can't be sure about NB.*)
    2.69 +    Revl "[| evs: yahalom lost;  A ~= Spy;
    2.70 +             Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    2.71 +                        X|}
    2.72 +               : set_of_list evs |]
    2.73 +          ==> Says A Spy {|Nonce NA, Key K|} # evs : yahalom lost"
    2.74 +
    2.75 +end