src/HOL/Auth/OtwayRees.ML
changeset 2048 bb54fbba0071
parent 2045 ae1030e66745
child 2053 6c0594bfa726
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Oct 01 10:43:58 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Oct 01 15:49:29 1996 +0200
     1.3 @@ -43,25 +43,6 @@
     1.4                                :: otway.intrs))));
     1.5  qed "otway_mono";
     1.6  
     1.7 -(*The Spy can see more than anybody else, except for their initial state*)
     1.8 -goal thy 
     1.9 - "!!evs. evs : otway lost ==> \
    1.10 -\     sees lost A evs <= initState lost A Un sees lost Spy evs";
    1.11 -by (etac otway.induct 1);
    1.12 -by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.13 -                                addss (!simpset))));
    1.14 -qed "sees_agent_subset_sees_Spy";
    1.15 -
    1.16 -(*The Spy can see more than anybody else who's lost their key!*)
    1.17 -goal thy 
    1.18 - "!!evs. evs : otway lost ==> \
    1.19 -\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
    1.20 -by (etac otway.induct 1);
    1.21 -by (agent.induct_tac "A" 1);
    1.22 -by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
    1.23 -qed_spec_mp "sees_lost_agent_subset_sees_Spy";
    1.24 -
    1.25 -
    1.26  (*Nobody sends themselves messages*)
    1.27  goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.28  by (etac otway.induct 1);
    1.29 @@ -418,7 +399,7 @@
    1.30  
    1.31  
    1.32  
    1.33 -(**** Towards proving stronger authenticity properties ****)
    1.34 +(**** Authenticity properties relating to NA ****)
    1.35  
    1.36  (*Only OR1 can have caused such a part of a message to appear.*)
    1.37  goal thy 
    1.38 @@ -443,8 +424,8 @@
    1.39  goal thy 
    1.40   "!!evs. [| evs : otway lost; A ~: lost |]               \
    1.41  \ ==> EX B'. ALL B.    \
    1.42 -\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) --> \
    1.43 -\        B = B'";
    1.44 +\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
    1.45 +\        --> B = B'";
    1.46  by (etac otway.induct 1);
    1.47  by parts_Fake_tac;
    1.48  by (ALLGOALS Asm_simp_tac);
    1.49 @@ -463,9 +444,9 @@
    1.50  val lemma = result();
    1.51  
    1.52  goal thy 
    1.53 - "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs); \ 
    1.54 -\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees lost Spy evs); \ 
    1.55 -\          evs : otway lost;  A ~: lost |]                                         \
    1.56 + "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A): parts(sees lost Spy evs); \
    1.57 +\          Crypt {|NA, Agent A, Agent C|} (shrK A): parts(sees lost Spy evs); \
    1.58 +\          evs : otway lost;  A ~: lost |]                                    \
    1.59  \        ==> B = C";
    1.60  by (dtac lemma 1);
    1.61  by (assume_tac 1);
    1.62 @@ -473,7 +454,7 @@
    1.63  (*Duplicate the assumption*)
    1.64  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.65  by (fast_tac (!claset addSDs [spec]) 1);
    1.66 -qed "unique_OR1_nonce";
    1.67 +qed "unique_NA";
    1.68  
    1.69  
    1.70  val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
    1.71 @@ -503,19 +484,18 @@
    1.72  qed_spec_mp"no_nonce_OR1_OR2";
    1.73  
    1.74  
    1.75 -
    1.76  (*If the encrypted message appears, and A has used Nonce NA to start a run,
    1.77    then it originated with the Server!*)
    1.78  goal thy 
    1.79 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                     \
    1.80 -\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
    1.81 -\            Says A B {|Nonce NA, Agent A, Agent B,                          \
    1.82 -\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
    1.83 -\             : set_of_list evs -->                                          \
    1.84 -\            (EX NB. Says Server B                                           \
    1.85 -\                 {|Nonce NA,                                                \
    1.86 -\                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
    1.87 -\                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
    1.88 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
    1.89 +\    ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs)      \
    1.90 +\        --> Says A B {|NA, Agent A, Agent B,                          \
    1.91 +\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}      \
    1.92 +\             : set_of_list evs -->                                    \
    1.93 +\            (EX NB. Says Server B                                     \
    1.94 +\                 {|NA,                                                \
    1.95 +\                   Crypt {|NA, Key K|} (shrK A),                      \
    1.96 +\                   Crypt {|NB, Key K|} (shrK B)|}                     \
    1.97  \                   : set_of_list evs)";
    1.98  by (etac otway.induct 1);
    1.99  by parts_Fake_tac;
   1.100 @@ -538,31 +518,31 @@
   1.101  (*OR3*)  (** LEVEL 8 **)
   1.102  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.103  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.104 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.105 -                      addSEs [MPair_parts]
   1.106 -                      addEs  [unique_OR1_nonce]) 1);
   1.107  by (fast_tac (!claset addSEs [MPair_parts]
   1.108                        addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.109                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.110 -                      delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   1.111 -qed_spec_mp "Crypt_imp_Server_msg";
   1.112 +                      delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   1.113 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.114 +                      addSEs [MPair_parts]
   1.115 +                      addEs  [unique_NA]) 1);
   1.116 +qed_spec_mp "NA_Crypt_imp_Server_msg";
   1.117  
   1.118  
   1.119  (*Crucial property: if A receives B's OR4 message and the nonce NA agrees
   1.120    then the key really did come from the Server!  CANNOT prove this of the
   1.121 -  lost form of this protocol, even though we can prove
   1.122 +  bad form of this protocol, even though we can prove
   1.123    Spy_not_see_encrypted_key*)
   1.124  goal thy 
   1.125 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   1.126 -\        ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}  \
   1.127 -\             : set_of_list evs -->                                      \
   1.128 -\            Says A B {|Nonce NA, Agent A, Agent B,                      \
   1.129 -\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
   1.130 -\             : set_of_list evs -->                                      \
   1.131 -\            (EX NB. Says Server B                                       \
   1.132 -\                     {|Nonce NA,                                        \
   1.133 -\                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   1.134 -\                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   1.135 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   1.136 +\        ==> Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}        \
   1.137 +\             : set_of_list evs -->                                \
   1.138 +\            Says A B {|NA, Agent A, Agent B,                      \
   1.139 +\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   1.140 +\             : set_of_list evs -->                                \
   1.141 +\            (EX NB. Says Server B                                 \
   1.142 +\                     {|NA,                                        \
   1.143 +\                       Crypt {|NA, Key K|} (shrK A),              \
   1.144 +\                       Crypt {|NB, Key K|} (shrK B)|}             \
   1.145  \                       : set_of_list evs)";
   1.146  by (etac otway.induct 1);
   1.147  by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   1.148 @@ -581,16 +561,15 @@
   1.149                        addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
   1.150  (** LEVEL 8 **)
   1.151  (*Still subcases of Fake and OR4*)
   1.152 -by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   1.153 +by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.154                        addDs  [impOfSubs analz_subset_parts]) 1);
   1.155 -by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   1.156 +by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.157                        addEs  partsEs
   1.158                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.159 -val OR4_imp_Says_Server_A = 
   1.160 +val A_can_trust = 
   1.161      result() RSN (2, rev_mp) RS mp |> standard;
   1.162  
   1.163  
   1.164 -
   1.165  (*Describes the form of K and NA when the Server sends this message.*)
   1.166  goal thy 
   1.167   "!!evs. [| Says Server B \
   1.168 @@ -598,22 +577,25 @@
   1.169  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.170  \           evs : otway lost |]                                        \
   1.171  \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   1.172 -\            (EX i. NA = Nonce i)";
   1.173 +\            (EX i. NA = Nonce i) &                  \
   1.174 +\            (EX j. NB = Nonce j)";
   1.175  by (etac rev_mp 1);
   1.176  by (etac otway.induct 1);
   1.177 -by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.178 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.179  qed "Says_Server_message_form";
   1.180  
   1.181  
   1.182 -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 **)
   1.183 +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.184 +    Does not in itself guarantee security: an attack could violate 
   1.185 +    the premises, e.g. by having A=Spy **)
   1.186  
   1.187  goal thy 
   1.188   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
   1.189 -\        ==> Says Server B                                             \
   1.190 -\              {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   1.191 -\                Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   1.192 -\            Says A Spy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   1.193 -\            Key(newK evt) ~: analz (sees lost Spy evs)";
   1.194 +\        ==> Says Server B                                                 \
   1.195 +\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
   1.196 +\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
   1.197 +\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
   1.198 +\            Key K ~: analz (sees lost Spy evs)";
   1.199  by (etac otway.induct 1);
   1.200  by (dtac OR2_analz_sees_Spy 4);
   1.201  by (dtac OR4_analz_sees_Spy 6);
   1.202 @@ -628,25 +610,25 @@
   1.203  (*OR3*)
   1.204  by (fast_tac (!claset addSIs [parts_insertI]
   1.205                        addEs [Says_imp_old_keys RS less_irrefl]
   1.206 -                      addss (!simpset)) 3);
   1.207 +                      addss (!simpset addsimps [parts_insert2])) 3);
   1.208  (*Reveal case 2, OR4, OR2, Fake*) 
   1.209  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.210  (*Reveal case 1*) (** LEVEL 8 **)
   1.211  by (excluded_middle_tac "Aa : lost" 1);
   1.212 -(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
   1.213 +(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.214  by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   1.215  by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   1.216  (*So now we have  Aa ~: lost *)
   1.217 -by (dtac OR4_imp_Says_Server_A 1);
   1.218 +by (dtac A_can_trust 1);
   1.219  by (REPEAT (assume_tac 1));
   1.220  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.221  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.222  
   1.223  goal thy 
   1.224   "!!evs. [| Says Server B \
   1.225 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.226 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.227 -\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
   1.228 +\            {|NA, Crypt {|NA, K|} (shrK A),                             \
   1.229 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
   1.230 +\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.231  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.232  \        ==> K ~: analz (sees lost Spy evs)";
   1.233  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.234 @@ -655,11 +637,11 @@
   1.235  
   1.236  
   1.237  goal thy 
   1.238 - "!!evs. [| C ~: {A,B,Server}; \
   1.239 -\           Says Server B \
   1.240 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.241 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.242 -\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
   1.243 + "!!evs. [| C ~: {A,B,Server};                                           \
   1.244 +\           Says Server B                                                \
   1.245 +\            {|NA, Crypt {|NA, K|} (shrK A),                             \
   1.246 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
   1.247 +\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.248  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.249  \        ==> K ~: analz (sees lost C evs)";
   1.250  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.251 @@ -669,8 +651,136 @@
   1.252  qed "Agent_not_see_encrypted_key";
   1.253  
   1.254  
   1.255 +(**** Authenticity properties relating to NB ****)
   1.256 +
   1.257 +(*Only OR2 can have caused such a part of a message to appear.  We do not
   1.258 +  know anything about X'.*)
   1.259 +goal thy 
   1.260 + "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   1.261 +\        ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B)       \
   1.262 +\             : parts (sees lost Spy evs) -->                  \
   1.263 +\            (EX X'. Says B Server                             \
   1.264 +\             {|NA, Agent A, Agent B, X',                      \
   1.265 +\               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
   1.266 +\             : set_of_list evs)";
   1.267 +by (etac otway.induct 1);
   1.268 +by parts_Fake_tac;
   1.269 +by (ALLGOALS Asm_simp_tac);
   1.270 +(*Fake*)
   1.271 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.272 +                              impOfSubs Fake_parts_insert]) 2);
   1.273 +by (Auto_tac());
   1.274 +qed_spec_mp "Crypt_imp_OR2";
   1.275 +
   1.276 +
   1.277 +(** The Nonce NB uniquely identifies B's  message. **)
   1.278 +
   1.279 +goal thy 
   1.280 + "!!evs. [| evs : otway lost; B ~: lost |]               \
   1.281 +\ ==> EX NA' A'. ALL NA A.                              \
   1.282 +\      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
   1.283 +\      --> NA = NA' & A = A'";
   1.284 +by (etac otway.induct 1);
   1.285 +by parts_Fake_tac;
   1.286 +by (ALLGOALS Asm_simp_tac);
   1.287 +(*Fake*)
   1.288 +by (best_tac (!claset delrules [conjI,conjE]
   1.289 +		      addSDs [impOfSubs analz_subset_parts,
   1.290 +                              impOfSubs Fake_parts_insert]) 2);
   1.291 +(*Base case*)
   1.292 +by (fast_tac (!claset addss (!simpset)) 1);
   1.293 +by (Step_tac 1);
   1.294 +(*OR2: creation of new Nonce.  Move assertion into global context*)
   1.295 +by (excluded_middle_tac "NB = Nonce (newN evsa)" 1);
   1.296 +by (Asm_simp_tac 1);
   1.297 +by (fast_tac (!claset addSIs [exI]) 1);
   1.298 +by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   1.299 +val lemma = result();
   1.300 +
   1.301 +goal thy 
   1.302 + "!!evs.[| Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \
   1.303 +\                  : parts(sees lost Spy evs);         \
   1.304 +\          Crypt {|NC, NB, Agent C, Agent B|} (shrK B) \
   1.305 +\                  : parts(sees lost Spy evs);         \
   1.306 +\          evs : otway lost;  B ~: lost |]             \
   1.307 +\        ==> NC = NA & C = A";
   1.308 +by (dtac lemma 1);
   1.309 +by (assume_tac 1);
   1.310 +by (REPEAT (etac exE 1));
   1.311 +(*Duplicate the assumption*)
   1.312 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.313 +by (fast_tac (!claset addSDs [spec]) 1);
   1.314 +qed "unique_NB";
   1.315 +
   1.316 +
   1.317 +(*If the encrypted message appears, and B has used Nonce NB,
   1.318 +  then it originated with the Server!*)
   1.319 +goal thy 
   1.320 + "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   1.321 +\    ==> Crypt {|NB, Key K|} (shrK B) : parts (sees lost Spy evs)        \
   1.322 +\        --> (ALL X'. Says B Server                                      \
   1.323 +\                       {|NA, Agent A, Agent B, X',                      \
   1.324 +\                         Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
   1.325 +\             : set_of_list evs                                          \
   1.326 +\             --> Says Server B                                          \
   1.327 +\                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
   1.328 +\                        Crypt {|NB, Key K|} (shrK B)|}                  \
   1.329 +\                   : set_of_list evs)";
   1.330 +by (etac otway.induct 1);
   1.331 +by parts_Fake_tac;
   1.332 +by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   1.333 +(*Fake*)
   1.334 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.335 +                              impOfSubs Fake_parts_insert]) 1);
   1.336 +(*OR1: it cannot be a new Nonce, contradiction.*)
   1.337 +by (fast_tac (!claset addSIs [parts_insertI]
   1.338 +                      addSEs partsEs
   1.339 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.340 +                      addss (!simpset)) 1);
   1.341 +(*OR3 and OR4*)  (** LEVEL 5 **)
   1.342 +(*OR4*)
   1.343 +by (REPEAT (Safe_step_tac 2));
   1.344 +br (Crypt_imp_OR2 RS exE) 2;
   1.345 +by (REPEAT (fast_tac (!claset addEs partsEs) 2));
   1.346 +(*OR3*)  (** LEVEL 8 **)
   1.347 +by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.348 +by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   1.349 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.350 +                      addSEs [MPair_parts]
   1.351 +                      addDs  [unique_NB]) 2);
   1.352 +by (fast_tac (!claset addSEs [MPair_parts]
   1.353 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.354 +                      addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.355 +                      delrules [conjI, impCE] (*stop split-up*)) 1);
   1.356 +qed_spec_mp "NB_Crypt_imp_Server_msg";
   1.357 +
   1.358 +
   1.359 +(*Guarantee for B: if it gets a message with matching NB then the Server
   1.360 +  has sent the correct message.*)
   1.361 +goal thy 
   1.362 + "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   1.363 +\           Says S B {|NA, X, Crypt {|NB, Key K|} (shrK B)|}       \
   1.364 +\            : set_of_list evs;                                    \
   1.365 +\           Says B Server {|NA, Agent A, Agent B, X',              \
   1.366 +\                           Crypt {|NA, NB, Agent A, Agent B|}     \
   1.367 +\                                 (shrK B)|}                       \
   1.368 +\            : set_of_list evs |]                                  \
   1.369 +\        ==> Says Server B                                         \
   1.370 +\                 {|NA,                                            \
   1.371 +\                   Crypt {|NA, Key K|} (shrK A),                  \
   1.372 +\                   Crypt {|NB, Key K|} (shrK B)|}                 \
   1.373 +\                   : set_of_list evs";
   1.374 +by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.375 +                      addEs  partsEs
   1.376 +                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.377 +qed "B_can_trust";
   1.378 +
   1.379 +
   1.380 +B_can_trust RS Spy_not_see_encrypted_key;
   1.381 +
   1.382 +
   1.383  (** A session key uniquely identifies a pair of senders in the message
   1.384 -    encrypted by a good agent C. **)
   1.385 +    encrypted by a good agent C.  NEEDED?  INTERESTING?**)
   1.386  goal thy 
   1.387   "!!evs. evs : otway lost ==>                                           \
   1.388  \      EX A B. ALL C N.                                            \