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