src/HOL/Auth/OtwayRees_AN.ML
changeset 3543 82f33248d89d
parent 3519 ab0a9fbed4c0
child 3674 65ec38fbb265
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Jul 22 11:23:03 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Jul 22 11:26:02 1997 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  (*A "possibility property": there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
     1.7 -\        ==> EX K. EX NA. EX evs: otway.                                 \
     1.8 +\        ==> EX K. EX NA. EX evs: otway.                                      \
     1.9  \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    1.10  \             : set evs";
    1.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.12 @@ -125,7 +125,7 @@
    1.13  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.14  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.15  \             : set evs;                                            \
    1.16 -\           evs : otway |]                                     \
    1.17 +\           evs : otway |]                                          \
    1.18  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.19  by (etac rev_mp 1);
    1.20  by (etac otway.induct 1);
    1.21 @@ -183,9 +183,9 @@
    1.22  (*** The Key K uniquely identifies the Server's  message. **)
    1.23  
    1.24  goal thy 
    1.25 - "!!evs. evs : otway ==>                                   \
    1.26 -\      EX A' B' NA' NB'. ALL A B NA NB.                    \
    1.27 -\       Says Server B                                      \
    1.28 + "!!evs. evs : otway ==>                                            \
    1.29 +\      EX A' B' NA' NB'. ALL A B NA NB.                             \
    1.30 +\       Says Server B                                               \
    1.31  \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
    1.32  \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    1.33  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    1.34 @@ -258,12 +258,12 @@
    1.35      the premises, e.g. by having A=Spy **)
    1.36  
    1.37  goal thy 
    1.38 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                         \
    1.39 -\        ==> Says Server B                                                 \
    1.40 -\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    1.41 -\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    1.42 -\            : set evs -->                                                 \
    1.43 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
    1.44 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                 \
    1.45 +\        ==> Says Server B                                         \
    1.46 +\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.47 +\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.48 +\            : set evs -->                                         \
    1.49 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    1.50  \            Key K ~: analz (sees Spy evs)";
    1.51  by (etac otway.induct 1);
    1.52  by analz_sees_tac;