59 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
59 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
60 # evs : otway" |
60 # evs : otway" |
61 |
61 |
62 (*Bob receives the Server's (?) message and compares the Nonces with |
62 (*Bob receives the Server's (?) message and compares the Nonces with |
63 those in the message he previously sent the Server.*) |
63 those in the message he previously sent the Server.*) |
64 OR4 "[| evs: otway; A ~= B; B ~= Server; |
64 OR4 "[| evs: otway; A ~= B; |
65 Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
65 Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
66 : set_of_list evs; |
66 : set_of_list evs; |
67 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} |
67 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} |
68 : set_of_list evs |] |
68 : set_of_list evs |] |
69 ==> Says B A {|Nonce NA, X|} # evs : otway" |
69 ==> Says B A {|Nonce NA, X|} # evs : otway" |
70 |
70 |
71 (*This message models possible leaks of session keys. Alice's Nonce |
71 (*This message models possible leaks of session keys. The nonces |
72 identifies the protocol run.*) |
72 identify the protocol run.*) |
73 Revl "[| evs: otway; A ~= Spy; |
73 Oops "[| evs: otway; B ~= Spy; |
74 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
74 Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
75 : set_of_list evs; |
|
76 Says A B {|Nonce NA, Agent A, Agent B, |
|
77 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} |
|
78 : set_of_list evs |] |
75 : set_of_list evs |] |
79 ==> Says A Spy {|Nonce NA, Key K|} # evs : otway" |
76 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway" |
80 |
77 |
81 end |
78 end |