--- 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);
--- 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),