src/HOL/Auth/Recur.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24)
changeset 4477 b3e5857d8d99
parent 4471 0abf9d3f4391
child 4509 828148415197
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     1 (*  Title:      HOL/Auth/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 set proof_timing;
    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 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
   168 	Spy_analz_shrK RSN (2, rev_iffD1)];
   169 
   170 
   171 (** Nobody can have used non-existent keys! **)
   172 
   173 goal thy
   174  "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
   175 \        ==> K : range shrK";
   176 by (etac rev_mp 1);
   177 by (etac (respond_imp_responses RS responses.induct) 1);
   178 by Auto_tac;
   179 qed_spec_mp "Key_in_keysFor_parts";
   180 
   181 
   182 goal thy "!!evs. evs : recur ==>          \
   183 \                Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   184 by (parts_induct_tac 1);
   185 (*RA3*)
   186 by (best_tac (claset() addDs  [Key_in_keysFor_parts]
   187 	      addss  (simpset() addsimps [parts_insert_spies])) 2);
   188 (*Fake*)
   189 by (best_tac
   190       (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   191                addIs  [impOfSubs analz_subset_parts]
   192                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
   193                addss  (simpset())) 1);
   194 qed_spec_mp "new_keys_not_used";
   195 
   196 
   197 bind_thm ("new_keys_not_analzd",
   198           [analz_subset_parts RS keysFor_mono,
   199            new_keys_not_used] MRS contra_subsetD);
   200 
   201 Addsimps [new_keys_not_used, new_keys_not_analzd];
   202 
   203 
   204 
   205 (*** Proofs involving analz ***)
   206 
   207 (*For proofs involving analz.*)
   208 val analz_spies_tac = 
   209     etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
   210     dtac RA2_analz_spies 4 THEN 
   211     forward_tac [respond_imp_responses] 5                THEN
   212     dtac RA4_analz_spies 6;
   213 
   214 
   215 (** Session keys are not used to encrypt other session keys **)
   216 
   217 (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
   218   Note that it holds for *any* set H (not just "spies evs")
   219   satisfying the inductive hypothesis.*)
   220 goal thy  
   221  "!!evs. [| RB : responses evs;                             \
   222 \           ALL K KK. KK <= Compl (range shrK) -->          \
   223 \                     (Key K : analz (Key``KK Un H)) =      \
   224 \                     (K : KK | Key K : analz H) |]         \
   225 \       ==> ALL K KK. KK <= Compl (range shrK) -->          \
   226 \                     (Key K : analz (insert RB (Key``KK Un H))) = \
   227 \                     (K : KK | Key K : analz (insert RB H))";
   228 by (etac responses.induct 1);
   229 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   230 qed "resp_analz_image_freshK_lemma";
   231 
   232 (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
   233 goal thy  
   234  "!!evs. evs : recur ==>                                    \
   235 \  ALL K KK. KK <= Compl (range shrK) -->                   \
   236 \            (Key K : analz (Key``KK Un (spies evs))) =  \
   237 \            (K : KK | Key K : analz (spies evs))";
   238 by (etac recur.induct 1);
   239 by analz_spies_tac;
   240 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   241 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   242 by (ALLGOALS 
   243     (asm_simp_tac
   244      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
   245 (*Fake*) 
   246 by (spy_analz_tac 1);
   247 val raw_analz_image_freshK = result();
   248 qed_spec_mp "analz_image_freshK";
   249 
   250 
   251 (*Instance of the lemma with H replaced by (spies evs):
   252    [| RB : responses evs;  evs : recur; |]
   253    ==> KK <= Compl (range shrK) --> 
   254        Key K : analz (insert RB (Key``KK Un spies evs)) =
   255        (K : KK | Key K : analz (insert RB (spies evs))) 
   256 *)
   257 bind_thm ("resp_analz_image_freshK",
   258           raw_analz_image_freshK RSN
   259             (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
   260 
   261 goal thy
   262  "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>              \
   263 \        Key K : analz (insert (Key KAB) (spies evs)) =      \
   264 \        (K = KAB | Key K : analz (spies evs))";
   265 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   266 qed "analz_insert_freshK";
   267 
   268 
   269 (*Everything that's hashed is already in past traffic. *)
   270 goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs);  \
   271 \                   evs : recur;  A ~: bad |]                       \
   272 \                ==> X : parts (spies evs)";
   273 by (etac rev_mp 1);
   274 by (parts_induct_tac 1);
   275 (*RA3 requires a further induction*)
   276 by (etac responses.induct 2);
   277 by (ALLGOALS Asm_simp_tac);
   278 (*Fake*)
   279 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1);
   280 by (Fake_parts_insert_tac 1);
   281 qed "Hash_imp_body";
   282 
   283 
   284 (** The Nonce NA uniquely identifies A's message. 
   285     This theorem applies to steps RA1 and RA2!
   286 
   287   Unicity is not used in other proofs but is desirable in its own right.
   288 **)
   289 
   290 goal thy 
   291  "!!evs. [| evs : recur; A ~: bad |]                   \
   292 \ ==> EX B' P'. ALL B P.                                     \
   293 \        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
   294 \          -->  B=B' & P=P'";
   295 by (parts_induct_tac 1);
   296 by (Fake_parts_insert_tac 1);
   297 by (etac responses.induct 3);
   298 by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib]))); 
   299 by (clarify_tac (claset() addSEs partsEs) 1);
   300 (*RA1,2: creation of new Nonce.  Move assertion into global context*)
   301 by (ALLGOALS (expand_case_tac "NA = ?y"));
   302 by (REPEAT_FIRST (ares_tac [exI]));
   303 by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]
   304                                addSEs spies_partsEs) 1));
   305 val lemma = result();
   306 
   307 goalw thy [HPair_def]
   308  "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(spies evs); \
   309 \        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \
   310 \        evs : recur;  A ~: bad |]                                     \
   311 \      ==> B=B' & P=P'";
   312 by (REPEAT (eresolve_tac partsEs 1));
   313 by (prove_unique_tac lemma 1);
   314 qed "unique_NA";
   315 
   316 
   317 (*** Lemmas concerning the Server's response
   318       (relations "respond" and "responses") 
   319 ***)
   320 
   321 goal thy
   322  "!!evs. [| RB : responses evs;  evs : recur |] \
   323 \ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
   324 by (etac responses.induct 1);
   325 by (ALLGOALS
   326     (asm_simp_tac 
   327      (analz_image_freshK_ss addsimps [Spy_analz_shrK,
   328                                       resp_analz_image_freshK])));
   329 qed "shrK_in_analz_respond";
   330 Addsimps [shrK_in_analz_respond];
   331 
   332 
   333 goal thy  
   334  "!!evs. [| RB : responses evs;                             \
   335 \           ALL K KK. KK <= Compl (range shrK) -->          \
   336 \                     (Key K : analz (Key``KK Un H)) =      \
   337 \                     (K : KK | Key K : analz H) |]         \
   338 \       ==> (Key K : analz (insert RB H)) -->               \
   339 \           (Key K : parts{RB} | Key K : analz H)";
   340 by (etac responses.induct 1);
   341 by (ALLGOALS
   342     (asm_simp_tac 
   343      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
   344 (*Simplification using two distinct treatments of "image"*)
   345 by (simp_tac (simpset() addsimps [parts_insert2]) 1);
   346 by (blast_tac (claset() delrules [allE]) 1);
   347 qed "resp_analz_insert_lemma";
   348 
   349 bind_thm ("resp_analz_insert",
   350           raw_analz_image_freshK RSN
   351             (2, resp_analz_insert_lemma) RSN(2, rev_mp));
   352 
   353 
   354 (*The Server does not send such messages.  This theorem lets us avoid
   355   assuming B~=Server in RA4.*)
   356 goal thy 
   357  "!!evs. evs : recur \
   358 \        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
   359 by (etac recur.induct 1);
   360 by (etac (respond.induct) 5);
   361 by Auto_tac;
   362 qed_spec_mp "Says_Server_not";
   363 AddSEs [Says_Server_not RSN (2,rev_notE)];
   364 
   365 
   366 (*The last key returned by respond indeed appears in a certificate*)
   367 goal thy 
   368  "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
   369 \ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
   370 by (etac respond.elim 1);
   371 by (ALLGOALS Asm_full_simp_tac);
   372 qed "respond_certificate";
   373 
   374 
   375 goal thy 
   376  "!!K'. (PB,RB,KXY) : respond evs                          \
   377 \  ==> EX A' B'. ALL A B N.                                \
   378 \        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
   379 \          -->   (A'=A & B'=B) | (A'=B & B'=A)";
   380 by (etac respond.induct 1);
   381 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib]))); 
   382 (*Base case*)
   383 by (Blast_tac 1);
   384 by Safe_tac;
   385 by (expand_case_tac "K = KBC" 1);
   386 by (dtac respond_Key_in_parts 1);
   387 by (blast_tac (claset() addSIs [exI]
   388                        addSEs partsEs
   389                        addDs [Key_in_parts_respond]) 1);
   390 by (expand_case_tac "K = KAB" 1);
   391 by (REPEAT (ares_tac [exI] 2));
   392 by (ex_strip_tac 1);
   393 by (dtac respond_certificate 1);
   394 by (Fast_tac 1);
   395 val lemma = result();
   396 
   397 goal thy 
   398  "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};      \
   399 \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
   400 \          (PB,RB,KXY) : respond evs |]                            \
   401 \ ==>   (A'=A & B'=B) | (A'=B & B'=A)";
   402 by (prove_unique_tac lemma 1);
   403 qed "unique_session_keys";
   404 
   405 
   406 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3
   407     Does not in itself guarantee security: an attack could violate 
   408     the premises, e.g. by having A=Spy **)
   409 
   410 goal thy 
   411  "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur |]              \
   412 \        ==> ALL A A' N. A ~: bad & A' ~: bad -->                 \
   413 \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
   414 \            Key K ~: analz (insert RB (spies evs))";
   415 by (etac respond.induct 1);
   416 by (forward_tac [respond_imp_responses] 2);
   417 by (forward_tac [respond_imp_not_used] 2);
   418 by (ALLGOALS (*6 seconds*)
   419     (asm_simp_tac 
   420      (analz_image_freshK_ss 
   421         addsimps expand_ifs
   422 	addsimps 
   423           [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
   424 by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib])));
   425 (** LEVEL 5 **)
   426 by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
   427 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
   428 by (ALLGOALS Clarify_tac);
   429 by (blast_tac (claset() addSDs  [resp_analz_insert]
   430 		       addIs  [impOfSubs analz_subset_parts]) 2);
   431 by (blast_tac (claset() addSDs [respond_certificate]) 1);
   432 by (Asm_full_simp_tac 1);
   433 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
   434 by (blast_tac
   435     (claset() addSEs [MPair_parts]
   436 	     addDs [parts.Body,
   437 		    respond_certificate RSN (2, unique_session_keys)]) 1);
   438 qed_spec_mp "respond_Spy_not_see_session_key";
   439 
   440 
   441 goal thy
   442  "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
   443 \           A ~: bad;  A' ~: bad;  evs : recur |]                      \
   444 \        ==> Key K ~: analz (spies evs)";
   445 by (etac rev_mp 1);
   446 by (etac recur.induct 1);
   447 by analz_spies_tac;
   448 by (ALLGOALS
   449     (asm_simp_tac
   450      (simpset() addsimps (expand_ifs @
   451 			 [analz_insert_eq, parts_insert_spies, 
   452 			  analz_insert_freshK]))));
   453 (*RA4*)
   454 by (spy_analz_tac 5);
   455 (*RA2*)
   456 by (spy_analz_tac 3);
   457 (*Fake*)
   458 by (spy_analz_tac 2);
   459 (*Base*)
   460 by (Blast_tac 1);
   461 (*RA3 remains*)
   462 by (safe_tac (claset() delrules [impCE]));
   463 (*RA3, case 2: K is an old key*)
   464 by (blast_tac (claset() addSDs [resp_analz_insert]
   465                        addSEs partsEs
   466                        addDs  [Key_in_parts_respond]) 2);
   467 (*RA3, case 1: use lemma previously proved by induction*)
   468 by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN
   469 			       (2,rev_notE)]) 1);
   470 qed "Spy_not_see_session_key";
   471 
   472 
   473 (**** Authenticity properties for Agents ****)
   474 
   475 (*The response never contains Hashes*)
   476 goal thy
   477  "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
   478 \           (PB,RB,K) : respond evs |]                      \
   479 \        ==> Hash {|Key (shrK B), M|} : parts H";
   480 by (etac rev_mp 1);
   481 by (etac (respond_imp_responses RS responses.induct) 1);
   482 by Auto_tac;
   483 qed "Hash_in_parts_respond";
   484 
   485 (*Only RA1 or RA2 can have caused such a part of a message to appear.
   486   This result is of no use to B, who cannot verify the Hash.  Moreover,
   487   it can say nothing about how recent A's message is.  It might later be
   488   used to prove B's presence to A at the run's conclusion.*)
   489 goalw thy [HPair_def]
   490  "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
   491 \           A ~: bad;  evs : recur |]                      \
   492 \     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
   493 by (etac rev_mp 1);
   494 by (parts_induct_tac 1);
   495 by (Fake_parts_insert_tac 1);
   496 (*RA3*)
   497 by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1);
   498 qed_spec_mp "Hash_auth_sender";
   499 
   500 (** These two results subsume (for all agents) the guarantees proved
   501     separately for A and B in the Otway-Rees protocol.
   502 **)
   503 
   504 
   505 (*Certificates can only originate with the Server.*)
   506 goal thy 
   507  "!!evs. [| Crypt (shrK A) Y : parts (spies evs);    \
   508 \           A ~: bad;  A ~= Spy;  evs : recur |]       \
   509 \        ==> EX C RC. Says Server C RC : set evs  &     \
   510 \                     Crypt (shrK A) Y : parts {RC}";
   511 by (etac rev_mp 1);
   512 by (parts_induct_tac 1);
   513 by (Fake_parts_insert_tac 1);
   514 (*RA4*)
   515 by (Blast_tac 4);
   516 (*RA3*)
   517 by (full_simp_tac (simpset() addsimps [parts_insert_spies]) 3
   518     THEN Blast_tac 3);
   519 (*RA1*)
   520 by (Blast_tac 1);
   521 (*RA2: it cannot be a new Nonce, contradiction.*)
   522 by (Blast_tac 1);
   523 qed "Cert_imp_Server_msg";