src/HOL/Auth/OtwayRees_Bad.thy
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 2837 dee1c7f1f576
     1.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -27,26 +27,25 @@
     1.4            ==> Says Spy B X  # evs : otway"
     1.5  
     1.6           (*Alice initiates a protocol run*)
     1.7 -    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
     1.8 -          ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B, 
     1.9 -                         Crypt (shrK A) 
    1.10 -                            {|Nonce (newN(length evs)), Agent A, Agent B|} |} 
    1.11 +    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
    1.12 +          ==> Says A B {|Nonce NA, Agent A, Agent B, 
    1.13 +                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
    1.14                   # evs : otway"
    1.15  
    1.16           (*Bob's response to Alice's message.  Bob doesn't know who 
    1.17  	   the sender is, hence the A' in the sender field.
    1.18             We modify the published protocol by NOT encrypting NB.*)
    1.19 -    OR2  "[| evs: otway;  B ~= Server;
    1.20 +    OR2  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
    1.21               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    1.22            ==> Says B Server 
    1.23 -                  {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)), 
    1.24 +                  {|Nonce NA, Agent A, Agent B, X, Nonce NB,
    1.25                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    1.26                   # evs : otway"
    1.27  
    1.28           (*The Server receives Bob's message and checks that the three NAs
    1.29             match.  Then he sends a new session key to Bob with a packet for
    1.30             forwarding to Alice.*)
    1.31 -    OR3  "[| evs: otway;  B ~= Server;
    1.32 +    OR3  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
    1.33               Says B' Server 
    1.34                    {|Nonce NA, Agent A, Agent B, 
    1.35                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    1.36 @@ -55,16 +54,16 @@
    1.37                 : set_of_list evs |]
    1.38            ==> Says Server B 
    1.39                    {|Nonce NA, 
    1.40 -                    Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
    1.41 -                    Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
    1.42 +                    Crypt (shrK A) {|Nonce NA, Key KAB|},
    1.43 +                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
    1.44                   # evs : otway"
    1.45  
    1.46           (*Bob receives the Server's (?) message and compares the Nonces with
    1.47  	   those in the message he previously sent the Server.*)
    1.48      OR4  "[| evs: otway;  A ~= B;
    1.49 -             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    1.50 +             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    1.51                 : set_of_list evs;
    1.52 -             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    1.53 +             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    1.54                 : set_of_list evs |]
    1.55            ==> Says B A {|Nonce NA, X|} # evs : otway"
    1.56