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