12 Proc. Royal Soc. 426 (1989) |
12 Proc. Royal Soc. 426 (1989) |
13 *) |
13 *) |
14 |
14 |
15 OtwayRees = Shared + |
15 OtwayRees = Shared + |
16 |
16 |
17 consts otway :: "event list set" |
17 consts otway :: "agent set => event list set" |
18 inductive otway |
18 inductive "otway lost" |
19 intrs |
19 intrs |
20 (*Initial trace is empty*) |
20 (*Initial trace is empty*) |
21 Nil "[]: otway" |
21 Nil "[]: otway lost" |
22 |
22 |
23 (*The enemy MAY say anything he CAN say. We do not expect him to |
23 (*The spy MAY say anything he CAN say. We do not expect him to |
24 invent new nonces here, but he can also use NS1. Common to |
24 invent new nonces here, but he can also use NS1. Common to |
25 all similar protocols.*) |
25 all similar protocols.*) |
26 Fake "[| evs: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) |] |
26 Fake "[| evs: otway lost; B ~= Spy; |
27 ==> Says Enemy B X # evs : otway" |
27 X: synth (analz (sees lost Spy evs)) |] |
|
28 ==> Says Spy B X # evs : otway lost" |
28 |
29 |
29 (*Alice initiates a protocol run*) |
30 (*Alice initiates a protocol run*) |
30 OR1 "[| evs: otway; A ~= B; B ~= Server |] |
31 OR1 "[| evs: otway lost; A ~= B; B ~= Server |] |
31 ==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
32 ==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
32 Crypt {|Nonce (newN evs), Agent A, Agent B|} |
33 Crypt {|Nonce (newN evs), Agent A, Agent B|} |
33 (shrK A) |} |
34 (shrK A) |} |
34 # evs : otway" |
35 # evs : otway lost" |
35 |
36 |
36 (*Bob's response to Alice's message. Bob doesn't know who |
37 (*Bob's response to Alice's message. Bob doesn't know who |
37 the sender is, hence the A' in the sender field. |
38 the sender is, hence the A' in the sender field. |
38 We modify the published protocol by NOT encrypting NB.*) |
39 We modify the published protocol by NOT encrypting NB.*) |
39 OR2 "[| evs: otway; B ~= Server; |
40 OR2 "[| evs: otway lost; B ~= Server; |
40 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
41 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
41 ==> Says B Server |
42 ==> Says B Server |
42 {|Nonce NA, Agent A, Agent B, X, |
43 {|Nonce NA, Agent A, Agent B, X, |
43 Crypt {|Nonce NA, Nonce (newN evs), |
44 Crypt {|Nonce NA, Nonce (newN evs), |
44 Agent A, Agent B|} (shrK B)|} |
45 Agent A, Agent B|} (shrK B)|} |
45 # evs : otway" |
46 # evs : otway lost" |
46 |
47 |
47 (*The Server receives Bob's message and checks that the three NAs |
48 (*The Server receives Bob's message and checks that the three NAs |
48 match. Then he sends a new session key to Bob with a packet for |
49 match. Then he sends a new session key to Bob with a packet for |
49 forwarding to Alice.*) |
50 forwarding to Alice.*) |
50 OR3 "[| evs: otway; B ~= Server; |
51 OR3 "[| evs: otway lost; B ~= Server; |
51 Says B' Server |
52 Says B' Server |
52 {|Nonce NA, Agent A, Agent B, |
53 {|Nonce NA, Agent A, Agent B, |
53 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
54 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
54 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|} |
55 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|} |
55 : set_of_list evs |] |
56 : set_of_list evs |] |
56 ==> Says Server B |
57 ==> Says Server B |
57 {|Nonce NA, |
58 {|Nonce NA, |
58 Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
59 Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
59 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
60 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
60 # evs : otway" |
61 # evs : otway lost" |
61 |
62 |
62 (*Bob receives the Server's (?) message and compares the Nonces with |
63 (*Bob receives the Server's (?) message and compares the Nonces with |
63 those in the message he previously sent the Server.*) |
64 those in the message he previously sent the Server.*) |
64 OR4 "[| evs: otway; A ~= B; B ~= Server; |
65 OR4 "[| evs: otway lost; A ~= B; B ~= Server; |
65 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)|} |
66 : set_of_list evs; |
67 : set_of_list evs; |
67 Says B Server {|Nonce NA, Agent A, Agent B, X', |
68 Says B Server {|Nonce NA, Agent A, Agent B, X', |
68 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} |
69 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} |
69 (shrK B)|} |
70 (shrK B)|} |
70 : set_of_list evs |] |
71 : set_of_list evs |] |
71 ==> Says B A {|Nonce NA, X|} # evs : otway" |
72 ==> Says B A {|Nonce NA, X|} # evs : otway lost" |
72 |
73 |
73 (*This message models possible leaks of session keys. Alice's Nonce |
74 (*This message models possible leaks of session keys. Alice's Nonce |
74 identifies the protocol run.*) |
75 identifies the protocol run.*) |
75 Reveal "[| evs: otway; A ~= Enemy; |
76 Reveal "[| evs: otway lost; A ~= Spy; |
76 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
77 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
77 : set_of_list evs; |
78 : set_of_list evs; |
78 Says A B {|Nonce NA, Agent A, Agent B, |
79 Says A B {|Nonce NA, Agent A, Agent B, |
79 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} |
80 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} |
80 : set_of_list evs |] |
81 : set_of_list evs |] |
81 ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway" |
82 ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost" |
82 |
83 |
83 end |
84 end |