src/HOL/Auth/OtwayRees.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
--- a/src/HOL/Auth/OtwayRees.ML	Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Thu Jan 08 18:10:34 1998 +0100
@@ -60,15 +60,10 @@
 qed "OR4_analz_spies";
 
 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\                 ==> K : parts (spies evs)";
+\                ==> K : parts (spies evs)";
 by (Blast_tac 1);
 qed "Oops_parts_spies";
 
-(*OR2_analz... and OR4_analz... let us treat those cases using the same 
-  argument as for the Fake case.  This is possible for most, but not all,
-  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
-  messages originate from the Spy. *)
-
 bind_thm ("OR2_parts_spies",
           OR2_analz_spies RS (impOfSubs analz_subset_parts));
 bind_thm ("OR4_parts_spies",
@@ -86,8 +81,7 @@
 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
     sends messages containing X! **)
 
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+(*Spy never sees a good agent's shared key!*)
 goal thy 
  "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
 by (parts_induct_tac 1);
@@ -111,6 +105,7 @@
 by (parts_induct_tac 1);
 (*Fake*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
+(*OR2, OR3*)
 by (ALLGOALS Blast_tac);
 qed_spec_mp "new_keys_not_used";
 
@@ -141,8 +136,7 @@
 val analz_spies_tac = 
     dtac OR2_analz_spies 4 THEN 
     dtac OR4_analz_spies 6 THEN
-    forward_tac [Says_Server_message_form] 7 THEN
-    assume_tac 7 THEN
+    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
 
 
@@ -194,7 +188,7 @@
 by (ALLGOALS Clarify_tac);
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
-by (Best_tac 2);
+by (Best_tac 2);	(*Blast_tac's too slow (in reconstruction)*)
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message, and handle this case by contradiction*)
@@ -315,11 +309,11 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
+ "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
 \        ==> Says Server B                                            \
 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
-\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
+\            Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
 \            Key K ~: analz (spies evs)";
 by (etac otway.induct 1);
 by analz_spies_tac;
@@ -341,8 +335,8 @@
  "!!evs. [| Says Server B                                           \
 \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
 \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
-\           A ~: bad;  B ~: bad;  evs : otway |]                  \
+\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
+\           A ~: bad;  B ~: bad;  evs : otway |]                    \
 \        ==> Key K ~: analz (spies evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (claset() addSEs [lemma]) 1);