34 |
34 |
35 (*Bob's response to Alice's message. Bob doesn't know who |
35 (*Bob's response to Alice's message. Bob doesn't know who |
36 the sender is, hence the A' in the sender field. |
36 the sender is, hence the A' in the sender field. |
37 We modify the published protocol by NOT encrypting NB.*) |
37 We modify the published protocol by NOT encrypting NB.*) |
38 OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs; |
38 OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs; |
39 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
39 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |] |
40 ==> Says B Server |
40 ==> Says B Server |
41 {|Nonce NA, Agent A, Agent B, X, Nonce NB, |
41 {|Nonce NA, Agent A, Agent B, X, Nonce NB, |
42 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
42 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
43 # evs : otway" |
43 # evs : otway" |
44 |
44 |
49 Says B' Server |
49 Says B' Server |
50 {|Nonce NA, Agent A, Agent B, |
50 {|Nonce NA, Agent A, Agent B, |
51 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
51 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
52 Nonce NB, |
52 Nonce NB, |
53 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
53 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
54 : set_of_list evs |] |
54 : set evs |] |
55 ==> Says Server B |
55 ==> Says Server B |
56 {|Nonce NA, |
56 {|Nonce NA, |
57 Crypt (shrK A) {|Nonce NA, Key KAB|}, |
57 Crypt (shrK A) {|Nonce NA, Key KAB|}, |
58 Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
58 Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
59 # evs : otway" |
59 # evs : otway" |
60 |
60 |
61 (*Bob receives the Server's (?) message and compares the Nonces with |
61 (*Bob receives the Server's (?) message and compares the Nonces with |
62 those in the message he previously sent the Server.*) |
62 those in the message he previously sent the Server.*) |
63 OR4 "[| evs: otway; A ~= B; |
63 OR4 "[| evs: otway; A ~= B; |
64 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} |
64 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} |
65 : set_of_list evs; |
65 : set evs; |
66 Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
66 Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
67 : set_of_list evs |] |
67 : set evs |] |
68 ==> Says B A {|Nonce NA, X|} # evs : otway" |
68 ==> Says B A {|Nonce NA, X|} # evs : otway" |
69 |
69 |
70 (*This message models possible leaks of session keys. The nonces |
70 (*This message models possible leaks of session keys. The nonces |
71 identify the protocol run.*) |
71 identify the protocol run.*) |
72 Oops "[| evs: otway; B ~= Spy; |
72 Oops "[| evs: otway; B ~= Spy; |
73 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
73 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
74 : set_of_list evs |] |
74 : set evs |] |
75 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway" |
75 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway" |
76 |
76 |
77 end |
77 end |