src/HOL/Auth/OtwayRees_Bad.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jan 08 18:10:34 1998 +0100
@@ -20,6 +20,10 @@
 set proof_timing;
 HOL_quantifiers := false;
 
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
@@ -46,26 +50,23 @@
 
 (** For reasoning about the encrypted portion of messages **)
 
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
-\                X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
+\                ==> X : analz (spies evs)";
+by (dtac (Says_imp_spies RS analz.Inj) 1);
+by (Blast_tac 1);
 qed "OR2_analz_spies";
 
-goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
-\                X : analz (spies evs)";
-by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
+\                ==> X : analz (spies evs)";
+by (dtac (Says_imp_spies RS analz.Inj) 1);
+by (Blast_tac 1);
 qed "OR4_analz_spies";
 
 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\                 ==> K : parts (spies evs)";
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+\                ==> 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",
@@ -83,11 +84,10 @@
 (** 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);
-by (Fake_parts_insert_tac 1);
 by (ALLGOALS Blast_tac);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
@@ -108,7 +108,7 @@
 by (parts_induct_tac 1);
 (*Fake*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-(*OR1-3*)
+(*OR2, OR3*)
 by (ALLGOALS Blast_tac);
 qed_spec_mp "new_keys_not_used";
 
@@ -125,14 +125,13 @@
 (*Describes the form of K and NA when the Server sends this message.  Also
   for Oops case.*)
 goal thy 
- "!!evs. [| Says Server B                                                 \
-\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
-\           evs : otway |]                                                \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\           evs : otway |]                                           \
 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
-by (prove_simple_subgoals_tac 1);
-by (Blast_tac 1); 
+by (ALLGOALS Simp_tac);
+by (ALLGOALS Blast_tac);
 qed "Says_Server_message_form";
 
 
@@ -140,7 +139,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);
 
 
@@ -192,12 +191,11 @@
 by (ALLGOALS Clarify_tac);
 (*Remaining cases: OR3 and OR4*)
 by (ex_strip_tac 2);
-by (Blast_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*)
-by (blast_tac (claset() addSEs spies_partsEs
-                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
+by (blast_tac (claset() addSEs spies_partsEs) 1);
 val lemma = result();
 
 goal thy 
@@ -208,37 +206,39 @@
 qed "unique_session_keys";
 
 
-(*Crucial security property, but not itself enough to guarantee correctness!*)
+(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
+    Does not in itself guarantee security: an attack could violate 
+    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;
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong] 
-                            addsimps [analz_insert_eq, analz_insert_freshK]
-                            addsimps (pushes@expand_ifs))));
+                             addsimps [analz_insert_eq, analz_insert_freshK]
+                             addsimps (pushes@expand_ifs))));
 (*Oops*)
 by (blast_tac (claset() addSDs [unique_session_keys]) 4);
 (*OR4*) 
 by (Blast_tac 3);
 (*OR3*)
-by (blast_tac (claset() addSEs spies_partsEs
-                       addIs [impOfSubs analz_subset_parts]) 2);
+by (Blast_tac 2);
 (*Fake*) 
 by (spy_analz_tac 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 goal thy 
- "!!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 |]                \
+ "!!evs. [| Says Server B                                           \
+\            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
+\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
+\           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);
@@ -257,8 +257,7 @@
 \            Says A B {|NA, Agent A, Agent B,                  \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
 by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (Blast_tac 1);
+by (ALLGOALS Blast_tac);
 qed_spec_mp "Crypt_imp_OR1";
 
 
@@ -277,16 +276,15 @@
 \                   Crypt (shrK A) {|NA, Key K|},                    \
 \                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
 by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+(*Fake*)
+by (Blast_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
-by (blast_tac (claset() addSIs [parts_insertI]
-                       addSEs spies_partsEs) 1);
+by (Blast_tac 1);
 (*OR3 and OR4*)
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
 by (ALLGOALS Clarify_tac);
 (*OR4*)
-by (blast_tac (claset() addSIs [Crypt_imp_OR1]
-                       addEs  spies_partsEs) 2);
+by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
 (*OR3*)  (** LEVEL 5 **)
 (*The hypotheses at this point suggest an attack in which nonce NB is used
   in two different roles: