src/HOL/Auth/Yahalom2.thy
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 3432 04412cfe6861
equal deleted inserted replaced
2515:6ff9bd353121 2516:4d68fbe6378b
    28     Fake "[| evs: yahalom lost;  B ~= Spy;  
    28     Fake "[| evs: yahalom lost;  B ~= Spy;  
    29              X: synth (analz (sees lost Spy evs)) |]
    29              X: synth (analz (sees lost Spy evs)) |]
    30           ==> Says Spy B X  # evs : yahalom lost"
    30           ==> Says Spy B X  # evs : yahalom lost"
    31 
    31 
    32          (*Alice initiates a protocol run*)
    32          (*Alice initiates a protocol run*)
    33     YM1  "[| evs: yahalom lost;  A ~= B |]
    33     YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
    34           ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost"
    34           ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
    35 
    35 
    36          (*Bob's response to Alice's message.  Bob doesn't know who 
    36          (*Bob's response to Alice's message.  Bob doesn't know who 
    37 	   the sender is, hence the A' in the sender field.*)
    37 	   the sender is, hence the A' in the sender field.*)
    38     YM2  "[| evs: yahalom lost;  B ~= Server;
    38     YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
    39              Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    39              Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    40           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|}
    40           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs
    41                  # evs : yahalom lost"
    41                 : yahalom lost"
    42 
    42 
    43          (*The Server receives Bob's message.  He responds by sending a
    43          (*The Server receives Bob's message.  He responds by sending a
    44            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.
    45            Fields are reversed in the 2nd packet to prevent attacks.*)
    45            Fields are reversed in the 2nd packet to prevent attacks.*)
    46     YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;
    46     YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    47              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    47              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    48                : set_of_list evs |]
    48                : set_of_list evs |]
    49           ==> Says Server A
    49           ==> Says Server A
    50                {|Nonce NB, 
    50                {|Nonce NB, 
    51                  Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|},
    51                  Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    52                  Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|}
    52                  Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
    53                  # evs : yahalom lost"
    53                  # evs : yahalom lost"
    54 
    54 
    55          (*Alice receives the Server's (?) message, checks her Nonce, and
    55          (*Alice receives the Server's (?) message, checks her Nonce, and
    56            uses the new session key to send Bob his Nonce.*)
    56            uses the new session key to send Bob his Nonce.*)
    57     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    57     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;