src/HOL/Auth/NS_Shared.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4831 dae4d63a1318
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -258,7 +258,7 @@
     1.4  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
     1.5  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
     1.6  \             : set evs -->                                            \
     1.7 -\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
     1.8 +\        (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) -->          \
     1.9  \        Key K ~: analz (spies evs)";
    1.10  by (etac ns_shared.induct 1);
    1.11  by analz_spies_tac;
    1.12 @@ -288,7 +288,7 @@
    1.13  goal thy 
    1.14   "!!evs. [| Says Server A                                        \
    1.15  \              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
    1.16 -\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;     \
    1.17 +\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
    1.18  \           A ~: bad;  B ~: bad;  evs : ns_shared                \
    1.19  \        |] ==> Key K ~: analz (spies evs)";
    1.20  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.21 @@ -345,7 +345,7 @@
    1.22  goal thy
    1.23   "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
    1.24  \           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    1.25 -\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
    1.26 +\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
    1.27  \           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
    1.28  \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
    1.29  by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
    1.30 @@ -415,7 +415,7 @@
    1.31   "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
    1.32  \           Says B A (Crypt K (Nonce NB))  : set evs;                \
    1.33  \           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
    1.34 -\           ALL NA NB. Says A Spy {|NA, NB, Key K|} ~: set evs;      \
    1.35 +\           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
    1.36  \           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \
    1.37  \        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
    1.38  by (dtac B_trusts_NS3 1);