New version with simpler disambiguation in YM3,
authorpaulson
Fri Nov 01 18:28:19 1996 +0100 (1996-11-01)
changeset 2155dc85854810eb
parent 2154 913b4fc7670a
child 2156 9c361df93bd5
New version with simpler disambiguation in YM3,
Oops message, and no encryption in YM2
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Nov 01 18:27:38 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Nov 01 18:28:19 1996 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  bind_thm ("YM4_parts_sees_Spy",
     1.5            YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
     1.6  
     1.7 -(*Relates to both YM4 and Revl*)
     1.8 +(*Relates to both YM4 and Oops*)
     1.9  goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
    1.10  \                  : set_of_list evs ==> \
    1.11  \                K : parts (sees lost Spy evs)";
    1.12 @@ -169,7 +169,6 @@
    1.13  \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
    1.14  by (parts_induct_tac 1);
    1.15  by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
    1.16 -
    1.17  (*YM1, YM2 and YM3*)
    1.18  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    1.19  (*Fake and YM4: these messages send unknown (X) components*)
    1.20 @@ -200,40 +199,25 @@
    1.21  Addsimps [new_keys_not_used, new_keys_not_analzd];
    1.22  
    1.23  
    1.24 -(*Describes the form of Key K when the following message is sent.  The use of
    1.25 -  "parts" strengthens the induction hyp for proving the Fake case.  The
    1.26 -  assumption A ~: lost prevents its being a Faked message.  (Based
    1.27 -  on NS_Shared/Says_S_message_form) *)
    1.28 -goal thy
    1.29 - "!!evs. evs: yahalom lost ==>                                        \
    1.30 -\        Crypt {|B, Key K, NA|} (shrK A) : parts (sees lost Spy evs)  \
    1.31 -\        --> A ~: lost --> (EX evt: yahalom lost. K = newK evt)";
    1.32 -by (parts_induct_tac 1);
    1.33 -by (Auto_tac());
    1.34 -qed_spec_mp "Reveal_message_lemma";
    1.35 -
    1.36 -(*EITHER describes the form of Key K when the following message is sent, 
    1.37 -  OR     reduces it to the Fake case.*)
    1.38 -
    1.39 +(*Describes the form of K when the Server sends this message.  Useful for
    1.40 +  Oops as well as main secrecy property.*)
    1.41  goal thy 
    1.42 - "!!evs. [| Says S A {|NB, Crypt {|B, Key K, NA|} (shrK A), X|} \
    1.43 -\           : set_of_list evs;                                  \
    1.44 -\           evs : yahalom lost |]                               \
    1.45 -\        ==> (EX evt: yahalom lost. K = newK evt)               \
    1.46 -\          | Key K : analz (sees lost Spy evs)";
    1.47 -br (Reveal_message_lemma RS disjCI) 1;
    1.48 -ba 1;
    1.49 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    1.50 -                      addDs [impOfSubs analz_subset_parts]) 1);
    1.51 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    1.52 -                      addss (!simpset)) 1);
    1.53 -qed "Reveal_message_form";
    1.54 + "!!evs. [| Says Server A {|NB', Crypt {|Agent B, K, NA|} (shrK A), X|} \
    1.55 +\            : set_of_list evs;                                         \
    1.56 +\           evs : yahalom lost |]                                       \
    1.57 +\        ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
    1.58 +by (etac rev_mp 1);
    1.59 +by (etac yahalom.induct 1);
    1.60 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.61 +qed "Says_Server_message_form";
    1.62  
    1.63  
    1.64  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
    1.65  val analz_Fake_tac = 
    1.66      dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
    1.67 -    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
    1.68 +    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    1.69 +    assume_tac 7 THEN Full_simp_tac 7 THEN
    1.70 +    REPEAT ((eresolve_tac [bexE,conjE] ORELSE' hyp_subst_tac) 7);
    1.71  
    1.72  
    1.73  (****
    1.74 @@ -255,16 +239,14 @@
    1.75  by (etac yahalom.induct 1);
    1.76  by analz_Fake_tac;
    1.77  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
    1.78 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 8));
    1.79  by (ALLGOALS  (*Takes 26 secs*)
    1.80      (asm_simp_tac 
    1.81       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.82                           @ pushes)
    1.83                 setloop split_tac [expand_if])));
    1.84 -(** LEVEL 5 **)
    1.85 -(*Reveal case 2, YM4, Fake*) 
    1.86 -by (EVERY (map spy_analz_tac [6, 4, 2]));
    1.87 -(*Reveal case 1, YM3, Base*)
    1.88 +(*YM4, Fake*) 
    1.89 +by (EVERY (map spy_analz_tac [4, 2]));
    1.90 +(*Oops, YM3, Base*)
    1.91  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
    1.92  qed_spec_mp "analz_image_newK";
    1.93  
    1.94 @@ -282,11 +264,10 @@
    1.95  
    1.96  goal thy 
    1.97   "!!evs. evs : yahalom lost ==>                                     \
    1.98 -\      EX A' B' NA' NB'. ALL A B NA NB.                             \
    1.99 +\      EX A' B' NA' NB' X'. ALL A B NA NB X.                        \
   1.100  \          Says Server A                                            \
   1.101 -\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),            \
   1.102 -\                 Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}           \
   1.103 -\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB'";
   1.104 +\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
   1.105 +\          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   1.106  by (etac yahalom.induct 1);
   1.107  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.108  by (Step_tac 1);
   1.109 @@ -301,12 +282,10 @@
   1.110  
   1.111  goal thy 
   1.112  "!!evs. [| Says Server A                                            \
   1.113 -\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),            \
   1.114 -\                 Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}           \
   1.115 +\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
   1.116  \           : set_of_list evs;                                      \
   1.117  \          Says Server A'                                           \
   1.118 -\           {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'),        \
   1.119 -\                  Crypt {|Agent A', Key K, NB', NB'|} (shrK B')|}       \
   1.120 +\           {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), X'|}   \
   1.121  \           : set_of_list evs;                                      \
   1.122  \          evs : yahalom lost |]                                    \
   1.123  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.124 @@ -318,49 +297,19 @@
   1.125  qed "unique_session_keys";
   1.126  
   1.127  
   1.128 -(*If the encrypted message appears then it originated with the Server*)
   1.129 -goal thy
   1.130 - "!!evs. [| Crypt {|Agent B, Key K, Nonce NA|} (shrK A)                \
   1.131 -\            : parts (sees lost Spy evs);                              \
   1.132 -\           A ~: lost;  evs : yahalom lost |]                          \
   1.133 -\         ==> EX NB. Says Server A                                            \
   1.134 -\              {|NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),            \
   1.135 -\                    Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}           \
   1.136 -\             : set_of_list evs";
   1.137 -by (etac rev_mp 1);
   1.138 -by (parts_induct_tac 1);
   1.139 -by (Fast_tac 1);
   1.140 -qed "A_trust_YM3";
   1.141 -
   1.142 -
   1.143 -(*Describes the form of K when the Server sends this message.*)
   1.144 -goal thy 
   1.145 - "!!evs. [| Says Server A                                           \
   1.146 -\            {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   1.147 -\                  Crypt {|Agent A, K, NB, NB|} (shrK B)|}          \
   1.148 -\            : set_of_list evs;   \
   1.149 -\           evs : yahalom lost |]                                   \
   1.150 -\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   1.151 -by (etac rev_mp 1);
   1.152 -by (etac yahalom.induct 1);
   1.153 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.154 -qed "Says_Server_message_form";
   1.155 -
   1.156 -
   1.157  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   1.158  
   1.159  goal thy 
   1.160 - "!!evs. [| A ~: lost;  B ~: lost;                                \
   1.161 -\           evs : yahalom lost;  evt : yahalom lost |]            \
   1.162 + "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
   1.163 +\           evs : yahalom lost |]            \
   1.164  \        ==> Says Server A                                           \
   1.165  \              {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),           \
   1.166 -\                    Crypt {|Agent A, Key K, NB, NB|} (shrK B)|}          \
   1.167 +\                    Crypt {|NB, Key K, Agent A|} (shrK B)|}          \
   1.168  \             : set_of_list evs -->                               \
   1.169 -\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->  \
   1.170 +\            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
   1.171  \            Key K ~: analz (sees lost Spy evs)";
   1.172  by (etac yahalom.induct 1);
   1.173  by analz_Fake_tac;
   1.174 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.175  by (ALLGOALS
   1.176      (asm_simp_tac 
   1.177       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.178 @@ -370,18 +319,11 @@
   1.179  by (fast_tac (!claset addIs [parts_insertI]
   1.180                        addEs [Says_imp_old_keys RS less_irrefl]
   1.181                        addss (!simpset)) 2);
   1.182 -(*Reveal case 2, OR4, Fake*) 
   1.183 +(*OR4, Fake*) 
   1.184  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.185 -(*Reveal case 1*) (** LEVEL 6 **)
   1.186 -by (case_tac "Aa : lost" 1);
   1.187 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.188 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.189 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.190 -(*So now we have  Aa ~: lost *)
   1.191 -bd (Says_imp_sees_Spy RS parts.Inj) 1;
   1.192 +(*Oops*)
   1.193  by (fast_tac (!claset delrules [disjE] 
   1.194 -	              addSEs [MPair_parts]
   1.195 -		      addDs [A_trust_YM3, unique_session_keys]
   1.196 +		      addDs [unique_session_keys]
   1.197  	              addss (!simpset)) 1);
   1.198  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.199  
   1.200 @@ -390,25 +332,25 @@
   1.201  goal thy 
   1.202   "!!evs. [| Says Server A                                         \
   1.203  \              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   1.204 -\                    Crypt {|Agent A, K, NB, NB|} (shrK B)|}      \
   1.205 +\                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
   1.206  \           : set_of_list evs;                                    \
   1.207 -\           Says A Spy {|NA, K|} ~: set_of_list evs;          \
   1.208 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>     \
   1.209 -\     K ~: analz (sees lost Spy evs)";
   1.210 +\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
   1.211 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.212 +\        ==> K ~: analz (sees lost Spy evs)";
   1.213  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.214  by (fast_tac (!claset addSEs [lemma]) 1);
   1.215  qed "Spy_not_see_encrypted_key";
   1.216  
   1.217  
   1.218  goal thy 
   1.219 - "!!evs. [| C ~: {A,B,Server};                                          \
   1.220 + "!!evs. [| C ~: {A,B,Server};                                    \
   1.221  \           Says Server A                                         \
   1.222  \              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   1.223 -\                    Crypt {|Agent A, K, NB, NB|} (shrK B)|}          \
   1.224 +\                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
   1.225  \           : set_of_list evs;                                    \
   1.226 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                \
   1.227 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.228 -\     K ~: analz (sees lost C evs)";
   1.229 +\           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
   1.230 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.231 +\        ==> K ~: analz (sees lost C evs)";
   1.232  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.233  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.234  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.235 @@ -416,18 +358,34 @@
   1.236  qed "Agent_not_see_encrypted_key";
   1.237  
   1.238  
   1.239 -(*** Security Guarantee for B upon receiving YM4 ***)
   1.240 +(*** Security Guarantees for A and B ***)
   1.241 +
   1.242 +(*If the encrypted message appears then it originated with the Server.*)
   1.243 +goal thy
   1.244 + "!!evs. [| Crypt {|Agent B, Key K, NA|} (shrK A)                \
   1.245 +\            : parts (sees lost Spy evs);                              \
   1.246 +\           A ~: lost;  evs : yahalom lost |]                          \
   1.247 +\         ==> EX NB. Says Server A                                     \
   1.248 +\                      {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),    \
   1.249 +\                            Crypt {|NB, Key K, Agent A|} (shrK B)|}   \
   1.250 +\                    : set_of_list evs";
   1.251 +by (etac rev_mp 1);
   1.252 +by (parts_induct_tac 1);
   1.253 +(*The nested conjunctions are entirely useless*)
   1.254 +by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI])));
   1.255 +qed "A_trust_YM3";
   1.256 +
   1.257  
   1.258  (*B knows, by the first part of A's message, that the Server distributed 
   1.259 -  the key for A and B.  But this part says nothing about nonces.*)
   1.260 +  the key for A and B. *)
   1.261  goal thy 
   1.262 - "!!evs. [| Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)    \
   1.263 -\            : parts (sees lost Spy evs); \
   1.264 -\           B ~: lost;  evs : yahalom lost |]                           \
   1.265 + "!!evs. [| Crypt {|Nonce NB, Key K, Agent A|} (shrK B)              \
   1.266 +\            : parts (sees lost Spy evs);                            \
   1.267 +\           B ~: lost;  evs : yahalom lost |]                        \
   1.268  \        ==> EX NA. Says Server A                                    \
   1.269 -\                    {|Nonce NB,                                   \
   1.270 -\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
   1.271 -\                      Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)|}\
   1.272 +\                    {|Nonce NB,                                     \
   1.273 +\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),  \
   1.274 +\                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
   1.275  \                       : set_of_list evs";
   1.276  by (etac rev_mp 1);
   1.277  by (parts_induct_tac 1);
   1.278 @@ -439,17 +397,16 @@
   1.279    Nonce NB is available in the first part.  However the 2nd part does assure B
   1.280    of A's existence.*)
   1.281  
   1.282 -(*What can B deduce from receipt of YM4?  Note how the two components of
   1.283 -  the message contribute to a single conclusion about the Server's message.*)
   1.284 +(*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   1.285 +  because we do not have to show that NB is secret. *)
   1.286  goal thy 
   1.287 - "!!evs. [| Says A' B {|Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B),              \
   1.288 + "!!evs. [| Says A' B {|Crypt {|Nonce NB, Key K, Agent A|} (shrK B),    \
   1.289  \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   1.290 -\           ALL N N'. Says A Spy {|N,N', Key K|} ~: set_of_list evs;    \
   1.291  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   1.292  \        ==> EX NA. Says Server A                                       \
   1.293 -\                    {|Nonce NB,                                   \
   1.294 -\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
   1.295 -\                      Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)|}\
   1.296 +\                    {|Nonce NB,                                        \
   1.297 +\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),     \
   1.298 +\                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|}    \
   1.299  \                   : set_of_list evs";
   1.300  be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
   1.301  by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
     2.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Nov 01 18:27:38 1996 +0100
     2.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Nov 01 18:28:19 1996 +0100
     2.3 @@ -6,6 +6,8 @@
     2.4  Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     2.5  
     2.6  This version trades encryption of NB for additional explicitness in YM3.
     2.7 +It also omits encryption in YM2.  The resulting protocol no longer guarantees
     2.8 +that the other agent is present.
     2.9  
    2.10  From page 259 of
    2.11    Burrows, Abadi and Needham.  A Logic of Authentication.
    2.12 @@ -35,38 +37,37 @@
    2.13  	   the sender is, hence the A' in the sender field.*)
    2.14      YM2  "[| evs: yahalom lost;  B ~= Server;
    2.15               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    2.16 -          ==> Says B Server 
    2.17 -                  {|Agent B, Nonce (newN evs), 
    2.18 -                    Crypt {|Agent A, Nonce NA|} (shrK B)|}
    2.19 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
    2.20                   # evs : yahalom lost"
    2.21  
    2.22           (*The Server receives Bob's message.  He responds by sending a
    2.23 -            new session key to Alice, with a packet for forwarding to Bob.*)
    2.24 -    YM3  "[| evs: yahalom lost;  A ~= Server;
    2.25 -             Says B' Server 
    2.26 -                  {|Agent B, Nonce NB, Crypt {|Agent A, Nonce NA|} (shrK B)|}
    2.27 +           new session key to Alice, with a packet for forwarding to Bob.
    2.28 +           Fields are reversed in the 2nd packet to prevent attacks.*)
    2.29 +    YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;
    2.30 +             Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    2.31                 : set_of_list evs |]
    2.32            ==> Says Server A
    2.33                 {|Nonce NB, 
    2.34                   Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
    2.35 -                 Crypt {|Agent A, Key (newK evs), Nonce NB, Nonce NB|} (shrK B)|}
    2.36 +                 Crypt {|Nonce NB, Key (newK evs), Agent A|} (shrK B)|}
    2.37                   # evs : yahalom lost"
    2.38  
    2.39           (*Alice receives the Server's (?) message, checks her Nonce, and
    2.40             uses the new session key to send Bob his Nonce.*)
    2.41 -    YM4  "[| evs: yahalom lost;  A ~= B;  
    2.42 +    YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    2.43               Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    2.44                          X|}
    2.45                 : set_of_list evs;
    2.46               Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    2.47            ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
    2.48  
    2.49 -         (*This message models possible leaks of session keys.  The Nonce NA
    2.50 -           identifies the protocol run.  We can't be sure about NB.*)
    2.51 -    Revl "[| evs: yahalom lost;  A ~= Spy;
    2.52 -             Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    2.53 -                        X|}
    2.54 -               : set_of_list evs |]
    2.55 -          ==> Says A Spy {|Nonce NA, Key K|} # evs : yahalom lost"
    2.56 +         (*This message models possible leaks of session keys.  The nonces
    2.57 +           identify the protocol run.  Quoting Server here ensures they are
    2.58 +           correct. *)
    2.59 +    Oops "[| evs: yahalom lost;  A ~= Spy;
    2.60 +             Says Server A {|Nonce NB, 
    2.61 +                             Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    2.62 +                             X|}  : set_of_list evs |]
    2.63 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
    2.64  
    2.65  end