src/HOL/Auth/Yahalom.ML
author oheimb
Sat Feb 15 17:52:31 1997 +0100 (1997-02-15)
changeset 2637 e9b203f854ae
parent 2516 4d68fbe6378b
child 3121 cbb6c0c1c58a
permissions -rw-r--r--
reflecting my recent changes of the simplifier and classical reasoner
     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 "otway" 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 val op addss = op unsafe_addss;
    20 
    21 
    22 (*A "possibility property": there are traces that reach the end*)
    23 goal thy 
    24  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    25 \        ==> EX X NB K. EX evs: yahalom lost.          \
    26 \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    27 by (REPEAT (resolve_tac [exI,bexI] 1));
    28 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    29           yahalom.YM4) 2);
    30 by possibility_tac;
    31 result();
    32 
    33 
    34 (**** Inductive proofs about yahalom ****)
    35 
    36 (*Monotonicity*)
    37 goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    38 by (rtac subsetI 1);
    39 by (etac yahalom.induct 1);
    40 by (REPEAT_FIRST
    41     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    42                               :: yahalom.intrs))));
    43 qed "yahalom_mono";
    44 
    45 
    46 (*Nobody sends themselves messages*)
    47 goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    48 by (etac yahalom.induct 1);
    49 by (Auto_tac());
    50 qed_spec_mp "not_Says_to_self";
    51 Addsimps [not_Says_to_self];
    52 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    53 
    54 
    55 (** For reasoning about the encrypted portion of messages **)
    56 
    57 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    58 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    59 \                X : analz (sees lost Spy evs)";
    60 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    61 qed "YM4_analz_sees_Spy";
    62 
    63 bind_thm ("YM4_parts_sees_Spy",
    64           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    65 
    66 (*Relates to both YM4 and Oops*)
    67 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
    68 \                  : set_of_list evs ==> \
    69 \                K : parts (sees lost Spy evs)";
    70 by (fast_tac (!claset addSEs partsEs
    71                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    72 qed "YM4_Key_parts_sees_Spy";
    73 
    74 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    75   harder: the simplifier does less.*)
    76 val parts_Fake_tac = 
    77     forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
    78     forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
    79 
    80 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    81 fun parts_induct_tac i = SELECT_GOAL
    82     (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
    83              (*Fake message*)
    84              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    85                                            impOfSubs Fake_parts_insert]
    86                                     addss (!simpset)) 2)) THEN
    87      (*Base case*)
    88      fast_tac (!claset addss (!simpset)) 1 THEN
    89      ALLGOALS Asm_simp_tac) i;
    90 
    91 
    92 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    93     sends messages containing X! **)
    94 
    95 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    96 goal thy 
    97  "!!evs. evs : yahalom lost \
    98 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    99 by (parts_induct_tac 1);
   100 by (Auto_tac());
   101 qed "Spy_see_shrK";
   102 Addsimps [Spy_see_shrK];
   103 
   104 goal thy 
   105  "!!evs. evs : yahalom lost \
   106 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   107 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   108 qed "Spy_analz_shrK";
   109 Addsimps [Spy_analz_shrK];
   110 
   111 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   112 \                  evs : yahalom lost |] ==> A:lost";
   113 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   114 qed "Spy_see_shrK_D";
   115 
   116 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   117 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   118 
   119 
   120 (*Nobody can have used non-existent keys!*)
   121 goal thy "!!evs. evs : yahalom lost ==>          \
   122 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   123 by (parts_induct_tac 1);
   124 (*YM4: Key K is not fresh!*)
   125 by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
   126 (*YM3*)
   127 by (fast_tac (!claset addss (!simpset)) 2);
   128 (*Fake*)
   129 by (best_tac
   130       (!claset addIs [impOfSubs analz_subset_parts]
   131                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   132                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   133                addss (!simpset)) 1);
   134 qed_spec_mp "new_keys_not_used";
   135 
   136 bind_thm ("new_keys_not_analzd",
   137           [analz_subset_parts RS keysFor_mono,
   138            new_keys_not_used] MRS contra_subsetD);
   139 
   140 Addsimps [new_keys_not_used, new_keys_not_analzd];
   141 
   142 
   143 (*Describes the form of K when the Server sends this message.  Useful for
   144   Oops as well as main secrecy property.*)
   145 goal thy 
   146  "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
   147 \             : set_of_list evs;                                           \
   148 \           evs : yahalom lost |]                                          \
   149 \        ==> K ~: range shrK";
   150 by (etac rev_mp 1);
   151 by (etac yahalom.induct 1);
   152 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   153 qed "Says_Server_message_form";
   154 
   155 
   156 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   157 val analz_Fake_tac = 
   158     forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   159     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   160     assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   161 
   162 
   163 (****
   164  The following is to prove theorems of the form
   165 
   166   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   167   Key K : analz (sees lost Spy evs)
   168 
   169  A more general formula must be proved inductively.
   170 ****)
   171 
   172 (** Session keys are not used to encrypt other session keys **)
   173 
   174 goal thy  
   175  "!!evs. evs : yahalom lost ==> \
   176 \  ALL K KK. KK <= Compl (range shrK) -->                      \
   177 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   178 \            (K : KK | Key K : analz (sees lost Spy evs))";
   179 by (etac yahalom.induct 1);
   180 by analz_Fake_tac;
   181 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   182 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   183 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   184 (*Base*)
   185 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   186 (*YM4, Fake*) 
   187 by (REPEAT (spy_analz_tac 1));
   188 qed_spec_mp "analz_image_freshK";
   189 
   190 goal thy
   191  "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   192 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   193 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   194 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   195 qed "analz_insert_freshK";
   196 
   197 
   198 (*** The Key K uniquely identifies the Server's  message. **)
   199 
   200 goal thy 
   201  "!!evs. evs : yahalom lost ==>                                     \
   202 \      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
   203 \          Says Server A                                            \
   204 \           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
   205 \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   206 by (etac yahalom.induct 1);
   207 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   208 by (Step_tac 1);
   209 by (ex_strip_tac 2);
   210 by (Fast_tac 2);
   211 (*Remaining case: YM3*)
   212 by (expand_case_tac "K = ?y" 1);
   213 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   214 (*...we assume X is a recent message and handle this case by contradiction*)
   215 by (fast_tac (!claset addSEs sees_Spy_partsEs
   216                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   217                       addss (!simpset addsimps [parts_insertI])) 1);
   218 val lemma = result();
   219 
   220 goal thy 
   221 "!!evs. [| Says Server A                                            \
   222 \           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
   223 \           : set_of_list evs;                                      \
   224 \          Says Server A'                                           \
   225 \           {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|}   \
   226 \           : set_of_list evs;                                      \
   227 \          evs : yahalom lost |]                                    \
   228 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   229 by (prove_unique_tac lemma 1);
   230 qed "unique_session_keys";
   231 
   232 
   233 (*If the encrypted message appears then it originated with the Server*)
   234 goal thy
   235  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|}                  \
   236 \            : parts (sees lost Spy evs);                              \
   237 \           A ~: lost;  evs : yahalom lost |]                          \
   238 \         ==> Says Server A                                            \
   239 \              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},            \
   240 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   241 \             : set_of_list evs";
   242 by (etac rev_mp 1);
   243 by (parts_induct_tac 1);
   244 qed "A_trusts_YM3";
   245 
   246 
   247 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   248 
   249 goal thy 
   250  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   251 \        ==> Says Server A                                        \
   252 \              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   253 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   254 \             : set_of_list evs -->                               \
   255 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
   256 \            Key K ~: analz (sees lost Spy evs)";
   257 by (etac yahalom.induct 1);
   258 by analz_Fake_tac;
   259 by (ALLGOALS
   260     (asm_simp_tac 
   261      (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
   262                setloop split_tac [expand_if])));
   263 (*YM3*)
   264 by (fast_tac (!claset delrules [impCE]
   265                       addSEs sees_Spy_partsEs
   266                       addIs [impOfSubs analz_subset_parts]
   267                       addss (!simpset addsimps [parts_insert2])) 2);
   268 (*OR4, Fake*) 
   269 by (REPEAT_FIRST spy_analz_tac);
   270 (*Oops*)
   271 by (fast_tac (!claset delrules [disjE] 
   272                       addDs [unique_session_keys]
   273                       addss (!simpset)) 1);
   274 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   275 
   276 
   277 (*Final version: Server's message in the most abstract form*)
   278 goal thy 
   279  "!!evs. [| 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 Spy evs)";
   286 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   287 by (fast_tac (!claset addSEs [lemma]) 1);
   288 qed "Spy_not_see_encrypted_key";
   289 
   290 
   291 goal thy 
   292  "!!evs. [| C ~: {A,B,Server};                                    \
   293 \           Says Server A                                         \
   294 \              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   295 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   296 \             : set_of_list evs;                                  \
   297 \           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   298 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   299 \        ==> Key K ~: analz (sees lost C evs)";
   300 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   301 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   302 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   303 by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
   304 qed "Agent_not_see_encrypted_key";
   305 
   306 
   307 (*** Security Guarantee for B upon receiving YM4 ***)
   308 
   309 (*B knows, by the first part of A's message, that the Server distributed 
   310   the key for A and B.  But this part says nothing about nonces.*)
   311 goal thy 
   312  "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
   313 \           B ~: lost;  evs : yahalom lost |]                           \
   314 \        ==> EX NA NB. Says Server A                                    \
   315 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   316 \                                           Nonce NA, Nonce NB|},       \
   317 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   318 \                       : set_of_list evs";
   319 by (etac rev_mp 1);
   320 by (parts_induct_tac 1);
   321 (*YM3*)
   322 by (Fast_tac 1);
   323 qed "B_trusts_YM4_shrK";
   324 
   325 
   326 (** The Nonce NB uniquely identifies B's message. **)
   327 
   328 goal thy 
   329  "!!evs. evs : yahalom lost ==> \
   330 \   EX NA' A' B'. ALL NA A B. \
   331 \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
   332 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   333 by (etac yahalom.induct 1 THEN parts_Fake_tac);
   334 (*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
   335 by (REPEAT (etac exE 2) THEN 
   336     best_tac (!claset addSIs [exI]
   337                       addDs [impOfSubs Fake_parts_insert]
   338                       addss (!simpset)) 2);
   339 (*Base case*)
   340 by (fast_tac (!claset addss (!simpset)) 1);
   341 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
   342 (*YM2: creation of new Nonce.  Move assertion into global context*)
   343 by (expand_case_tac "NB = ?y" 1);
   344 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   345 by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
   346 val lemma = result();
   347 
   348 goal thy 
   349  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|} \
   350 \                  : parts (sees lost Spy evs);         \
   351 \          Crypt (shrK B') {|Agent A', Nonce NA', NB|} \
   352 \                  : parts (sees lost Spy evs);         \
   353 \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   354 \        ==> NA' = NA & A' = A & B' = B";
   355 by (prove_unique_tac lemma 1);
   356 qed "unique_NB";
   357 
   358 fun lost_tac s =
   359     case_tac ("(" ^ s ^ ") : lost") THEN'
   360     SELECT_GOAL 
   361       (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   362        REPEAT_DETERM (etac MPair_analz 1) THEN
   363        THEN_BEST_FIRST 
   364          (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   365          (has_fewer_prems 1, size_of_thm)
   366          (Step_tac 1));
   367 
   368 
   369 (*Variant useful for proving secrecy of NB*)
   370 goal thy 
   371  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
   372 \          : set_of_list evs;  B ~: lost;         \
   373 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   374 \          : set_of_list evs;                           \
   375 \          NB ~: analz (sees lost Spy evs);             \
   376 \          evs : yahalom lost |]  \
   377 \        ==> NA' = NA & A' = A & B' = B";
   378 by (lost_tac "B'" 1);
   379 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   380                       addSEs [MPair_parts]
   381                       addDs  [unique_NB]) 1);
   382 qed "Says_unique_NB";
   383 
   384 goal thy 
   385  "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
   386 \ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
   387 \      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
   388 \ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
   389 by (etac yahalom.induct 1);
   390 by parts_Fake_tac;
   391 by (REPEAT_FIRST 
   392     (rtac impI THEN' 
   393      dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   394      mp_tac));
   395 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   396                              impOfSubs Fake_parts_insert]
   397                       addss (!simpset)) 2);
   398 by (ALLGOALS Asm_simp_tac);
   399 by (fast_tac (!claset addss (!simpset)) 1);
   400 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   401                       addSIs [parts_insertI]
   402                       addSEs partsEs
   403                       addss (!simpset)) 1);
   404 val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
   405 
   406 
   407 
   408 (**** Towards proving secrecy of Nonce NB ****)
   409 
   410 (*B knows, by the second part of A's message, that the Server distributed 
   411   the key quoting nonce NB.  This part says nothing about agent names. 
   412   Secrecy of NB is crucial.*)
   413 goal thy 
   414  "!!evs. evs : yahalom lost                                             \
   415 \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   416 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   417 \            (EX A B NA. Says Server A                                  \
   418 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   419 \                                  Nonce NA, Nonce NB|},                \
   420 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   421 \                       : set_of_list evs)";
   422 by (etac yahalom.induct 1);
   423 by parts_Fake_tac;
   424 by (fast_tac (!claset addss (!simpset)) 1);
   425 by (REPEAT_FIRST
   426     (rtac impI THEN'
   427      dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   428 by (ALLGOALS Asm_simp_tac);
   429 (*Fake, YM3, YM4*)
   430 by (Fast_tac 2);
   431 by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   432                       addDs [impOfSubs analz_subset_parts]
   433                       addss (!simpset)) 1);
   434 (*YM4*)
   435 by (Step_tac 1);
   436 by (lost_tac "A" 1);
   437 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   438                              A_trusts_YM3]) 1);
   439 val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
   440 
   441 
   442 (*This is the original version of the result above.  But it is of little
   443   value because it assumes secrecy of K, which we cannot be assured of
   444   until we know that K is fresh -- which we do not know at the point this
   445   result is applied.*)
   446 goal thy 
   447  "!!evs. evs : yahalom lost                                             \
   448 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   449 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   450 \            (EX A B NA. Says Server A                                  \
   451 \                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   452 \                                  Nonce NA, Nonce NB|},       \
   453 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   454 \                       : set_of_list evs)";
   455 by (etac yahalom.induct 1);
   456 by parts_Fake_tac;
   457 by (fast_tac (!claset addss (!simpset)) 1);
   458 by (TRYALL (rtac impI));
   459 by (REPEAT_FIRST
   460     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   461 by (ALLGOALS Asm_simp_tac);
   462 (*Fake, YM3, YM4*)
   463 by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   464                       addDs  [impOfSubs analz_subset_parts]) 1);
   465 by (Fast_tac 1);
   466 (*YM4*)
   467 by (Step_tac 1);
   468 by (lost_tac "A" 1);
   469 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   470                              A_trusts_YM3]) 1);
   471 result() RS mp RSN (2, rev_mp);
   472 
   473 
   474 (*YM3 can only be triggered by YM2*)
   475 goal thy 
   476  "!!evs. [| Says Server A                                           \
   477 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
   478 \           evs : yahalom lost |]                                        \
   479 \        ==> EX B'. Says B' Server                                       \
   480 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   481 \                   : set_of_list evs";
   482 by (etac rev_mp 1);
   483 by (etac yahalom.induct 1);
   484 by (ALLGOALS Asm_simp_tac);
   485 by (ALLGOALS Fast_tac);
   486 qed "Says_Server_imp_YM2";
   487 
   488 
   489 (** Dedicated tactics for the nonce secrecy proofs **)
   490 
   491 val no_nonce_tac = SELECT_GOAL
   492    (REPEAT (resolve_tac [impI, notI] 1) THEN
   493     REPEAT (hyp_subst_tac 1) THEN
   494     etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
   495     THEN
   496     etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
   497     THEN 
   498     REPEAT_FIRST assume_tac);
   499 
   500 val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
   501 
   502 
   503 (*The only nonces that can be found with the help of session keys are
   504   those distributed as nonce NB by the Server.  The form of the theorem
   505   recalls analz_image_freshK, but it is much more complicated.*)
   506 
   507 (*As with analz_image_freshK, we take some pains to express the property
   508   as a logical equivalence so that the simplifier can apply it.*)
   509 goal thy  
   510  "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
   511 \        P --> (X : analz (G Un H)) = (X : analz H)";
   512 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   513 qed "Nonce_secrecy_lemma";
   514 
   515 goal thy 
   516  "!!evs. evs : yahalom lost ==>                                          \
   517 \        (ALL KK. KK <= Compl (range shrK) -->                               \
   518 \             (ALL K: KK. ALL A B na X.                                       \
   519 \                 Says Server A                                              \
   520 \                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   521 \                 ~: set_of_list evs)   -->  \
   522 \             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =      \
   523 \             (Nonce NB : analz (sees lost Spy evs)))";
   524 by (etac yahalom.induct 1);
   525 by analz_Fake_tac;
   526 by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   527 by (REPEAT_FIRST (rtac Nonce_secrecy_lemma ));
   528 by (rtac ccontr 7);
   529 by (subgoal_tac "ALL A B na X.                                       \
   530 \                 Says Server A                                              \
   531 \                     {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   532 \                 ~: set_of_list evsa" 7);
   533 by (eres_inst_tac [("P","?PP-->?QQ")] notE 7);
   534 by (subgoal_tac "ALL A B na X.                                       \
   535 \                 Says Server A                                              \
   536 \                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
   537 \                 ~: set_of_list evsa" 5);
   538 by (ALLGOALS  (*22 seconds*)
   539     (asm_simp_tac 
   540      (analz_image_freshK_ss  addsimps
   541              ([all_conj_distrib, 
   542                not_parts_not_analz, analz_image_freshK]
   543               @ pushes @ ball_simps))));
   544 (*Base*)
   545 by (fast_tac (!claset addss (!simpset)) 1);
   546 (*Fake*) (** LEVEL 10 **)
   547 by (spy_analz_tac 1);
   548 (*YM3*)
   549 by (fast_tac (!claset addSEs sees_Spy_partsEs) 1);
   550 (*Oops*)
   551 (*20 secs*)
   552 by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys]
   553                       addss (!simpset)) 2);
   554 (*YM4*)
   555 (** LEVEL 13 **)
   556 by (REPEAT (resolve_tac [impI, allI] 1));
   557 by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
   558 by (stac insert_commute 1);
   559 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   560 by (asm_simp_tac (analz_image_freshK_ss 
   561                   addsimps [analz_insertI, analz_image_freshK]) 1);
   562 by (step_tac (!claset addSDs [not_analz_insert]) 1);
   563 by (lost_tac "A" 1);
   564 (** LEVEL 20 **)
   565 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   566     THEN REPEAT (assume_tac 1));
   567 by (thin_tac "All ?PP" 1);
   568 by (Fast_tac 1);
   569 qed_spec_mp "Nonce_secrecy";
   570 
   571 
   572 (*Version required below: if NB can be decrypted using a session key then it
   573   was distributed with that key.  The more general form above is required
   574   for the induction to carry through.*)
   575 goal thy 
   576  "!!evs. [| Says Server A                                              \
   577 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
   578 \           : set_of_list evs;                                         \
   579 \           Nonce NB : analz (insert (Key KAB) (sees lost Spy evs));   \
   580 \           Nonce NB ~: analz (sees lost Spy evs);                     \
   581 \           KAB ~: range shrK;  evs : yahalom lost |]                  \
   582 \        ==>  NB = NB'";
   583 by (rtac ccontr 1);
   584 by (subgoal_tac "ALL A B na X.                                       \
   585 \                 Says Server A                                              \
   586 \                    {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \
   587 \                 ~: set_of_list evs" 1);
   588 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   589 by (asm_simp_tac (analz_image_freshK_ss 
   590                   addsimps ([Nonce_secrecy] @ ball_simps)) 1);
   591 by (auto_tac (!claset addDs [unique_session_keys], (!simpset)));
   592 qed "single_Nonce_secrecy";
   593 
   594 
   595 goal thy 
   596  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   597 \ ==> Says B Server                                                    \
   598 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   599 \     : set_of_list evs -->                               \
   600 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   601 \     Nonce NB ~: analz (sees lost Spy evs)";
   602 by (etac yahalom.induct 1);
   603 by analz_Fake_tac;
   604 by (ALLGOALS
   605     (asm_simp_tac 
   606      (!simpset addsimps ([not_parts_not_analz,
   607                           analz_insert_freshK] @ pushes)
   608                setloop split_tac [expand_if])));
   609 by (fast_tac (!claset addSIs [parts_insertI]
   610                       addSEs sees_Spy_partsEs
   611                       addss (!simpset)) 2);
   612 (*Proof of YM2*) (** LEVEL 4 **)
   613 by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj,
   614                                impOfSubs analz_subset_parts]
   615                         addSEs partsEs) 3 2);
   616 (*Prove YM3 by showing that no NB can also be an NA*)
   617 by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
   618 by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
   619 (*Fake*)
   620 by (spy_analz_tac 1);
   621 (*YM4*) (** LEVEL 8 **)
   622 by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   623 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   624 (*43 secs??*)
   625 by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
   626 by (lost_tac "Aa" 1);
   627 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   628 by (forward_tac [Says_Server_message_form] 3);
   629 by (forward_tac [Says_Server_imp_YM2] 4);
   630 (** LEVEL 15 **)
   631 by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   632 by (lost_tac "Ba" 1);
   633 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
   634 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   635                       addSEs [MPair_parts]) 1);
   636 by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
   637 (** LEVEL 20 **)
   638 by (dtac Spy_not_see_encrypted_key 1);
   639 by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   640 by (spy_analz_tac 1);
   641 (*Oops case*) (** LEVEL 23 **)
   642 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   643 by (step_tac (!claset delrules [disjE, conjI]) 1);
   644 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   645 by (expand_case_tac "NB = NBa" 1);
   646 by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   647 by (rtac conjI 1);
   648 by (no_nonce_tac 1);
   649 (** LEVEL 30 **)
   650 by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   651 by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
   652 val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
   653 
   654 
   655 (*What can B deduce from receipt of YM4?  Note how the two components of
   656   the message contribute to a single conclusion about the Server's message.
   657   It's annoying that the "Says A Spy" assumption must quantify over 
   658   ALL POSSIBLE keys instead of our particular K (though at least the
   659   nonces are forced to agree with NA and NB). *)
   660 goal thy 
   661  "!!evs. [| Says B Server                                               \
   662 \            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
   663 \           : set_of_list evs;       \
   664 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
   665 \                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   666 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   667 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
   668 \         ==> Says Server A                                             \
   669 \                     {|Crypt (shrK A) {|Agent B, Key K,                \
   670 \                               Nonce NA, Nonce NB|},                   \
   671 \                       Crypt (shrK B) {|Agent A, Key K|}|}             \
   672 \                   : set_of_list evs";
   673 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   674 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   675     dtac B_trusts_YM4_shrK 1);
   676 by (dtac B_trusts_YM4_newK 3);
   677 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   678 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   679 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   680 by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   681 qed "B_trusts_YM4";