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