Minor changes to comments
authorpaulson
Fri Nov 01 18:34:34 1996 +0100 (1996-11-01)
changeset 21569c361df93bd5
parent 2155 dc85854810eb
child 2157 50c26585e523
Minor changes to comments
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Nov 01 18:28:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 01 18:34:34 1996 +0100
     1.3 @@ -261,7 +261,7 @@
     1.4  by (etac yahalom.induct 1);
     1.5  by analz_Fake_tac;
     1.6  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
     1.7 -by (ALLGOALS  (*Takes 26 secs*)
     1.8 +by (ALLGOALS
     1.9      (asm_simp_tac 
    1.10       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.11                           @ pushes)
    1.12 @@ -455,7 +455,7 @@
    1.13   "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
    1.14  \      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
    1.15  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
    1.16 -by (parts_induct_tac 1);  (*TWO MINUTES*)
    1.17 +by (parts_induct_tac 1);  (*100 seconds??*)
    1.18  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
    1.19  (*YM2: creation of new Nonce.  Move assertion into global context*)
    1.20  by (expand_case_tac "NB = ?y" 1);
    1.21 @@ -650,7 +650,7 @@
    1.22  \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
    1.23  by (etac yahalom.induct 1);
    1.24  by analz_Fake_tac;
    1.25 -by (ALLGOALS  (*45 SECONDS*)
    1.26 +by (ALLGOALS  (*28 seconds*)
    1.27      (asm_simp_tac 
    1.28       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.29                            analz_image_newK,
    1.30 @@ -661,7 +661,7 @@
    1.31  by (fast_tac (!claset addss (!simpset)) 1);
    1.32  (*Fake*) (** LEVEL 4 **)
    1.33  by (spy_analz_tac 1);
    1.34 -(*YM1-YM3*)
    1.35 +(*YM1-YM3*) (*29 seconds*)
    1.36  by (EVERY (map grind_tac [3,2,1]));
    1.37  (*Oops*)
    1.38  by (Full_simp_tac 2);
     2.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:28:19 1996 +0100
     2.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:34:34 1996 +0100
     2.3 @@ -59,7 +59,8 @@
     2.4            ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
     2.5  
     2.6           (*This message models possible leaks of session keys.  The Nonces
     2.7 -           identify the protocol run.*)
     2.8 +           identify the protocol run.  Quoting Server here ensures they are
     2.9 +           correct.*)
    2.10      Oops "[| evs: yahalom lost;  A ~= Spy;
    2.11               Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} 
    2.12                                     (shrK A),