20 Nil "[]: otway" |
20 Nil "[]: otway" |
21 |
21 |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
23 invent new nonces here, but he can also use NS1. Common to |
23 invent new nonces here, but he can also use NS1. Common to |
24 all similar protocols.*) |
24 all similar protocols.*) |
25 Fake "[| evs: otway; X: synth (analz (spies evs)) |] |
25 Fake "[| evs: otway; X: synth (analz (knows Spy evs)) |] |
26 ==> Says Spy B X # evs : otway" |
26 ==> Says Spy B X # evs : otway" |
|
27 |
|
28 (*A message that has been sent can be received by the |
|
29 intended recipient.*) |
|
30 Reception "[| evsr: otway; Says A B X : set evsr |] |
|
31 ==> Gets B X # evsr : otway" |
27 |
32 |
28 (*Alice initiates a protocol run*) |
33 (*Alice initiates a protocol run*) |
29 OR1 "[| evs1: otway; Nonce NA ~: used evs1 |] |
34 OR1 "[| evs1: otway; Nonce NA ~: used evs1 |] |
30 ==> Says A B {|Nonce NA, Agent A, Agent B, |
35 ==> Says A B {|Nonce NA, Agent A, Agent B, |
31 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} |
36 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} |
33 |
38 |
34 (*Bob's response to Alice's message. Bob doesn't know who |
39 (*Bob's response to Alice's message. Bob doesn't know who |
35 the sender is, hence the A' in the sender field. |
40 the sender is, hence the A' in the sender field. |
36 We modify the published protocol by NOT encrypting NB.*) |
41 We modify the published protocol by NOT encrypting NB.*) |
37 OR2 "[| evs2: otway; Nonce NB ~: used evs2; |
42 OR2 "[| evs2: otway; Nonce NB ~: used evs2; |
38 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] |
43 Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] |
39 ==> Says B Server |
44 ==> Says B Server |
40 {|Nonce NA, Agent A, Agent B, X, Nonce NB, |
45 {|Nonce NA, Agent A, Agent B, X, Nonce NB, |
41 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
46 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
42 # evs2 : otway" |
47 # evs2 : otway" |
43 |
48 |
44 (*The Server receives Bob's message and checks that the three NAs |
49 (*The Server receives Bob's message and checks that the three NAs |
45 match. Then he sends a new session key to Bob with a packet for |
50 match. Then he sends a new session key to Bob with a packet for |
46 forwarding to Alice.*) |
51 forwarding to Alice.*) |
47 OR3 "[| evs3: otway; Key KAB ~: used evs3; |
52 OR3 "[| evs3: otway; Key KAB ~: used evs3; |
48 Says B' Server |
53 Gets Server |
49 {|Nonce NA, Agent A, Agent B, |
54 {|Nonce NA, Agent A, Agent B, |
50 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
55 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
51 Nonce NB, |
56 Nonce NB, |
52 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
57 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
53 : set evs3 |] |
58 : set evs3 |] |
58 # evs3 : otway" |
63 # evs3 : otway" |
59 |
64 |
60 (*Bob receives the Server's (?) message and compares the Nonces with |
65 (*Bob receives the Server's (?) message and compares the Nonces with |
61 those in the message he previously sent the Server. |
66 those in the message he previously sent the Server. |
62 Need B ~= Server because we allow messages to self.*) |
67 Need B ~= Server because we allow messages to self.*) |
63 OR4 "[| evs4: otway; A ~= B; B ~= Server; |
68 OR4 "[| evs4: otway; B ~= Server; |
64 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, |
69 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, |
65 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
70 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
66 : set evs4; |
71 : set evs4; |
67 Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
72 Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
68 : set evs4 |] |
73 : set evs4 |] |
69 ==> Says B A {|Nonce NA, X|} # evs4 : otway" |
74 ==> Says B A {|Nonce NA, X|} # evs4 : otway" |
70 |
75 |
71 (*This message models possible leaks of session keys. The nonces |
76 (*This message models possible leaks of session keys. The nonces |
72 identify the protocol run.*) |
77 identify the protocol run.*) |