src/HOL/Auth/NS_Shared.ML
author paulson
Fri Sep 13 13:22:08 1996 +0200 (1996-09-13)
changeset 1997 6efba890341e
parent 1967 0ff58b41c037
child 1999 b5efc4108d04
permissions -rw-r--r--
No longer assumes Alice is not the Enemy in NS3.
Proofs do not need it, and the assumption complicated the liveness argument
     1 (*  Title:      HOL/Auth/NS_Shared
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
     7 
     8 From page 247 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 open NS_Shared;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 
    18 (** Weak liveness: there are traces that reach the end **)
    19 
    20 goal thy 
    21  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    22 \        ==> EX N K. EX evs: ns_shared.          \
    23 \               Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
    24 by (REPEAT (resolve_tac [exI,bexI] 1));
    25 br (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2;
    26 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    27 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    28 by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    29 qed "weak_liveness";
    30 
    31 (**** Inductive proofs about ns_shared ****)
    32 
    33 (*The Enemy can see more than anybody else, except for their initial state*)
    34 goal thy 
    35  "!!evs. evs : ns_shared ==> \
    36 \     sees A evs <= initState A Un sees Enemy evs";
    37 be ns_shared.induct 1;
    38 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    39 			        addss (!simpset))));
    40 qed "sees_agent_subset_sees_Enemy";
    41 
    42 
    43 (*Nobody sends themselves messages*)
    44 goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set_of_list evs";
    45 be ns_shared.induct 1;
    46 by (Auto_tac());
    47 qed_spec_mp "not_Says_to_self";
    48 Addsimps [not_Says_to_self];
    49 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    50 
    51 goal thy "!!evs. evs : ns_shared ==> Notes A X ~: set_of_list evs";
    52 be ns_shared.induct 1;
    53 by (Auto_tac());
    54 qed "not_Notes";
    55 Addsimps [not_Notes];
    56 AddSEs   [not_Notes RSN (2, rev_notE)];
    57 
    58 
    59 (*For reasoning about the encrypted portion of message NS3*)
    60 goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
    61 \                X : parts (sees Enemy evs)";
    62 by (fast_tac (!claset addSEs partsEs
    63 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    64 qed "NS3_msg_in_parts_sees_Enemy";
    65 			      
    66 
    67 (*** Shared keys are not betrayed ***)
    68 
    69 (*Enemy never sees another agent's shared key!*)
    70 goal thy 
    71  "!!evs. [| evs : ns_shared; A ~: bad |] ==> \
    72 \        Key (shrK A) ~: parts (sees Enemy evs)";
    73 be ns_shared.induct 1;
    74 bd NS3_msg_in_parts_sees_Enemy 5;
    75 by (Auto_tac());
    76 (*Deals with Fake message*)
    77 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    78 			     impOfSubs Fake_parts_insert]) 1);
    79 qed "Enemy_not_see_shrK";
    80 
    81 bind_thm ("Enemy_not_analz_shrK",
    82 	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    83 
    84 Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
    85 
    86 (*We go to some trouble to preserve R in the 3rd and 4th subgoals
    87   As usual fast_tac cannot be used because it uses the equalities too soon*)
    88 val major::prems = 
    89 goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
    90 \             evs : ns_shared;                             \
    91 \             A:bad ==> R                                  \
    92 \           |] ==> R";
    93 br ccontr 1;
    94 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
    95 by (swap_res_tac prems 2);
    96 by (ALLGOALS (fast_tac (!claset addIs prems)));
    97 qed "Enemy_see_shrK_E";
    98 
    99 bind_thm ("Enemy_analz_shrK_E", 
   100 	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   101 
   102 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   103 
   104 
   105 goal thy  
   106  "!!evs. evs : ns_shared ==>                              \
   107 \        (Key (shrK A) : analz (sees Enemy evs)) = (A : bad)";
   108 by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   109 		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   110 	              addss (!simpset)) 1);
   111 qed "shrK_mem_analz";
   112 
   113 Addsimps [shrK_mem_analz];
   114 
   115 
   116 (*** Future keys can't be seen or used! ***)
   117 
   118 (*Nobody can have SEEN keys that will be generated in the future.
   119   This has to be proved anew for each protocol description,
   120   but should go by similar reasoning every time.  Hardest case is the
   121   standard Fake rule.  
   122       The length comparison, and Union over C, are essential for the 
   123   induction! *)
   124 goal thy "!!evs. evs : ns_shared ==> \
   125 \                length evs <= length evs' --> \
   126 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   127 be ns_shared.induct 1;
   128 bd NS3_msg_in_parts_sees_Enemy 5;
   129 (*auto_tac does not work here, as it performs safe_tac first*)
   130 by (ALLGOALS Asm_simp_tac);
   131 by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   132 				       impOfSubs parts_insert_subset_Un,
   133 				       Suc_leD]
   134 			        addss (!simpset))));
   135 val lemma = result();
   136 
   137 (*Variant needed for the main theorem below*)
   138 goal thy 
   139  "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
   140 \        Key (newK evs') ~: parts (sees C evs)";
   141 by (fast_tac (!claset addDs [lemma]) 1);
   142 qed "new_keys_not_seen";
   143 Addsimps [new_keys_not_seen];
   144 
   145 (*Another variant: old messages must contain old keys!*)
   146 goal thy 
   147  "!!evs. [| Says A B X : set_of_list evs;  \
   148 \           Key (newK evt) : parts {X};    \
   149 \           evs : ns_shared                 \
   150 \        |] ==> length evt < length evs";
   151 br ccontr 1;
   152 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   153 	              addIs [impOfSubs parts_mono, leI]) 1);
   154 qed "Says_imp_old_keys";
   155 
   156 
   157 (*Nobody can have USED keys that will be generated in the future.
   158   ...very like new_keys_not_seen*)
   159 goal thy "!!evs. evs : ns_shared ==> \
   160 \                length evs <= length evs' --> \
   161 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   162 be ns_shared.induct 1;
   163 bd NS3_msg_in_parts_sees_Enemy 5;
   164 by (ALLGOALS Asm_simp_tac);
   165 (*NS1 and NS2*)
   166 map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
   167 (*Fake and NS3*)
   168 map (by o best_tac
   169      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   170 		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   171 		     Suc_leD]
   172 	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   173 	      addss (!simpset)))
   174     [2,1];
   175 (*NS4 and NS5: nonce exchange*)
   176 by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
   177 	                          addIs  [less_SucI, impOfSubs keysFor_mono]
   178 		                  addss (!simpset addsimps [le_def])) 0));
   179 val lemma = result();
   180 
   181 goal thy 
   182  "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
   183 \        newK evs' ~: keysFor (parts (sees C evs))";
   184 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   185 qed "new_keys_not_used";
   186 
   187 bind_thm ("new_keys_not_analzd",
   188 	  [analz_subset_parts RS keysFor_mono,
   189 	   new_keys_not_used] MRS contra_subsetD);
   190 
   191 Addsimps [new_keys_not_used, new_keys_not_analzd];
   192 
   193 
   194 (** Lemmas concerning the form of items passed in messages **)
   195 
   196 (*Describes the form *and age* of K, and the form of X,
   197   when the following message is sent*)
   198 goal thy 
   199  "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
   200 \           evs : ns_shared    \
   201 \        |] ==> (EX evt:ns_shared. \
   202 \                         K = Key(newK evt) & \
   203 \                         X = (Crypt {|K, Agent A|} (shrK B)) & \
   204 \                         K' = shrK A & \
   205 \                         length evt < length evs)";
   206 be rev_mp 1;
   207 be ns_shared.induct 1;
   208 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   209 qed "Says_Server_message_form";
   210 
   211 
   212 (*Describes the form of X when the following message is sent.  The use of
   213   "parts" strengthens the induction hyp for proving the Fake case.  The
   214   assumptions on A are needed to prevent its being a Faked message.*)
   215 goal thy
   216  "!!evs. evs : ns_shared ==>                                              \
   217 \        ALL A NA B K X.                                                  \
   218 \            Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)               \
   219 \               : parts (sees Enemy evs) &                                \
   220 \            A ~: bad --> \
   221 \          (EX evt:ns_shared. K = newK evt & \
   222 \                             X = (Crypt {|Key K, Agent A|} (shrK B)))";
   223 be ns_shared.induct 1;
   224 bd NS3_msg_in_parts_sees_Enemy 5;
   225 by (Step_tac 1);
   226 by (ALLGOALS Asm_full_simp_tac);
   227 by (fast_tac (!claset addss (!simpset)) 1);
   228 (*Remaining cases are Fake and NS2*)
   229 by (fast_tac (!claset addSDs [spec]) 2);
   230 (*Now for the Fake case*)
   231 by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   232 	              addDs  [impOfSubs analz_subset_parts]
   233 	              addss  (!simpset)) 1);
   234 qed_spec_mp "encrypted_form";
   235 
   236 
   237 (*If such a message is sent with a bad key then the Enemy sees it (even if
   238   he didn't send it in the first place).*)
   239 goal thy
   240  "!!evs. [| Says S A (Crypt {|N, B, K, X|} (shrK A)) : set_of_list evs;   \
   241 \           A : bad |]                                                    \
   242 \        ==> X : analz (sees Enemy evs)";
   243 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   244 	              addss (!simpset)) 1);
   245 qed_spec_mp "bad_encrypted_form";
   246 
   247 
   248 
   249 (*EITHER describes the form of X when the following message is sent, 
   250   OR     reduces it to the Fake case.
   251   Use Says_Server_message_form if applicable.*)
   252 goal thy 
   253  "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))    \
   254 \            : set_of_list evs;  evs : ns_shared |]                      \
   255 \        ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
   256 \                               X = (Crypt {|Key K, Agent A|} (shrK B))) | \
   257 \            X : analz (sees Enemy evs)";
   258 by (excluded_middle_tac "A : bad" 1);
   259 by (fast_tac (!claset addIs [bad_encrypted_form]) 2);
   260 by (forward_tac [encrypted_form] 1);
   261 br (parts.Inj RS conjI) 1;
   262 by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
   263 qed "Says_S_message_form";
   264 
   265 
   266 
   267 (****
   268  The following is to prove theorems of the form
   269 
   270           Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   271           Key K : analz (sees Enemy evs)
   272 
   273  A more general formula must be proved inductively.
   274 
   275 ****)
   276 
   277 
   278 (*NOT useful in this form, but it says that session keys are not used
   279   to encrypt messages containing other keys, in the actual protocol.
   280   We require that agents should behave like this subsequently also.*)
   281 goal thy 
   282  "!!evs. evs : ns_shared ==> \
   283 \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   284 \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   285 be ns_shared.induct 1;
   286 bd NS3_msg_in_parts_sees_Enemy 5;
   287 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   288 (*Deals with Faked messages*)
   289 by (best_tac (!claset addSEs partsEs
   290 		      addDs [impOfSubs analz_subset_parts,
   291                              impOfSubs parts_insert_subset_Un]
   292                       addss (!simpset)) 2);
   293 (*Base, NS4 and NS5*)
   294 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   295 result();
   296 
   297 
   298 (** Specialized rewriting for this proof **)
   299 
   300 Delsimps [image_insert];
   301 Addsimps [image_insert RS sym];
   302 
   303 Delsimps [image_Un];
   304 Addsimps [image_Un RS sym];
   305 
   306 goal thy "insert (Key (newK x)) (sees A evs) = \
   307 \         Key `` (newK``{x}) Un (sees A evs)";
   308 by (Fast_tac 1);
   309 val insert_Key_singleton = result();
   310 
   311 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   312 \         Key `` (f `` (insert x E)) Un C";
   313 by (Fast_tac 1);
   314 val insert_Key_image = result();
   315 
   316 
   317 (** Session keys are not used to encrypt other session keys **)
   318 
   319 (*Lemma for the trivial direction of the if-and-only-if*)
   320 goal thy  
   321  "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   322 \         (K : nE | Key K : analz sEe)  ==>     \
   323 \        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   324 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   325 val lemma = result();
   326 
   327 goal thy  
   328  "!!evs. evs : ns_shared ==> \
   329 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   330 \           (K : newK``E | Key K : analz (sees Enemy evs))";
   331 be ns_shared.induct 1;
   332 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   333 by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
   334 by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   335 by (ALLGOALS 
   336     (asm_simp_tac 
   337      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   338 			 @ pushes)
   339                setloop split_tac [expand_if])));
   340 (** LEVEL 5 **)
   341 (*NS3, Fake subcase*)
   342 by (enemy_analz_tac 5);
   343 (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   344 by (REPEAT (Fast_tac 3));
   345 (*Fake case*) (** LEVEL 7 **)
   346 by (enemy_analz_tac 2);
   347 (*Base case*)
   348 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   349 qed_spec_mp "analz_image_newK";
   350 
   351 
   352 goal thy
   353  "!!evs. evs : ns_shared ==>                               \
   354 \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   355 \        (K = newK evt | Key K : analz (sees Enemy evs))";
   356 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   357 				   insert_Key_singleton]) 1);
   358 by (Fast_tac 1);
   359 qed "analz_insert_Key_newK";
   360 
   361 
   362 (** First, two lemmas for the Fake and NS3 cases **)
   363 
   364 goal thy 
   365  "!!evs. [| X : synth (analz (sees Enemy evs));                \
   366 \           Crypt X' (shrK C) : parts{X};                      \
   367 \           C ~: bad;  evs : ns_shared |]  \
   368 \        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   369 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   370 	              addDs [impOfSubs parts_insert_subset_Un]
   371                       addss (!simpset)) 1);
   372 qed "Crypt_Fake_parts";
   373 
   374 goal thy 
   375  "!!evs. [| Crypt X' K : parts (sees A evs);  evs : ns_shared |]  \
   376 \        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   377 \            Crypt X' K : parts {Y}";
   378 bd parts_singleton 1;
   379 by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   380 qed "Crypt_parts_singleton";
   381 
   382 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   383 
   384 (*This says that the Key, K, uniquely identifies the message.
   385     But if Enemy knows C's key then he could send all sorts of nonsense.*)
   386 goal thy 
   387  "!!evs. evs : ns_shared ==>                      \
   388 \      EX X'. ALL C.                              \
   389 \       C ~: bad -->                              \
   390 \        (ALL S A Y. Says S A Y : set_of_list evs -->     \
   391 \         (ALL N B X. Crypt {|N, Agent B, Key K, X|} (shrK C) : parts{Y} --> \
   392 \          X=X'))";
   393 be ns_shared.induct 1;
   394 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   395 by (ALLGOALS 
   396     (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   397 by (REPEAT_FIRST (eresolve_tac [exE,disjE]));
   398 (*NS3: Fake (compromised) case*)
   399 by (ex_strip_tac 4);
   400 by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   401 			      Crypt_parts_singleton]) 4);
   402 (*NS3: Good case, no relevant messages*)
   403 by (fast_tac (!claset addSEs [exI] addss (!simpset)) 3);
   404 (*NS2: Case split propagates some context to other subgoal...*)
   405 by (excluded_middle_tac "K = newK evsa" 2);
   406 by (Asm_simp_tac 2);
   407 be exI 2;
   408 (*...we assume X is a very new message, and handle this case by contradiction*)
   409 by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   410 		      addSEs partsEs
   411 		      addEs [Says_imp_old_keys RS less_irrefl]
   412 	              addss (!simpset)) 2);
   413 (*Fake*) (** LEVEL 11 **)
   414 by (ex_strip_tac 1);
   415 by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   416 val lemma = result();
   417 
   418 
   419 (*In messages of this form, the session key uniquely identifies the rest*)
   420 goal thy 
   421  "!!evs. [| Says S A          \
   422 \             (Crypt {|N, Agent B, Key K, X|} (shrK C))     \
   423 \                  : set_of_list evs; \ 
   424 \           Says S' A'                                         \
   425 \             (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
   426 \                  : set_of_list evs;                         \
   427 \           evs : ns_shared;  C ~= Enemy;  C ~: bad;  C' ~: bad |] ==> X = X'";
   428 bd lemma 1;
   429 be exE 1;
   430 (*Duplicate the assumption*)
   431 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   432 (*Are these instantiations essential?*)
   433 by (dres_inst_tac [("x","C")] spec 1);
   434 by (dres_inst_tac [("x","C'")] spec 1);
   435 by (fast_tac (!claset addSDs [spec]) 1);
   436 qed "unique_session_keys";
   437 
   438 
   439 
   440 (*Crucial secrecy property: Enemy does not see the keys sent in msg NS2*)
   441 goal thy 
   442  "!!evs. [| Says Server A                                       \
   443 \            (Crypt {|N, Agent B, K, X|} K') : set_of_list evs;  \
   444 \           A ~: bad;  B ~: bad;  evs : ns_shared                  \
   445 \        |] ==>                                                          \
   446 \     K ~: analz (sees Enemy evs)";
   447 be rev_mp 1;
   448 be ns_shared.induct 1;
   449 by (ALLGOALS Asm_simp_tac);
   450 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   451 by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   452 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   453 by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   454 by (ALLGOALS 
   455     (asm_full_simp_tac 
   456      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   457 			  analz_insert_Key_newK] @ pushes)
   458                setloop split_tac [expand_if])));
   459 (*NS2*)
   460 by (fast_tac (!claset addSEs [less_irrefl]) 2);
   461 (*Fake case*) (** LEVEL 8 **)
   462 by (enemy_analz_tac 1);
   463 (*NS3: that message from the Server was sent earlier*)
   464 by (mp_tac 1);
   465 by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
   466 by (Step_tac 1);
   467 by (enemy_analz_tac 2);		(*Prove the Fake subcase*)
   468 by (asm_full_simp_tac
   469     (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   470 by (Step_tac 1);
   471 (**LEVEL 15 **)
   472 by (excluded_middle_tac "Aa : bad" 1);
   473 (*But this contradicts Key (newK evta) ~: analz (sees Enemy evsa) *)
   474 bd (Says_imp_sees_Enemy RS analz.Inj) 2;
   475 bd analz.Decrypt 2;
   476 by (Asm_full_simp_tac 2);
   477 by (Fast_tac 2);
   478 (*So now we know that (Friend i) is a good agent*)
   479 bd unique_session_keys 1;
   480 by (REPEAT_FIRST assume_tac);
   481 by (Auto_tac ());
   482 qed "Enemy_not_see_encrypted_key";