# HG changeset patch
# User paulson
# Date 846869674 -3600
# Node ID 9c361df93bd5874bf4e27f6e3eec71cca44d3fee
# Parent  dc85854810eb893d9abd0ac929591d4e39fa7e3b
Minor changes to comments

diff -r dc85854810eb -r 9c361df93bd5 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Fri Nov 01 18:28:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 01 18:34:34 1996 +0100
@@ -261,7 +261,7 @@
 by (etac yahalom.induct 1);
 by analz_Fake_tac;
 by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS  (*Takes 26 secs*)
+by (ALLGOALS
     (asm_simp_tac 
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
                          @ pushes)
@@ -455,7 +455,7 @@
  "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
 \      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
-by (parts_induct_tac 1);  (*TWO MINUTES*)
+by (parts_induct_tac 1);  (*100 seconds??*)
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
 (*YM2: creation of new Nonce.  Move assertion into global context*)
 by (expand_case_tac "NB = ?y" 1);
@@ -650,7 +650,7 @@
 \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by analz_Fake_tac;
-by (ALLGOALS  (*45 SECONDS*)
+by (ALLGOALS  (*28 seconds*)
     (asm_simp_tac 
      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
                           analz_image_newK,
@@ -661,7 +661,7 @@
 by (fast_tac (!claset addss (!simpset)) 1);
 (*Fake*) (** LEVEL 4 **)
 by (spy_analz_tac 1);
-(*YM1-YM3*)
+(*YM1-YM3*) (*29 seconds*)
 by (EVERY (map grind_tac [3,2,1]));
 (*Oops*)
 by (Full_simp_tac 2);
diff -r dc85854810eb -r 9c361df93bd5 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:28:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:34:34 1996 +0100
@@ -59,7 +59,8 @@
           ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
 
          (*This message models possible leaks of session keys.  The Nonces
-           identify the protocol run.*)
+           identify the protocol run.  Quoting Server here ensures they are
+           correct.*)
     Oops "[| evs: yahalom lost;  A ~= Spy;
              Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} 
                                    (shrK A),