--- a/src/HOL/Auth/Message.ML Tue Jul 01 10:37:03 1997 +0200
+++ b/src/HOL/Auth/Message.ML Tue Jul 01 10:37:42 1997 +0200
@@ -824,7 +824,9 @@
(*** Tactics useful for many protocol proofs ***)
-(*Prove base case (subgoal i) and simplify others*)
+(*Prove base case (subgoal i) and simplify others. A typical base case
+ concerns Crypt K X ~: Key``shrK``lost and cannot be proved by rewriting
+ alone.*)
fun prove_simple_subgoals_tac i =
fast_tac (!claset addss (!simpset)) i THEN
ALLGOALS Asm_simp_tac;
--- a/src/HOL/Auth/WooLam.thy Tue Jul 01 10:37:03 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Tue Jul 01 10:37:42 1997 +0200
@@ -47,7 +47,10 @@
Says B' A (Nonce NB) : set evs |]
==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
- (*Bob forwards Alice's response to the Server.*)
+ (*Bob forwards Alice's response to the Server. NOTE: usually
+ the messages are shown in chronological order, for clarity.
+ But here, exchanging the two events would cause the lemma
+ WL4_analz_sees_Spy to pick up the wrong assumption!*)
WL4 "[| evs: woolam; B ~= Server;
Says A' B X : set evs;
Says A'' B (Agent A) : set evs |]