src/HOL/Auth/Yahalom.ML
changeset 3543 82f33248d89d
parent 3519 ab0a9fbed4c0
child 3674 65ec38fbb265
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Jul 22 11:23:03 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Jul 22 11:26:02 1997 +0200
     1.3 @@ -278,8 +278,8 @@
     1.4  (*B knows, by the first part of A's message, that the Server distributed 
     1.5    the key for A and B.  But this part says nothing about nonces.*)
     1.6  goal thy 
     1.7 - "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
     1.8 -\           B ~: lost;  evs : yahalom |]                           \
     1.9 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs);   \
    1.10 +\           B ~: lost;  evs : yahalom |]                                \
    1.11  \        ==> EX NA NB. Says Server A                                    \
    1.12  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
    1.13  \                                           Nonce NA, Nonce NB|},       \
    1.14 @@ -299,10 +299,10 @@
    1.15   "!!evs. evs : yahalom                                             \
    1.16  \        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
    1.17  \            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
    1.18 -\            (EX A B NA. Says Server A                                  \
    1.19 -\                        {|Crypt (shrK A) {|Agent B, Key K,             \
    1.20 -\                                  Nonce NA, Nonce NB|},                \
    1.21 -\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
    1.22 +\            (EX A B NA. Says Server A                             \
    1.23 +\                        {|Crypt (shrK A) {|Agent B, Key K,        \
    1.24 +\                                  Nonce NA, Nonce NB|},           \
    1.25 +\                          Crypt (shrK B) {|Agent A, Key K|}|}     \
    1.26  \                       : set evs)";
    1.27  by (parts_induct_tac 1);
    1.28  (*YM3 & Fake*)