src/HOL/Auth/Yahalom2.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -209,7 +209,7 @@
     1.4  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
     1.5  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
     1.6  \             : set evs -->                                     \
     1.7 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->        \
     1.8 +\            Notes Spy {|na, nb, Key K|} ~: set evs -->         \
     1.9  \            Key K ~: analz (spies evs)";
    1.10  by (etac yahalom.induct 1);
    1.11  by analz_spies_tac;
    1.12 @@ -235,8 +235,8 @@
    1.13  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
    1.14  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
    1.15  \           : set evs;                                       \
    1.16 -\           Says A Spy {|na, nb, Key K|} ~: set evs;         \
    1.17 -\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
    1.18 +\           Notes Spy {|na, nb, Key K|} ~: set evs;          \
    1.19 +\           A ~: bad;  B ~: bad;  evs : yahalom |]           \
    1.20  \        ==> Key K ~: analz (spies evs)";
    1.21  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.22  by (blast_tac (claset() addSEs [lemma]) 1);
    1.23 @@ -249,8 +249,8 @@
    1.24    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
    1.25  goal thy
    1.26   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
    1.27 -\            : parts (spies evs);                                   \
    1.28 -\           A ~: bad;  evs : yahalom |]                               \
    1.29 +\            : parts (spies evs);                                      \
    1.30 +\           A ~: bad;  evs : yahalom |]                                \
    1.31  \         ==> EX nb. Says Server A                                     \
    1.32  \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
    1.33  \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
    1.34 @@ -384,7 +384,7 @@
    1.35  goal thy 
    1.36   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
    1.37  \                       Crypt K (Nonce NB)|} : set evs;                 \
    1.38 -\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
    1.39 +\           (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
    1.40  \           A ~: bad;  B ~: bad;  evs : yahalom |]                    \
    1.41  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    1.42  by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);