src/HOL/Auth/OtwayRees_AN.thy
changeset 2284 80ebd1a213fd
parent 2131 3106a99d30a5
child 2378 fc103154ad8f
equal deleted inserted replaced
2283:68829cf138fc 2284:80ebd1a213fd
    43            session key to Bob with a packet for forwarding to Alice.*)
    43            session key to Bob with a packet for forwarding to Alice.*)
    44     OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;
    44     OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;
    45              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    45              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    46                : set_of_list evs |]
    46                : set_of_list evs |]
    47           ==> Says Server B 
    47           ==> Says Server B 
    48                {|Crypt {|Nonce NA, Agent A, Agent B, Key(newK evs)|} (shrK A),
    48                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
    49                  Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|}
    49                  Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
    50               # evs : otway lost"
    50               # evs : otway lost"
    51 
    51 
    52          (*Bob receives the Server's (?) message and compares the Nonces with
    52          (*Bob receives the Server's (?) message and compares the Nonces with
    53 	   those in the message he previously sent the Server.*)
    53 	   those in the message he previously sent the Server.*)
    54     OR4  "[| evs: otway lost;  A ~= B;
    54     OR4  "[| evs: otway lost;  A ~= B;
    55              Says S B {|X, 
    55              Says S B {|X, 
    56                         Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
    56                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    57                : set_of_list evs;
    57                : set_of_list evs;
    58              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    58              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    59                : set_of_list evs |]
    59                : set_of_list evs |]
    60           ==> Says B A X # evs : otway lost"
    60           ==> Says B A X # evs : otway lost"
    61 
    61 
    62          (*This message models possible leaks of session keys.  The nonces
    62          (*This message models possible leaks of session keys.  The nonces
    63            identify the protocol run.  B is not assumed to know shrK A.*)
    63            identify the protocol run.  B is not assumed to know shrK A.*)
    64     Oops "[| evs: otway lost;  B ~= Spy;
    64     Oops "[| evs: otway lost;  B ~= Spy;
    65              Says Server B 
    65              Says Server B 
    66                       {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A), 
    66                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
    67                         Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
    67                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    68                : set_of_list evs |]
    68                : set_of_list evs |]
    69           ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    69           ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    70 
    70 
    71 end
    71 end