src/HOL/Auth/OtwayRees.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -60,15 +60,10 @@
     1.4  qed "OR4_analz_spies";
     1.5  
     1.6  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
     1.7 -\                 ==> K : parts (spies evs)";
     1.8 +\                ==> K : parts (spies evs)";
     1.9  by (Blast_tac 1);
    1.10  qed "Oops_parts_spies";
    1.11  
    1.12 -(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.13 -  argument as for the Fake case.  This is possible for most, but not all,
    1.14 -  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.15 -  messages originate from the Spy. *)
    1.16 -
    1.17  bind_thm ("OR2_parts_spies",
    1.18            OR2_analz_spies RS (impOfSubs analz_subset_parts));
    1.19  bind_thm ("OR4_parts_spies",
    1.20 @@ -86,8 +81,7 @@
    1.21  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.22      sends messages containing X! **)
    1.23  
    1.24 -
    1.25 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.26 +(*Spy never sees a good agent's shared key!*)
    1.27  goal thy 
    1.28   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.29  by (parts_induct_tac 1);
    1.30 @@ -111,6 +105,7 @@
    1.31  by (parts_induct_tac 1);
    1.32  (*Fake*)
    1.33  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    1.34 +(*OR2, OR3*)
    1.35  by (ALLGOALS Blast_tac);
    1.36  qed_spec_mp "new_keys_not_used";
    1.37  
    1.38 @@ -141,8 +136,7 @@
    1.39  val analz_spies_tac = 
    1.40      dtac OR2_analz_spies 4 THEN 
    1.41      dtac OR4_analz_spies 6 THEN
    1.42 -    forward_tac [Says_Server_message_form] 7 THEN
    1.43 -    assume_tac 7 THEN
    1.44 +    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
    1.45      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    1.46  
    1.47  
    1.48 @@ -194,7 +188,7 @@
    1.49  by (ALLGOALS Clarify_tac);
    1.50  (*Remaining cases: OR3 and OR4*)
    1.51  by (ex_strip_tac 2);
    1.52 -by (Best_tac 2);
    1.53 +by (Best_tac 2);	(*Blast_tac's too slow (in reconstruction)*)
    1.54  by (expand_case_tac "K = ?y" 1);
    1.55  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.56  (*...we assume X is a recent message, and handle this case by contradiction*)
    1.57 @@ -315,11 +309,11 @@
    1.58      the premises, e.g. by having A=Spy **)
    1.59  
    1.60  goal thy 
    1.61 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
    1.62 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
    1.63  \        ==> Says Server B                                            \
    1.64  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
    1.65  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
    1.66 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
    1.67 +\            Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
    1.68  \            Key K ~: analz (spies evs)";
    1.69  by (etac otway.induct 1);
    1.70  by analz_spies_tac;
    1.71 @@ -341,8 +335,8 @@
    1.72   "!!evs. [| Says Server B                                           \
    1.73  \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
    1.74  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
    1.75 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    1.76 -\           A ~: bad;  B ~: bad;  evs : otway |]                  \
    1.77 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    1.78 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
    1.79  \        ==> Key K ~: analz (spies evs)";
    1.80  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.81  by (blast_tac (claset() addSEs [lemma]) 1);