src/HOL/Auth/OtwayRees_AN.ML
changeset 2454 92f43ed48935
parent 2451 ce85a2aafc7a
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Dec 19 17:02:27 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 20 10:23:48 1996 +0100
     1.3 @@ -295,11 +295,8 @@
     1.4  qed_spec_mp "NA_Crypt_imp_Server_msg";
     1.5  
     1.6  
     1.7 -(*Corollary: if A receives B's OR4 message and the nonce NA agrees
     1.8 -  then the key really did come from the Server!  CANNOT prove this of the
     1.9 -  bad form of this protocol, even though we can prove
    1.10 -  Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
    1.11 -  the Server's message from its nonce NA.)*)
    1.12 +(*Corollary: if A receives B's OR4 message then it originated with the Server.
    1.13 +  Freshness may be inferred from nonce NA.*)
    1.14  goal thy 
    1.15   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    1.16  \            : set_of_list evs;                                         \
    1.17 @@ -386,8 +383,8 @@
    1.18  qed_spec_mp "NB_Crypt_imp_Server_msg";
    1.19  
    1.20  
    1.21 -(*Guarantee for B: if it gets a message with matching NB then the Server
    1.22 -  has sent the correct message.*)
    1.23 +(*Guarantee for B: if it gets a well-formed certificate then the Server
    1.24 +  has sent the correct message in round 3.*)
    1.25  goal thy 
    1.26   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
    1.27  \           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \