src/HOL/Auth/OtwayRees_AN.thy
changeset 2451 ce85a2aafc7a
parent 2378 fc103154ad8f
child 2516 4d68fbe6378b
equal deleted inserted replaced
2450:3ad2493fa0e0 2451:ce85a2aafc7a
    27              X: synth (analz (sees lost Spy evs)) |]
    27              X: synth (analz (sees lost Spy evs)) |]
    28           ==> Says Spy B X  # evs : otway lost"
    28           ==> Says Spy B X  # evs : otway lost"
    29 
    29 
    30          (*Alice initiates a protocol run*)
    30          (*Alice initiates a protocol run*)
    31     OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
    31     OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
    32           ==> Says A B {|Agent A, Agent B, Nonce (newN evs)|}
    32           ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|}
    33                  # evs : otway lost"
    33                  # evs : otway lost"
    34 
    34 
    35          (*Bob's response to Alice's message.  Bob doesn't know who 
    35          (*Bob's response to Alice's message.  Bob doesn't know who 
    36 	   the sender is, hence the A' in the sender field.*)
    36 	   the sender is, hence the A' in the sender field.*)
    37     OR2  "[| evs: otway lost;  B ~= Server;
    37     OR2  "[| evs: otway lost;  B ~= Server;
    38              Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    38              Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    39           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
    39           ==> Says B Server {|Agent A, Agent B, Nonce NA, 
       
    40                               Nonce (newN(length evs))|}
    40                  # evs : otway lost"
    41                  # evs : otway lost"
    41 
    42 
    42          (*The Server receives Bob's message.  Then he sends a new
    43          (*The Server receives Bob's message.  Then he sends a new
    43            session key to Bob with a packet for forwarding to Alice.*)
    44            session key to Bob with a packet for forwarding to Alice.*)
    44     OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;
    45     OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;
    45              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    46              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    46                : set_of_list evs |]
    47                : set_of_list evs |]
    47           ==> Says Server B 
    48           ==> Says Server B 
    48                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
    49                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, 
    49                  Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
    50                                   Key(newK(length evs))|},
       
    51                  Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 
       
    52                                   Key(newK(length evs))|}|}
    50               # evs : otway lost"
    53               # evs : otway lost"
    51 
    54 
    52          (*Bob receives the Server's (?) message and compares the Nonces with
    55          (*Bob receives the Server's (?) message and compares the Nonces with
    53 	   those in the message he previously sent the Server.*)
    56 	   those in the message he previously sent the Server.*)
    54     OR4  "[| evs: otway lost;  A ~= B;
    57     OR4  "[| evs: otway lost;  A ~= B;