src/HOL/Auth/OtwayRees_AN.thy
changeset 2451 ce85a2aafc7a
parent 2378 fc103154ad8f
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Dec 19 11:54:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Dec 19 11:58:39 1996 +0100
     1.3 @@ -29,14 +29,15 @@
     1.4  
     1.5           (*Alice initiates a protocol run*)
     1.6      OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
     1.7 -          ==> Says A B {|Agent A, Agent B, Nonce (newN evs)|}
     1.8 +          ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|}
     1.9                   # evs : otway lost"
    1.10  
    1.11           (*Bob's response to Alice's message.  Bob doesn't know who 
    1.12  	   the sender is, hence the A' in the sender field.*)
    1.13      OR2  "[| evs: otway lost;  B ~= Server;
    1.14               Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    1.15 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
    1.16 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, 
    1.17 +                              Nonce (newN(length evs))|}
    1.18                   # evs : otway lost"
    1.19  
    1.20           (*The Server receives Bob's message.  Then he sends a new
    1.21 @@ -45,8 +46,10 @@
    1.22               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    1.23                 : set_of_list evs |]
    1.24            ==> Says Server B 
    1.25 -               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
    1.26 -                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
    1.27 +               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, 
    1.28 +                                  Key(newK(length evs))|},
    1.29 +                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 
    1.30 +                                  Key(newK(length evs))|}|}
    1.31                # evs : otway lost"
    1.32  
    1.33           (*Bob receives the Server's (?) message and compares the Nonces with