src/HOL/Auth/Recur.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Auth/Recur
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "recur" for the Recursive Authentication protocol.
     7 *)
     8 
     9 open Recur;
    10 
    11 proof_timing:=true;
    12 HOL_quantifiers := false;
    13 Pretty.setdepth 30;
    14 
    15 
    16 (** Possibility properties: traces that reach the end 
    17         ONE theorem would be more elegant and faster!
    18         By induction on a list of agents (no repetitions)
    19 **)
    20 
    21 
    22 (*Simplest case: Alice goes directly to the server*)
    23 goal thy
    24  "!!A. A ~= Server   \
    25 \ ==> EX K NA. EX evs: recur lost.          \
    26 \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
    27 \                     Agent Server|}      \
    28 \         : set_of_list evs";
    29 by (REPEAT (resolve_tac [exI,bexI] 1));
    30 by (rtac (recur.Nil RS recur.RA1 RS 
    31           (respond.One RSN (4,recur.RA3))) 2);
    32 by possibility_tac;
    33 result();
    34 
    35 
    36 (*Case two: Alice, Bob and the server*)
    37 goal thy
    38  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    39 \ ==> EX K. EX NA. EX evs: recur lost.            \
    40 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    41 \                  Agent Server|}                               \
    42 \         : set_of_list evs";
    43 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
    44 by (REPEAT (eresolve_tac [exE, conjE] 1));
    45 by (REPEAT (resolve_tac [exI,bexI] 1));
    46 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
    47           (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
    48           recur.RA4) 2);
    49 by basic_possibility_tac;
    50 by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
    51 			       less_not_refl2 RS not_sym] 1));
    52 result();
    53 
    54 
    55 (*Case three: Alice, Bob, Charlie and the server
    56   TOO SLOW to run every time!
    57 goal thy
    58  "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
    59 \ ==> EX K. EX NA. EX evs: recur lost.                          \
    60 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    61 \                  Agent Server|}                               \
    62 \         : set_of_list evs";
    63 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
    64 by (REPEAT (eresolve_tac [exE, conjE] 1));
    65 by (REPEAT (resolve_tac [exI,bexI] 1));
    66 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
    67           (respond.One RS respond.Cons RS respond.Cons RSN
    68            (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
    69 (*SLOW: 70 seconds*)
    70 by basic_possibility_tac;
    71 by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
    72 		 ORELSE
    73 		 eresolve_tac [asm_rl, less_not_refl2, 
    74 			       less_not_refl2 RS not_sym] 1));
    75 result();
    76 ****************)
    77 
    78 (**** Inductive proofs about recur ****)
    79 
    80 (*Monotonicity*)
    81 goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost";
    82 by (rtac subsetI 1);
    83 by (etac recur.induct 1);
    84 by (REPEAT_FIRST
    85     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    86                               :: recur.intrs))));
    87 qed "recur_mono";
    88 
    89 (*Nobody sends themselves messages*)
    90 goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set_of_list evs";
    91 by (etac recur.induct 1);
    92 by (Auto_tac());
    93 qed_spec_mp "not_Says_to_self";
    94 Addsimps [not_Says_to_self];
    95 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    96 
    97 
    98 
    99 goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
   100 by (etac respond.induct 1);
   101 by (ALLGOALS Simp_tac);
   102 qed "respond_Key_in_parts";
   103 
   104 goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
   105 by (etac respond.induct 1);
   106 by (REPEAT (assume_tac 1));
   107 qed "respond_imp_not_used";
   108 
   109 goal thy
   110  "!!evs. [| Key K : parts {RB};  (PB,RB,K') : respond evs |] \
   111 \        ==> Key K ~: used evs";
   112 by (etac rev_mp 1);
   113 by (etac respond.induct 1);
   114 by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
   115              !simpset));
   116 qed_spec_mp "Key_in_parts_respond";
   117 
   118 (*Simple inductive reasoning about responses*)
   119 goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
   120 by (etac respond.induct 1);
   121 by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
   122 qed "respond_imp_responses";
   123 
   124 
   125 (** For reasoning about the encrypted portion of messages **)
   126 
   127 val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
   128 
   129 goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \
   130 \                ==> RA : analz (sees lost Spy evs)";
   131 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   132 qed "RA4_analz_sees_Spy";
   133 
   134 (*RA2_analz... and RA4_analz... let us treat those cases using the same 
   135   argument as for the Fake case.  This is possible for most, but not all,
   136   proofs: Fake does not invent new nonces (as in RA2), and of course Fake
   137   messages originate from the Spy. *)
   138 
   139 bind_thm ("RA2_parts_sees_Spy",
   140           RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   141 bind_thm ("RA4_parts_sees_Spy",
   142           RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   143 
   144 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   145   harder to complete, since simplification does less for us.*)
   146 val parts_Fake_tac = 
   147     let val tac = forw_inst_tac [("lost","lost")] 
   148     in  tac RA2_parts_sees_Spy 4              THEN
   149         etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
   150         forward_tac [respond_imp_responses] 5 THEN
   151         tac RA4_parts_sees_Spy 6
   152     end;
   153 
   154 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
   155 fun parts_induct_tac i = SELECT_GOAL
   156     (DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN
   157              (*Fake message*)
   158              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   159                                            impOfSubs Fake_parts_insert]
   160                             unsafe_addss (!simpset)) 2)) THEN
   161      (*Base case*)
   162      fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
   163      ALLGOALS Asm_simp_tac) i;
   164 
   165 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   166     sends messages containing X! **)
   167 
   168 
   169 (** Spy never sees another agent's long-term key (unless initially lost) **)
   170 
   171 goal thy 
   172  "!!evs. evs : recur lost \
   173 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   174 by (parts_induct_tac 1);
   175 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   176 (*RA3*)
   177 by (fast_tac (!claset addDs [Key_in_parts_respond]
   178                       addss (!simpset addsimps [parts_insert_sees])) 2);
   179 (*RA2*)
   180 by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
   181                       unsafe_addss (!simpset)) 1);
   182 qed "Spy_see_shrK";
   183 Addsimps [Spy_see_shrK];
   184 
   185 goal thy 
   186  "!!evs. evs : recur lost \
   187 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   188 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   189 qed "Spy_analz_shrK";
   190 Addsimps [Spy_analz_shrK];
   191 
   192 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   193 \                  evs : recur lost |] ==> A:lost";
   194 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   195 qed "Spy_see_shrK_D";
   196 
   197 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   198 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   199 
   200 
   201 
   202 (** Nobody can have used non-existent keys! **)
   203 
   204 goal thy
   205  "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
   206 \        ==> K : range shrK";
   207 by (etac rev_mp 1);
   208 by (etac (respond_imp_responses RS responses.induct) 1);
   209 by (Auto_tac());
   210 qed_spec_mp "Key_in_keysFor_parts";
   211 
   212 
   213 goal thy "!!evs. evs : recur lost ==>          \
   214 \       Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   215 by (parts_induct_tac 1);
   216 (*RA3*)
   217 by (best_tac (!claset addDs  [Key_in_keysFor_parts]
   218                       unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
   219 (*Fake*)
   220 by (best_tac
   221       (!claset addIs [impOfSubs analz_subset_parts]
   222                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   223                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   224                unsafe_addss (!simpset)) 1);
   225 qed_spec_mp "new_keys_not_used";
   226 
   227 
   228 bind_thm ("new_keys_not_analzd",
   229           [analz_subset_parts RS keysFor_mono,
   230            new_keys_not_used] MRS contra_subsetD);
   231 
   232 Addsimps [new_keys_not_used, new_keys_not_analzd];
   233 
   234 
   235 
   236 (*** Proofs involving analz ***)
   237 
   238 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   239 val analz_Fake_tac = 
   240     etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
   241     dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
   242     forward_tac [respond_imp_responses] 5                THEN
   243     dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
   244 
   245 
   246 (** Session keys are not used to encrypt other session keys **)
   247 
   248 (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
   249   Note that it holds for *any* set H (not just "sees lost Spy evs")
   250   satisfying the inductive hypothesis.*)
   251 goal thy  
   252  "!!evs. [| RB : responses evs;                             \
   253 \           ALL K KK. KK <= Compl (range shrK) -->          \
   254 \                     (Key K : analz (Key``KK Un H)) =      \
   255 \                     (K : KK | Key K : analz H) |]         \
   256 \       ==> ALL K KK. KK <= Compl (range shrK) -->          \
   257 \                     (Key K : analz (insert RB (Key``KK Un H))) = \
   258 \                     (K : KK | Key K : analz (insert RB H))";
   259 by (etac responses.induct 1);
   260 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   261 qed "resp_analz_image_freshK_lemma";
   262 
   263 (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
   264 goal thy  
   265  "!!evs. evs : recur lost ==>                                   \
   266 \  ALL K KK. KK <= Compl (range shrK) -->                       \
   267 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   268 \            (K : KK | Key K : analz (sees lost Spy evs))";
   269 by (etac recur.induct 1);
   270 by analz_Fake_tac;
   271 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   272 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   273 by (ALLGOALS 
   274     (asm_simp_tac
   275      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
   276 (*Base*)
   277 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   278 (*RA4, RA2, Fake*) 
   279 by (REPEAT (spy_analz_tac 1));
   280 val raw_analz_image_freshK = result();
   281 qed_spec_mp "analz_image_freshK";
   282 
   283 
   284 (*Instance of the lemma with H replaced by (sees lost Spy evs):
   285    [| RB : responses evs;  evs : recur lost; |]
   286    ==> KK <= Compl (range shrK) --> 
   287        Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
   288        (K : KK | Key K : analz (insert RB (sees lost Spy evs))) 
   289 *)
   290 bind_thm ("resp_analz_image_freshK",
   291           raw_analz_image_freshK RSN
   292             (2, resp_analz_image_freshK_lemma) RS spec RS spec);
   293 
   294 goal thy
   295  "!!evs. [| evs : recur lost;  KAB ~: range shrK |] ==>              \
   296 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =      \
   297 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   298 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   299 qed "analz_insert_freshK";
   300 
   301 
   302 (*Everything that's hashed is already in past traffic. *)
   303 goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees lost Spy evs);  \
   304 \                   evs : recur lost;  A ~: lost |]                       \
   305 \                ==> X : parts (sees lost Spy evs)";
   306 by (etac rev_mp 1);
   307 by (etac recur.induct 1);
   308 by parts_Fake_tac;
   309 (*RA3 requires a further induction*)
   310 by (etac responses.induct 5);
   311 by (ALLGOALS Asm_simp_tac);
   312 (*Fake*)
   313 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   314                              impOfSubs Fake_parts_insert]
   315                       addss (!simpset addsimps [parts_insert_sees])) 2);
   316 (*Two others*)
   317 by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
   318 qed "Hash_imp_body";
   319 
   320 
   321 (** The Nonce NA uniquely identifies A's message. 
   322     This theorem applies to steps RA1 and RA2!
   323 
   324   Unicity is not used in other proofs but is desirable in its own right.
   325 **)
   326 
   327 goal thy 
   328  "!!evs. [| evs : recur lost; A ~: lost |]                   \
   329 \ ==> EX B' P'. ALL B P.                                     \
   330 \        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \
   331 \          -->  B=B' & P=P'";
   332 by (parts_induct_tac 1);
   333 by (etac responses.induct 3);
   334 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
   335 by (step_tac (!claset addSEs partsEs) 1);
   336 (*RA1,2: creation of new Nonce.  Move assertion into global context*)
   337 by (ALLGOALS (expand_case_tac "NA = ?y"));
   338 by (REPEAT_FIRST (ares_tac [exI]));
   339 by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
   340                               addSEs sees_Spy_partsEs) 1));
   341 val lemma = result();
   342 
   343 goalw thy [HPair_def]
   344  "!!evs.[| Hash[Key(shrK A)] {|Agent A,B,NA,P|} : parts (sees lost Spy evs);  \
   345 \          Hash[Key(shrK A)] {|Agent A,B',NA,P'|} : parts (sees lost Spy evs);\
   346 \          evs : recur lost;  A ~: lost |]                                    \
   347 \        ==> B=B' & P=P'";
   348 by (REPEAT (eresolve_tac partsEs 1));
   349 by (prove_unique_tac lemma 1);
   350 qed "unique_NA";
   351 
   352 
   353 (*** Lemmas concerning the Server's response
   354       (relations "respond" and "responses") 
   355 ***)
   356 
   357 goal thy
   358  "!!evs. [| RB : responses evs;  evs : recur lost |] \
   359 \ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
   360 by (etac responses.induct 1);
   361 by (ALLGOALS
   362     (asm_simp_tac 
   363      (analz_image_freshK_ss addsimps [Spy_analz_shrK,
   364                                       resp_analz_image_freshK])));
   365 qed "shrK_in_analz_respond";
   366 Addsimps [shrK_in_analz_respond];
   367 
   368 
   369 goal thy  
   370  "!!evs. [| RB : responses evs;                             \
   371 \           ALL K KK. KK <= Compl (range shrK) -->          \
   372 \                     (Key K : analz (Key``KK Un H)) =      \
   373 \                     (K : KK | Key K : analz H) |]         \
   374 \       ==> (Key K : analz (insert RB H)) --> \
   375 \           (Key K : parts{RB} | Key K : analz H)";
   376 by (etac responses.induct 1);
   377 by (ALLGOALS
   378     (asm_simp_tac 
   379      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
   380 (*Simplification using two distinct treatments of "image"*)
   381 by (simp_tac (!simpset addsimps [parts_insert2]) 1);
   382 by (fast_tac (!claset delrules [allE]) 1);
   383 qed "resp_analz_insert_lemma";
   384 
   385 bind_thm ("resp_analz_insert",
   386           raw_analz_image_freshK RSN
   387             (2, resp_analz_insert_lemma) RSN(2, rev_mp));
   388 
   389 
   390 (*The Server does not send such messages.  This theorem lets us avoid
   391   assuming B~=Server in RA4.*)
   392 goal thy 
   393  "!!evs. evs : recur lost       \
   394 \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
   395 \                  ~: set_of_list evs";
   396 by (etac recur.induct 1);
   397 by (etac (respond.induct) 5);
   398 by (Auto_tac());
   399 qed_spec_mp "Says_Server_not";
   400 AddSEs [Says_Server_not RSN (2,rev_notE)];
   401 
   402 
   403 (*The last key returned by respond indeed appears in a certificate*)
   404 goal thy 
   405  "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
   406 \ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
   407 by (etac respond.elim 1);
   408 by (ALLGOALS Asm_full_simp_tac);
   409 qed "respond_certificate";
   410 
   411 
   412 goal thy 
   413  "!!K'. (PB,RB,KXY) : respond evs                          \
   414 \  ==> EX A' B'. ALL A B N.                                \
   415 \        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
   416 \          -->   (A'=A & B'=B) | (A'=B & B'=A)";
   417 by (etac respond.induct 1);
   418 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
   419 (*Base case*)
   420 by (Fast_tac 1);
   421 by (Step_tac 1);
   422 by (expand_case_tac "K = KBC" 1);
   423 by (dtac respond_Key_in_parts 1);
   424 by (best_tac (!claset addSIs [exI]
   425                       addSEs partsEs
   426                       addDs [Key_in_parts_respond]) 1);
   427 by (expand_case_tac "K = KAB" 1);
   428 by (REPEAT (ares_tac [exI] 2));
   429 by (ex_strip_tac 1);
   430 by (dtac respond_certificate 1);
   431 by (Fast_tac 1);
   432 val lemma = result();
   433 
   434 goal thy 
   435  "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};      \
   436 \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
   437 \          (PB,RB,KXY) : respond evs |]                            \
   438 \ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
   439 by (prove_unique_tac lemma 1);
   440 qed "unique_session_keys";
   441 
   442 
   443 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3
   444     Does not in itself guarantee security: an attack could violate 
   445     the premises, e.g. by having A=Spy **)
   446 
   447 goal thy 
   448  "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur lost |]         \
   449 \        ==> ALL A A' N. A ~: lost & A' ~: lost -->                 \
   450 \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
   451 \            Key K ~: analz (insert RB (sees lost Spy evs))";
   452 by (etac respond.induct 1);
   453 by (forward_tac [respond_imp_responses] 2);
   454 by (forward_tac [respond_imp_not_used] 2);
   455 by (ALLGOALS (*23 seconds*)
   456     (asm_simp_tac 
   457      (analz_image_freshK_ss addsimps 
   458        [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
   459 by (ALLGOALS Simp_tac);
   460 by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
   461 by (step_tac (!claset addSEs [MPair_parts]) 1);
   462 (** LEVEL 7 **)
   463 by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
   464                       addDs  [impOfSubs analz_subset_parts]) 4);
   465 by (fast_tac (!claset addSDs [respond_certificate]) 3);
   466 by (best_tac (!claset addSEs partsEs
   467                       addDs [Key_in_parts_respond]
   468                       addss (!simpset)) 2);
   469 by (dtac unique_session_keys 1);
   470 by (etac respond_certificate 1);
   471 by (assume_tac 1);
   472 by (Fast_tac 1);
   473 qed_spec_mp "respond_Spy_not_see_session_key";
   474 
   475 
   476 goal thy
   477  "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}          \
   478 \              : parts (sees lost Spy evs);                \
   479 \           A ~: lost;  A' ~: lost;  evs : recur lost |]   \
   480 \        ==> Key K ~: analz (sees lost Spy evs)";
   481 by (etac rev_mp 1);
   482 by (etac recur.induct 1);
   483 by analz_Fake_tac;
   484 by (ALLGOALS
   485     (asm_simp_tac
   486      (!simpset addsimps [parts_insert_sees, analz_insert_freshK] 
   487                setloop split_tac [expand_if])));
   488 (*RA4*)
   489 by (spy_analz_tac 5);
   490 (*RA2*)
   491 by (spy_analz_tac 3);
   492 (*Fake*)
   493 by (spy_analz_tac 2);
   494 (*Base*)
   495 by (fast_tac (!claset addss (!simpset)) 1);
   496 (*RA3 remains*)
   497 by (step_tac (!claset delrules [impCE]) 1);
   498 (*RA3, case 2: K is an old key*)
   499 by (best_tac (!claset addSDs [resp_analz_insert]
   500                       addSEs partsEs
   501                       addDs [Key_in_parts_respond]
   502                       addss (!simpset)) 2);
   503 (*RA3, case 1: use lemma previously proved by induction*)
   504 by (fast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
   505                               (2,rev_notE)]) 1);
   506 qed "Spy_not_see_session_key";
   507 
   508 
   509 goal thy 
   510  "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}         \
   511 \              : parts(sees lost Spy evs);                \
   512 \           C ~: {A,A',Server};                           \
   513 \           A ~: lost;  A' ~: lost;  evs : recur lost |]  \
   514 \        ==> Key K ~: analz (sees lost C evs)";
   515 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   516 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   517 by (FIRSTGOAL (rtac Spy_not_see_session_key));
   518 by (REPEAT_FIRST
   519     (deepen_tac
   520      (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])) 0));
   521 qed "Agent_not_see_session_key";
   522 
   523 
   524 (**** Authenticity properties for Agents ****)
   525 
   526 (*The response never contains Hashes*)
   527 goal thy
   528  "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
   529 \           (PB,RB,K) : respond evs |]                      \
   530 \        ==> Hash {|Key (shrK B), M|} : parts H";
   531 by (etac rev_mp 1);
   532 by (etac (respond_imp_responses RS responses.induct) 1);
   533 by (Auto_tac());
   534 qed "Hash_in_parts_respond";
   535 
   536 (*Only RA1 or RA2 can have caused such a part of a message to appear.
   537   This result is of no use to B, who cannot verify the Hash.  Moreover,
   538   it can say nothing about how recent A's message is.  It might later be
   539   used to prove B's presence to A at the run's conclusion.*)
   540 goalw thy [HPair_def]
   541  "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
   542 \             : parts (sees lost Spy evs);                        \
   543 \            A ~: lost;  evs : recur lost |]                        \
   544 \        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
   545 \             : set_of_list evs";
   546 by (etac rev_mp 1);
   547 by (parts_induct_tac 1);
   548 (*RA3*)
   549 by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
   550 qed_spec_mp "Hash_auth_sender";
   551 
   552 (** These two results subsume (for all agents) the guarantees proved
   553     separately for A and B in the Otway-Rees protocol.
   554 **)
   555 
   556 
   557 (*Certificates can only originate with the Server.*)
   558 goal thy 
   559  "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
   560 \           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
   561 \        ==> EX C RC. Says Server C RC : set_of_list evs &   \
   562 \                     Crypt (shrK A) Y : parts {RC}";
   563 by (etac rev_mp 1);
   564 by (parts_induct_tac 1);
   565 (*RA4*)
   566 by (Fast_tac 4);
   567 (*RA3*)
   568 by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
   569     THEN Fast_tac 3);
   570 (*RA1*)
   571 by (Fast_tac 1);
   572 (*RA2: it cannot be a new Nonce, contradiction.*)
   573 by (deepen_tac (!claset delrules [impCE]
   574                       addSIs [disjI2]
   575                       addSEs [MPair_parts]
   576                       addDs  [parts.Body]
   577                       unsafe_addss  (!simpset)) 0 1);
   578 qed "Cert_imp_Server_msg";