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