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