17 IEEE Trans. SE 22 (1), 1996 |
17 IEEE Trans. SE 22 (1), 1996 |
18 *) |
18 *) |
19 |
19 |
20 OtwayRees_AN = Shared + |
20 OtwayRees_AN = Shared + |
21 |
21 |
22 consts otway :: agent set => event list set |
22 consts otway :: event list set |
23 inductive "otway lost" |
23 inductive "otway" |
24 intrs |
24 intrs |
25 (*Initial trace is empty*) |
25 (*Initial trace is empty*) |
26 Nil "[]: otway lost" |
26 Nil "[]: otway" |
27 |
27 |
28 (*The spy MAY say anything he CAN say. We do not expect him to |
28 (*The spy MAY say anything he CAN say. We do not expect him to |
29 invent new nonces here, but he can also use NS1. Common to |
29 invent new nonces here, but he can also use NS1. Common to |
30 all similar protocols.*) |
30 all similar protocols.*) |
31 Fake "[| evs: otway lost; B ~= Spy; |
31 Fake "[| evs: otway; B ~= Spy; |
32 X: synth (analz (sees lost Spy evs)) |] |
32 X: synth (analz (sees Spy evs)) |] |
33 ==> Says Spy B X # evs : otway lost" |
33 ==> Says Spy B X # evs : otway" |
34 |
34 |
35 (*Alice initiates a protocol run*) |
35 (*Alice initiates a protocol run*) |
36 OR1 "[| evs: otway lost; A ~= B; B ~= Server |] |
36 OR1 "[| evs: otway; A ~= B; B ~= Server |] |
37 ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost" |
37 ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway" |
38 |
38 |
39 (*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 |
40 the sender is, hence the A' in the sender field.*) |
40 the sender is, hence the A' in the sender field.*) |
41 OR2 "[| evs: otway lost; B ~= Server; |
41 OR2 "[| evs: otway; B ~= Server; |
42 Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |] |
42 Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |] |
43 ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
43 ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
44 # evs : otway lost" |
44 # evs : otway" |
45 |
45 |
46 (*The Server receives Bob's message. Then he sends a new |
46 (*The Server receives Bob's message. Then he sends a new |
47 session key to Bob with a packet for forwarding to Alice.*) |
47 session key to Bob with a packet for forwarding to Alice.*) |
48 OR3 "[| evs: otway lost; B ~= Server; A ~= B; Key KAB ~: used evs; |
48 OR3 "[| evs: otway; B ~= Server; A ~= B; Key KAB ~: used evs; |
49 Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
49 Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
50 : set evs |] |
50 : set evs |] |
51 ==> Says Server B |
51 ==> Says Server B |
52 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|}, |
52 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|}, |
53 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} |
53 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} |
54 # evs : otway lost" |
54 # evs : otway" |
55 |
55 |
56 (*Bob receives the Server's (?) message and compares the Nonces with |
56 (*Bob receives the Server's (?) message and compares the Nonces with |
57 those in the message he previously sent the Server.*) |
57 those in the message he previously sent the Server.*) |
58 OR4 "[| evs: otway lost; A ~= B; |
58 OR4 "[| evs: otway; A ~= B; |
59 Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs; |
59 Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs; |
60 Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} |
60 Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} |
61 : set evs |] |
61 : set evs |] |
62 ==> Says B A X # evs : otway lost" |
62 ==> Says B A X # evs : otway" |
63 |
63 |
64 (*This message models possible leaks of session keys. The nonces |
64 (*This message models possible leaks of session keys. The nonces |
65 identify the protocol run. B is not assumed to know shrK A.*) |
65 identify the protocol run. B is not assumed to know shrK A.*) |
66 Oops "[| evs: otway lost; B ~= Spy; |
66 Oops "[| evs: otway; B ~= Spy; |
67 Says Server B |
67 Says Server B |
68 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, |
68 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, |
69 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|} |
69 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|} |
70 : set evs |] |
70 : set evs |] |
71 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" |
71 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway" |
72 |
72 |
73 end |
73 end |