49 Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|} |
49 Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|} |
50 # evs : otway lost" |
50 # evs : otway lost" |
51 |
51 |
52 (*Bob receives the Server's (?) message and compares the Nonces with |
52 (*Bob receives the Server's (?) message and compares the Nonces with |
53 those in the message he previously sent the Server.*) |
53 those in the message he previously sent the Server.*) |
54 OR4 "[| evs: otway lost; A ~= B; B ~= Server; |
54 OR4 "[| evs: otway lost; A ~= B; |
55 Says S B {|X, |
55 Says S B {|X, |
56 Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|} |
56 Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|} |
57 : set_of_list evs; |
57 : set_of_list evs; |
58 Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
58 Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
59 : set_of_list evs |] |
59 : set_of_list evs |] |
60 ==> Says B A X # evs : otway lost" |
60 ==> Says B A X # evs : otway lost" |
61 |
61 |
62 (*This message models possible leaks of session keys. Alice's Nonce |
62 (*This message models possible leaks of session keys. The nonces |
63 identifies the protocol run.*) |
63 identify the protocol run. B is not assumed to know shrK A.*) |
64 Revl "[| evs: otway lost; A ~= Spy; |
64 Oops "[| evs: otway lost; B ~= Spy; |
65 Says B' A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) |
65 Says Server B |
66 : set_of_list evs; |
66 {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A), |
67 Says A B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
67 Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|} |
68 ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost" |
68 : set_of_list evs |] |
|
69 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" |
69 |
70 |
70 end |
71 end |