src/HOL/Auth/Yahalom.thy
changeset 2451 ce85a2aafc7a
parent 2378 fc103154ad8f
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Dec 19 11:54:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Dec 19 11:58:39 1996 +0100
     1.3 @@ -27,7 +27,8 @@
     1.4  
     1.5           (*Alice initiates a protocol run*)
     1.6      YM1  "[| evs: yahalom lost;  A ~= B |]
     1.7 -          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
     1.8 +          ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs
     1.9 +                : yahalom 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 @@ -35,7 +36,8 @@
    1.14               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    1.15            ==> Says B Server 
    1.16                    {|Agent B, 
    1.17 -                    Crypt (shrK B) {|Agent A, Nonce NA, Nonce (newN evs)|}|}
    1.18 +                    Crypt (shrK B)
    1.19 +                      {|Agent A, Nonce NA, Nonce (newN(length evs))|}|}
    1.20                   # evs : yahalom lost"
    1.21  
    1.22           (*The Server receives Bob's message.  He responds by sending a
    1.23 @@ -45,9 +47,9 @@
    1.24                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    1.25                 : set_of_list evs |]
    1.26            ==> Says Server A
    1.27 -                  {|Crypt (shrK A) {|Agent B, Key (newK evs), 
    1.28 +                  {|Crypt (shrK A) {|Agent B, Key (newK(length evs)), 
    1.29                              Nonce NA, Nonce NB|},
    1.30 -                    Crypt (shrK B) {|Agent A, Key (newK evs)|}|}
    1.31 +                    Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|}
    1.32                   # evs : yahalom lost"
    1.33  
    1.34           (*Alice receives the Server's (?) message, checks her Nonce, and