Corrected comments
authorpaulson
Fri Dec 20 10:23:48 1996 +0100 (1996-12-20)
changeset 245492f43ed48935
parent 2453 2d416226b27d
child 2455 9c4444bfd44e
Corrected comments
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/Yahalom.ML
     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|}|}  \
     2.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Dec 19 17:02:27 1996 +0100
     2.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Dec 20 10:23:48 1996 +0100
     2.3 @@ -625,8 +625,7 @@
     2.4  by analz_Fake_tac;
     2.5  by (ALLGOALS  (*22 seconds*)
     2.6      (asm_simp_tac 
     2.7 -     (!simpset addsimps ([not_parts_not_analz,
     2.8 -                          analz_image_newK,
     2.9 +     (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
    2.10                            insert_Key_singleton, insert_Key_image]
    2.11                           @ pushes)
    2.12                 setloop split_tac [expand_if])));
    2.13 @@ -644,13 +643,13 @@
    2.14                        addDs [unique_session_keys]
    2.15                        addss (!simpset)) 2);
    2.16  (*YM4*)
    2.17 -(** LEVEL 11 **)
    2.18 +(** LEVEL 10 **)
    2.19  by (rtac (impI RS allI) 1);
    2.20  by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
    2.21  by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
    2.22  by (asm_simp_tac (!simpset addsimps [analz_image_newK]
    2.23                             setloop split_tac [expand_if]) 1);
    2.24 -(** LEVEL 15 **)
    2.25 +(** LEVEL 14 **)
    2.26  by (grind_tac 1);
    2.27  by (REPEAT (dtac not_analz_insert 1));
    2.28  by (lost_tac "A" 1);