Added a comment
authorpaulson
Tue Jul 01 10:37:42 1997 +0200 (1997-07-01)
changeset 34708160cc3f6d40
parent 3469 61d927bd57ec
child 3471 cd37ec057028
Added a comment
src/HOL/Auth/Message.ML
src/HOL/Auth/WooLam.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Jul 01 10:37:03 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Tue Jul 01 10:37:42 1997 +0200
     1.3 @@ -824,7 +824,9 @@
     1.4  
     1.5  (*** Tactics useful for many protocol proofs ***)
     1.6  
     1.7 -(*Prove base case (subgoal i) and simplify others*)
     1.8 +(*Prove base case (subgoal i) and simplify others.  A typical base case
     1.9 +  concerns  Crypt K X ~: Key``shrK``lost  and cannot be proved by rewriting
    1.10 +  alone.*)
    1.11  fun prove_simple_subgoals_tac i = 
    1.12      fast_tac (!claset addss (!simpset)) i THEN
    1.13      ALLGOALS Asm_simp_tac;
     2.1 --- a/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:03 1997 +0200
     2.2 +++ b/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:42 1997 +0200
     2.3 @@ -47,7 +47,10 @@
     2.4               Says B' A (Nonce NB) : set evs |]
     2.5            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
     2.6  
     2.7 -         (*Bob forwards Alice's response to the Server.*)
     2.8 +         (*Bob forwards Alice's response to the Server.  NOTE: usually
     2.9 +           the messages are shown in chronological order, for clarity.
    2.10 +           But here, exchanging the two events would cause the lemma
    2.11 +           WL4_analz_sees_Spy to pick up the wrong assumption!*)
    2.12      WL4  "[| evs: woolam;  B ~= Server;  
    2.13               Says A'  B X         : set evs;
    2.14               Says A'' B (Agent A) : set evs |]