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