src/HOL/Auth/OtwayRees_AN.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -58,10 +58,6 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Oops_parts_spies";
     1.6  
     1.7 -(*OR4_analz_spies lets us treat those cases using the same 
     1.8 -  argument as for the Fake case.  This is possible for most, but not all,
     1.9 -  proofs, since Fake messages originate from the Spy. *)
    1.10 -
    1.11  bind_thm ("OR4_parts_spies",
    1.12            OR4_analz_spies RS (impOfSubs analz_subset_parts));
    1.13  
    1.14 @@ -76,7 +72,7 @@
    1.15  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.16      sends messages containing X! **)
    1.17  
    1.18 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.19 +(*Spy never sees a good agent's shared key!*)
    1.20  goal thy 
    1.21   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.22  by (parts_induct_tac 1);
    1.23 @@ -248,12 +244,12 @@
    1.24      the premises, e.g. by having A=Spy **)
    1.25  
    1.26  goal thy 
    1.27 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                 \
    1.28 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                   \
    1.29  \        ==> Says Server B                                         \
    1.30  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.31  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.32  \            : set evs -->                                         \
    1.33 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    1.34 +\            Notes Spy {|NA, NB, Key K|} ~: set evs -->            \
    1.35  \            Key K ~: analz (spies evs)";
    1.36  by (etac otway.induct 1);
    1.37  by analz_spies_tac;
    1.38 @@ -276,8 +272,8 @@
    1.39  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.40  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.41  \             : set evs;                                            \
    1.42 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    1.43 -\           A ~: bad;  B ~: bad;  evs : otway |]                  \
    1.44 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    1.45 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
    1.46  \        ==> Key K ~: analz (spies evs)";
    1.47  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.48  by (blast_tac (claset() addSEs [lemma]) 1);