# HG changeset patch
# User paulson
# Date 851073828 -3600
# Node ID 92f43ed48935528345fd520ed37ce7b7407ae893
# Parent  2d416226b27d056fda2b4be648e46c8e9f783ff8
Corrected comments

diff -r 2d416226b27d -r 92f43ed48935 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Dec 19 17:02:27 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 20 10:23:48 1996 +0100
@@ -295,11 +295,8 @@
 qed_spec_mp "NA_Crypt_imp_Server_msg";
 
 
-(*Corollary: if A receives B's OR4 message and the nonce NA agrees
-  then the key really did come from the Server!  CANNOT prove this of the
-  bad form of this protocol, even though we can prove
-  Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
-  the Server's message from its nonce NA.)*)
+(*Corollary: if A receives B's OR4 message then it originated with the Server.
+  Freshness may be inferred from nonce NA.*)
 goal thy 
  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \            : set_of_list evs;                                         \
@@ -386,8 +383,8 @@
 qed_spec_mp "NB_Crypt_imp_Server_msg";
 
 
-(*Guarantee for B: if it gets a message with matching NB then the Server
-  has sent the correct message.*)
+(*Guarantee for B: if it gets a well-formed certificate then the Server
+  has sent the correct message in round 3.*)
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
 \           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
diff -r 2d416226b27d -r 92f43ed48935 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Thu Dec 19 17:02:27 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Fri Dec 20 10:23:48 1996 +0100
@@ -625,8 +625,7 @@
 by analz_Fake_tac;
 by (ALLGOALS  (*22 seconds*)
     (asm_simp_tac 
-     (!simpset addsimps ([not_parts_not_analz,
-                          analz_image_newK,
+     (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
                           insert_Key_singleton, insert_Key_image]
                          @ pushes)
                setloop split_tac [expand_if])));
@@ -644,13 +643,13 @@
                       addDs [unique_session_keys]
                       addss (!simpset)) 2);
 (*YM4*)
-(** LEVEL 11 **)
+(** LEVEL 10 **)
 by (rtac (impI RS allI) 1);
 by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
 by (asm_simp_tac (!simpset addsimps [analz_image_newK]
                            setloop split_tac [expand_if]) 1);
-(** LEVEL 15 **)
+(** LEVEL 14 **)
 by (grind_tac 1);
 by (REPEAT (dtac not_analz_insert 1));
 by (lost_tac "A" 1);