src/HOL/Auth/Yahalom.ML
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3466 30791e5a69c4
child 3501 4ab477ffb4c6
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
     1 (*  Title:      HOL/Auth/Yahalom
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "yahalom" for the Yahalom protocol.
     7 
     8 From page 257 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 open Yahalom;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 Pretty.setdepth 25;
    18 
    19 (*Replacing the variable by a constant improves speed*)
    20 val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
    21 
    22 
    23 (*A "possibility property": there are traces that reach the end*)
    24 goal thy 
    25  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    26 \        ==> EX X NB K. EX evs: yahalom lost.     \
    27 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    28 by (REPEAT (resolve_tac [exI,bexI] 1));
    29 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    30           yahalom.YM4) 2);
    31 by possibility_tac;
    32 result();
    33 
    34 
    35 (**** Inductive proofs about yahalom ****)
    36 
    37 (*Monotonicity*)
    38 goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    39 by (rtac subsetI 1);
    40 by (etac yahalom.induct 1);
    41 by (REPEAT_FIRST
    42     (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    43                               :: yahalom.intrs))));
    44 qed "yahalom_mono";
    45 
    46 
    47 (*Nobody sends themselves messages*)
    48 goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
    49 by (etac yahalom.induct 1);
    50 by (Auto_tac());
    51 qed_spec_mp "not_Says_to_self";
    52 Addsimps [not_Says_to_self];
    53 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    54 
    55 
    56 (** For reasoning about the encrypted portion of messages **)
    57 
    58 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    59 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
    60 \                X : analz (sees lost Spy evs)";
    61 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    62 qed "YM4_analz_sees_Spy";
    63 
    64 bind_thm ("YM4_parts_sees_Spy",
    65           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    66 
    67 (*Relates to both YM4 and Oops*)
    68 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    69 \                K : parts (sees lost Spy evs)";
    70 by (blast_tac (!claset addSEs partsEs
    71                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
    72 qed "YM4_Key_parts_sees_Spy";
    73 
    74 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    75   We instantiate the variable to "lost" since leaving it as a Var would
    76   interfere with simplification.*)
    77 val parts_sees_tac = 
    78     forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
    79     forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
    80     prove_simple_subgoals_tac  1;
    81 
    82 val parts_induct_tac = 
    83     etac yahalom.induct 1 THEN parts_sees_tac;
    84 
    85 
    86 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    87     sends messages containing X! **)
    88 
    89 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    90 goal thy 
    91  "!!evs. evs : yahalom lost \
    92 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    93 by parts_induct_tac;
    94 by (Fake_parts_insert_tac 1);
    95 by (Blast_tac 1);
    96 qed "Spy_see_shrK";
    97 Addsimps [Spy_see_shrK];
    98 
    99 goal thy 
   100  "!!evs. evs : yahalom lost \
   101 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   102 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   103 qed "Spy_analz_shrK";
   104 Addsimps [Spy_analz_shrK];
   105 
   106 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   107 \                  evs : yahalom lost |] ==> A:lost";
   108 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   109 qed "Spy_see_shrK_D";
   110 
   111 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   112 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   113 
   114 
   115 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   116 goal thy "!!evs. evs : yahalom lost ==>          \
   117 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   118 by parts_induct_tac;
   119 (*YM4: Key K is not fresh!*)
   120 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   121 (*YM3*)
   122 by (Blast_tac 2);
   123 (*Fake*)
   124 by (best_tac
   125       (!claset addIs [impOfSubs analz_subset_parts]
   126                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   127                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   128                addss (!simpset)) 1);
   129 qed_spec_mp "new_keys_not_used";
   130 
   131 bind_thm ("new_keys_not_analzd",
   132           [analz_subset_parts RS keysFor_mono,
   133            new_keys_not_used] MRS contra_subsetD);
   134 
   135 Addsimps [new_keys_not_used, new_keys_not_analzd];
   136 
   137 
   138 (*Describes the form of K when the Server sends this message.  Useful for
   139   Oops as well as main secrecy property.*)
   140 goal thy 
   141  "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
   142 \             : set evs;                                                   \
   143 \           evs : yahalom lost |]                                          \
   144 \        ==> K ~: range shrK";
   145 by (etac rev_mp 1);
   146 by (etac yahalom.induct 1);
   147 by (ALLGOALS Asm_simp_tac);
   148 by (Blast_tac 1);
   149 qed "Says_Server_message_form";
   150 
   151 
   152 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   153 val analz_sees_tac = 
   154     forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   155     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   156     assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   157 
   158 
   159 (****
   160  The following is to prove theorems of the form
   161 
   162   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   163   Key K : analz (sees lost Spy evs)
   164 
   165  A more general formula must be proved inductively.
   166 ****)
   167 
   168 (** Session keys are not used to encrypt other session keys **)
   169 
   170 goal thy  
   171  "!!evs. evs : yahalom lost ==>                                 \
   172 \  ALL K KK. KK <= Compl (range shrK) -->                       \
   173 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   174 \            (K : KK | Key K : analz (sees lost Spy evs))";
   175 by (etac yahalom.induct 1);
   176 by analz_sees_tac;
   177 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   178 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   179 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   180 (*Fake*) 
   181 by (spy_analz_tac 2);
   182 (*Base*)
   183 by (Blast_tac 1);
   184 qed_spec_mp "analz_image_freshK";
   185 
   186 goal thy
   187  "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   188 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
   189 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   190 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   191 qed "analz_insert_freshK";
   192 
   193 
   194 (*** The Key K uniquely identifies the Server's  message. **)
   195 
   196 goal thy 
   197  "!!evs. evs : yahalom lost ==>                                     \
   198 \      EX A' B' na' nb' X'. ALL A B na nb X.                        \
   199 \          Says Server A                                            \
   200 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   201 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   202 by (etac yahalom.induct 1);
   203 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   204 by (Step_tac 1);
   205 by (ex_strip_tac 2);
   206 by (Blast_tac 2);
   207 (*Remaining case: YM3*)
   208 by (expand_case_tac "K = ?y" 1);
   209 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   210 (*...we assume X is a recent message and handle this case by contradiction*)
   211 by (blast_tac (!claset addSEs sees_Spy_partsEs
   212                       delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   213 val lemma = result();
   214 
   215 goal thy 
   216 "!!evs. [| Says Server A                                            \
   217 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   218 \           : set evs;                                              \
   219 \          Says Server A'                                           \
   220 \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   221 \           : set evs;                                              \
   222 \          evs : yahalom lost |]                                    \
   223 \       ==> A=A' & B=B' & na=na' & nb=nb'";
   224 by (prove_unique_tac lemma 1);
   225 qed "unique_session_keys";
   226 
   227 
   228 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   229 
   230 goal thy 
   231  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   232 \        ==> Says Server A                                        \
   233 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   234 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   235 \             : set evs -->                                       \
   236 \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
   237 \            Key K ~: analz (sees lost Spy evs)";
   238 by (etac yahalom.induct 1);
   239 by analz_sees_tac;
   240 by (ALLGOALS
   241     (asm_simp_tac 
   242      (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
   243 			 analz_insert_freshK]
   244                setloop split_tac [expand_if])));
   245 (*Oops*)
   246 by (blast_tac (!claset addDs [unique_session_keys]) 3);
   247 (*YM3*)
   248 by (blast_tac (!claset delrules [impCE]
   249                        addSEs sees_Spy_partsEs
   250                        addIs [impOfSubs analz_subset_parts]) 2);
   251 (*Fake*) 
   252 by (spy_analz_tac 1);
   253 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   254 
   255 
   256 (*Final version*)
   257 goal thy 
   258  "!!evs. [| Says Server A                                         \
   259 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   260 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   261 \             : set evs;                                          \
   262 \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   263 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   264 \        ==> Key K ~: analz (sees lost Spy evs)";
   265 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   266 by (blast_tac (!claset addSEs [lemma]) 1);
   267 qed "Spy_not_see_encrypted_key";
   268 
   269 
   270 (*And other agents don't see the key either.*)
   271 goal thy 
   272  "!!evs. [| C ~: {A,B,Server};                                    \
   273 \           Says Server A                                         \
   274 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   275 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   276 \             : set evs;                                          \
   277 \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   278 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   279 \        ==> Key K ~: analz (sees lost C evs)";
   280 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   281 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   282 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   283 by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
   284 qed "Agent_not_see_encrypted_key";
   285 
   286 
   287 (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   288   It simplifies the proof by discarding needless information about
   289 	analz (insert X (sees lost Spy evs)) 
   290 *)
   291 val analz_mono_parts_induct_tac = 
   292     etac yahalom.induct 1 
   293     THEN 
   294     REPEAT_FIRST  
   295       (rtac impI THEN' 
   296        dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   297        mp_tac)  
   298     THEN  parts_sees_tac;
   299 
   300 
   301 (** Security Guarantee for A upon receiving YM3 **)
   302 
   303 (*If the encrypted message appears then it originated with the Server*)
   304 goal thy
   305  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
   306 \            : parts (sees lost Spy evs);                              \
   307 \           A ~: lost;  evs : yahalom lost |]                          \
   308 \         ==> Says Server A                                            \
   309 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   310 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   311 \             : set evs";
   312 by (etac rev_mp 1);
   313 by parts_induct_tac;
   314 by (Fake_parts_insert_tac 1);
   315 qed "A_trusts_YM3";
   316 
   317 
   318 (** Security Guarantees for B upon receiving YM4 **)
   319 
   320 (*B knows, by the first part of A's message, that the Server distributed 
   321   the key for A and B.  But this part says nothing about nonces.*)
   322 goal thy 
   323  "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
   324 \           B ~: lost;  evs : yahalom lost |]                           \
   325 \        ==> EX NA NB. Says Server A                                    \
   326 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   327 \                                           Nonce NA, Nonce NB|},       \
   328 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   329 \                       : set evs";
   330 by (etac rev_mp 1);
   331 by parts_induct_tac;
   332 by (Fake_parts_insert_tac 1);
   333 (*YM3*)
   334 by (Blast_tac 1);
   335 qed "B_trusts_YM4_shrK";
   336 
   337 (*B knows, by the second part of A's message, that the Server distributed 
   338   the key quoting nonce NB.  This part says nothing about agent names. 
   339   Secrecy of NB is crucial.*)
   340 goal thy 
   341  "!!evs. evs : yahalom lost                                             \
   342 \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   343 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   344 \            (EX A B NA. Says Server A                                  \
   345 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   346 \                                  Nonce NA, Nonce NB|},                \
   347 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   348 \                       : set evs)";
   349 by analz_mono_parts_induct_tac;
   350 (*YM3 & Fake*)
   351 by (Blast_tac 2);
   352 by (Fake_parts_insert_tac 1);
   353 (*YM4*)
   354 by (Step_tac 1);
   355 (*A is uncompromised because NB is secure*)
   356 by (not_lost_tac "A" 1);
   357 (*A's certificate guarantees the existence of the Server message*)
   358 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
   359 			      A_trusts_YM3]) 1);
   360 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   361 
   362 
   363 (**** Towards proving secrecy of Nonce NB ****)
   364 
   365 (** Lemmas about the predicate KeyWithNonce **)
   366 
   367 goalw thy [KeyWithNonce_def]
   368  "!!evs. Says Server A                                              \
   369 \            {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   370 \          : set evs ==> KeyWithNonce K NB evs";
   371 by (Blast_tac 1);
   372 qed "KeyWithNonceI";
   373 
   374 goalw thy [KeyWithNonce_def]
   375    "KeyWithNonce K NB (Says S A X # evs) =                                    \
   376 \    (Server = S &                                                            \
   377 \     (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \
   378 \    | KeyWithNonce K NB evs)";
   379 by (Simp_tac 1);
   380 by (Blast_tac 1);
   381 qed "KeyWithNonce_Says";
   382 Addsimps [KeyWithNonce_Says];
   383 
   384 (*A fresh key cannot be associated with any nonce 
   385   (with respect to a given trace). *)
   386 goalw thy [KeyWithNonce_def]
   387  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   388 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   389 qed "fresh_not_KeyWithNonce";
   390 
   391 (*The Server message associates K with NB' and therefore not with any 
   392   other nonce NB.*)
   393 goalw thy [KeyWithNonce_def]
   394  "!!evs. [| Says Server A                                                \
   395 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
   396 \             : set evs;                                                 \
   397 \           NB ~= NB';  evs : yahalom lost |]                            \
   398 \        ==> ~ KeyWithNonce K NB evs";
   399 by (blast_tac (!claset addDs [unique_session_keys]) 1);
   400 qed "Says_Server_KeyWithNonce";
   401 
   402 
   403 (*The only nonces that can be found with the help of session keys are
   404   those distributed as nonce NB by the Server.  The form of the theorem
   405   recalls analz_image_freshK, but it is much more complicated.*)
   406 
   407 
   408 (*As with analz_image_freshK, we take some pains to express the property
   409   as a logical equivalence so that the simplifier can apply it.*)
   410 goal thy  
   411  "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
   412 \        P --> (X : analz (G Un H)) = (X : analz H)";
   413 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   414 val lemma = result();
   415 
   416 goal thy 
   417  "!!evs. evs : yahalom lost ==>                                         \
   418 \        (ALL KK. KK <= Compl (range shrK) -->                          \
   419 \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
   420 \             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =     \
   421 \             (Nonce NB : analz (sees lost Spy evs)))";
   422 by (etac yahalom.induct 1);
   423 by analz_sees_tac;
   424 by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   425 by (REPEAT_FIRST (rtac lemma));
   426 (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   427   we get (~ KeyWithNonce K NB evsa); then simplification can apply the
   428   induction hypothesis with KK = {K}.*)
   429 by (ALLGOALS  (*22 seconds*)
   430     (asm_simp_tac 
   431      (analz_image_freshK_ss addsimps
   432         ([all_conj_distrib, not_parts_not_analz, analz_image_freshK,
   433 	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
   434 	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
   435 	  Says_Server_KeyWithNonce] 
   436 	 @ pushes))));
   437 (*Base*)
   438 by (Blast_tac 1);
   439 (*Fake*) 
   440 by (spy_analz_tac 1);
   441 (*YM4*)  (** LEVEL 7 **)
   442 by (not_lost_tac "A" 1);
   443 by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   444     THEN REPEAT (assume_tac 1));
   445 by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   446 qed_spec_mp "Nonce_secrecy";
   447 
   448 
   449 (*Version required below: if NB can be decrypted using a session key then it
   450   was distributed with that key.  The more general form above is required
   451   for the induction to carry through.*)
   452 goal thy 
   453  "!!evs. [| Says Server A                                                 \
   454 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   455 \           : set evs;                                                    \
   456 \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
   457 \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
   458 \            (Nonce NB : analz (sees lost Spy evs))";
   459 by (asm_simp_tac (analz_image_freshK_ss addsimps 
   460 		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   461 qed "single_Nonce_secrecy";
   462 
   463 
   464 (*** The Nonce NB uniquely identifies B's message. ***)
   465 
   466 goal thy 
   467  "!!evs. evs : yahalom lost ==>                                            \
   468 \   EX NA' A' B'. ALL NA A B.                                              \
   469 \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
   470 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   471 by parts_induct_tac;
   472 (*Fake*)
   473 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   474     THEN Fake_parts_insert_tac 1);
   475 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   476 (*YM2: creation of new Nonce.  Move assertion into global context*)
   477 by (expand_case_tac "NB = ?y" 1);
   478 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   479 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   480 val lemma = result();
   481 
   482 goal thy 
   483  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|}        \
   484 \                  : parts (sees lost Spy evs);            \
   485 \          Crypt (shrK B') {|Agent A', Nonce NA', NB|}     \
   486 \                  : parts (sees lost Spy evs);            \
   487 \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   488 \        ==> NA' = NA & A' = A & B' = B";
   489 by (prove_unique_tac lemma 1);
   490 qed "unique_NB";
   491 
   492 
   493 (*Variant useful for proving secrecy of NB: the Says... form allows 
   494   not_lost_tac to remove the assumption B' ~: lost.*)
   495 goal thy 
   496  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
   497 \            : set evs;          B ~: lost;                               \
   498 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   499 \            : set evs;                                                   \
   500 \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
   501 \        ==> NA' = NA & A' = A & B' = B";
   502 by (not_lost_tac "B'" 1);
   503 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   504                        addSEs [MPair_parts]
   505                        addDs  [unique_NB]) 1);
   506 qed "Says_unique_NB";
   507 
   508 val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
   509 
   510 
   511 (** A nonce value is never used both as NA and as NB **)
   512 
   513 goal thy 
   514  "!!evs. [| B ~: lost;  evs : yahalom lost  |]       \
   515 \ ==> Nonce NB ~: analz (sees lost Spy evs) -->      \
   516 \     Crypt (shrK B') {|Agent A', Nonce NB, NB'|}    \
   517 \       : parts(sees lost Spy evs)                   \
   518 \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
   519 \       ~: parts(sees lost Spy evs)";
   520 by analz_mono_parts_induct_tac;
   521 by (Fake_parts_insert_tac 1);
   522 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
   523                        addSIs [parts_insertI]
   524                        addSEs partsEs) 1);
   525 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   526 
   527 (*The Server sends YM3 only in response to YM2.*)
   528 goal thy 
   529  "!!evs. [| Says Server A                                                \
   530 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   531 \           evs : yahalom lost |]                                        \
   532 \        ==> EX B'. Says B' Server                                       \
   533 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   534 \                   : set evs";
   535 by (etac rev_mp 1);
   536 by (etac yahalom.induct 1);
   537 by (ALLGOALS Asm_simp_tac);
   538 by (ALLGOALS Blast_tac);
   539 qed "Says_Server_imp_YM2";
   540 
   541 
   542 (*A vital theorem for B, that nonce NB remains secure from the Spy.
   543   Unusually, the Fake case requires Spy:lost.*)
   544 goal thy 
   545  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   546 \ ==> Says B Server                                                    \
   547 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   548 \     : set evs -->                                                    \
   549 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   550 \     Nonce NB ~: analz (sees lost Spy evs)";
   551 by (etac yahalom.induct 1);
   552 by analz_sees_tac;
   553 by (ALLGOALS
   554     (asm_simp_tac 
   555      (!simpset addsimps ([analz_insert_eq, not_parts_not_analz,
   556                           analz_insert_freshK] @ pushes)
   557                setloop split_tac [expand_if])));
   558 (*Prove YM3 by showing that no NB can also be an NA*)
   559 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   560 	               addSEs [MPair_parts]
   561 		       addDs  [no_nonce_YM1_YM2, Says_unique_NB']) 4
   562     THEN flexflex_tac);
   563 (*YM2: similar freshness reasoning*) 
   564 by (blast_tac (!claset addSEs partsEs
   565 		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
   566 			       impOfSubs analz_subset_parts]) 3);
   567 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   568 by (blast_tac (!claset addSIs [parts_insertI]
   569                        addSEs sees_Spy_partsEs) 2);
   570 (*Fake*)
   571 by (spy_analz_tac 1);
   572 (** LEVEL 7: YM4 and Oops remain **)
   573 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   574 by (REPEAT (Safe_step_tac 1));
   575 by (not_lost_tac "Aa" 1);
   576 by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   577 by (forward_tac [Says_Server_message_form] 3);
   578 by (forward_tac [Says_Server_imp_YM2] 4);
   579 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   580 (*  use Says_unique_NB' to identify message components: Aa=A, Ba=B, NAa=NA *)
   581 by (blast_tac (!claset addDs [Says_unique_NB', Spy_not_see_encrypted_key,
   582 			      impOfSubs Fake_analz_insert]) 1);
   583 (** LEVEL 14 **)
   584 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   585   covered by the quantified Oops assumption.*)
   586 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   587 by (step_tac (!claset delrules [disjE, conjI]) 1);
   588 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   589 by (expand_case_tac "NB = NBa" 1);
   590 (*If NB=NBa then all other components of the Oops message agree*)
   591 by (blast_tac (!claset addDs [Says_unique_NB']) 1 THEN flexflex_tac);
   592 (*case NB ~= NBa*)
   593 by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   594 by (blast_tac (!claset addSEs [MPair_parts]
   595 		       addDs  [Says_imp_sees_Spy' RS parts.Inj, 
   596 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   597 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   598 
   599 
   600 (*B's session key guarantee from YM4.  The two certificates contribute to a
   601   single conclusion about the Server's message.  Note that the "Says A Spy"
   602   assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   603   If this run is broken and the spy substitutes a certificate containing an
   604   old key, B has no means of telling.*)
   605 goal thy 
   606  "!!evs. [| Says B Server                                                   \
   607 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   608 \             : set evs;                                                    \
   609 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   610 \                       Crypt K (Nonce NB)|} : set evs;                     \
   611 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   612 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   613 \         ==> Says Server A                                                 \
   614 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   615 \                               Nonce NA, Nonce NB|},                       \
   616 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   617 \               : set evs";
   618 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   619 by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
   620     dtac B_trusts_YM4_shrK 1);
   621 by (dtac B_trusts_YM4_newK 3);
   622 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   623 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   624 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   625 by (blast_tac (!claset addDs [Says_unique_NB']) 1);
   626 qed "B_trusts_YM4";
   627 
   628 
   629 
   630 (*** Authenticating B to A ***)
   631 
   632 (*The encryption in message YM2 tells us it cannot be faked.*)
   633 goal thy 
   634  "!!evs. evs : yahalom lost                                            \
   635 \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
   636 \        : parts (sees lost Spy evs) -->                               \
   637 \      B ~: lost -->                                                   \
   638 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   639 \         : set evs";
   640 by parts_induct_tac;
   641 by (Fake_parts_insert_tac 1);
   642 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   643 
   644 (*If the server sends YM3 then B sent YM2*)
   645 goal thy 
   646  "!!evs. evs : yahalom lost                                                 \
   647 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   648 \         : set evs -->                                                     \
   649 \      B ~: lost -->                                                        \
   650 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   651 \                 : set evs";
   652 by (etac yahalom.induct 1);
   653 by (ALLGOALS Asm_simp_tac);
   654 (*YM4*)
   655 by (Blast_tac 2);
   656 (*YM3*)
   657 by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy' RS parts.Inj]
   658 		      addSEs [MPair_parts]) 1);
   659 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   660 
   661 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   662 goal thy
   663  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   664 \             : set evs;                                                    \
   665 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   666 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   667 \         : set evs";
   668 by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   669 		       addEs sees_Spy_partsEs) 1);
   670 qed "YM3_auth_B_to_A";
   671 
   672 
   673 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   674 
   675 (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   676   It simplifies the proof by discarding needless information about
   677 	analz (insert X (sees lost Spy evs)) 
   678 *)
   679 val analz_mono_parts_induct_tac = 
   680     etac yahalom.induct 1 
   681     THEN 
   682     REPEAT_FIRST  
   683       (rtac impI THEN' 
   684        dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   685        mp_tac)  
   686     THEN  parts_sees_tac;
   687 
   688 (*Assuming the session key is secure, if both certificates are present then
   689   A has said NB.  We can't be sure about the rest of A's message, but only
   690   NB matters for freshness.*)  
   691 goal thy 
   692  "!!evs. evs : yahalom lost                                             \
   693 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   694 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   695 \            Crypt (shrK B) {|Agent A, Key K|}                          \
   696 \              : parts (sees lost Spy evs) -->                          \
   697 \            B ~: lost -->                                              \
   698 \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   699 by analz_mono_parts_induct_tac;
   700 (*Fake*)
   701 by (Fake_parts_insert_tac 1);
   702 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   703 by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   704 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   705 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   706 (*yes: apply unicity of session keys*)
   707 by (not_lost_tac "Aa" 1);
   708 by (blast_tac (!claset addSEs [MPair_parts]
   709                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   710 		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   711 			       unique_session_keys]) 1);
   712 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   713 
   714 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   715   Moreover, A associates K with NB (thus is talking about the same run).
   716   Other premises guarantee secrecy of K.*)
   717 goal thy 
   718  "!!evs. [| Says B Server                                                   \
   719 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   720 \             : set evs;                                                    \
   721 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   722 \                       Crypt K (Nonce NB)|} : set evs;                     \
   723 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   724 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   725 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   726 by (dtac B_trusts_YM4 1);
   727 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   728 by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   729 by (rtac lemma 1);
   730 by (rtac Spy_not_see_encrypted_key 2);
   731 by (REPEAT_FIRST assume_tac);
   732 by (blast_tac (!claset addSEs [MPair_parts]
   733 	       	       addDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   734 qed_spec_mp "YM4_imp_A_Said_YM3";