23 all similar protocols.*) |
25 all similar protocols.*) |
24 Fake "[| evs: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) |] |
26 Fake "[| evs: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) |] |
25 ==> Says Enemy B X # evs : otway" |
27 ==> Says Enemy B X # evs : otway" |
26 |
28 |
27 (*Alice initiates a protocol run*) |
29 (*Alice initiates a protocol run*) |
28 OR1 "[| evs: otway; A ~= B |] |
30 OR1 "[| evs: otway; A ~= B; B ~= Server |] |
29 ==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
31 ==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
30 Crypt {|Nonce (newN evs), Agent A, Agent B|} |
32 Crypt {|Nonce (newN evs), Agent A, Agent B|} |
31 (shrK A) |} |
33 (shrK A) |} |
32 # evs : otway" |
34 # evs : otway" |
33 |
35 |
34 (*Bob's response to Alice's message. Bob doesn't know who |
36 (*Bob's response to Alice's message. Bob doesn't know who |
35 the sender is, hence the A' in the sender field. |
37 the sender is, hence the A' in the sender field. |
36 We modify the published protocol by NOT encrypting NB.*) |
38 We modify the published protocol by NOT encrypting NB.*) |
37 OR2 "[| evs: otway; B ~= Server; |
39 OR2 "[| evs: otway; B ~= Server; |
38 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
40 Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
39 ==> Says B Server |
41 ==> Says B Server |
40 {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), |
42 {|Nonce NA, Agent A, Agent B, X, |
41 Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|} |
43 Crypt {|Nonce NA, Nonce (newN evs), |
|
44 Agent A, Agent B|} (shrK B)|} |
42 # evs : otway" |
45 # evs : otway" |
43 |
46 |
44 (*The Server receives Bob's message and checks that the three NAs |
47 (*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 |
48 match. Then he sends a new session key to Bob with a packet for |
46 forwarding to Alice.*) |
49 forwarding to Alice.*) |
47 OR3 "[| evs: otway; B ~= Server; |
50 OR3 "[| evs: otway; B ~= Server; |
48 Says B' Server |
51 Says B' Server |
49 {|Nonce NA, Agent A, Agent B, |
52 {|Nonce NA, Agent A, Agent B, |
50 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
53 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
51 Nonce NB, |
54 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|} |
52 Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|} |
|
53 : set_of_list evs |] |
55 : set_of_list evs |] |
54 ==> Says Server B |
56 ==> Says Server B |
55 {|Nonce NA, |
57 {|Nonce NA, |
56 Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
58 Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
57 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
59 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
58 # evs : otway" |
60 # evs : otway" |
59 |
61 |
60 (*Bob receives the Server's (?) message and compares the Nonces with |
62 (*Bob receives the Server's (?) message and compares the Nonces with |
61 those in the message he previously sent the Server.*) |
63 those in the message he previously sent the Server.*) |
62 OR4 "[| evs: otway; A ~= B; |
64 OR4 "[| evs: otway; A ~= B; B ~= Server; |
63 Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
65 Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
64 : set_of_list evs; |
66 : set_of_list evs; |
65 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} |
67 Says B Server {|Nonce NA, Agent A, Agent B, X', |
|
68 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} |
|
69 (shrK B)|} |
66 : set_of_list evs |] |
70 : set_of_list evs |] |
67 ==> (Says B A {|Nonce NA, X|}) # evs : otway" |
71 ==> Says B A {|Nonce NA, X|} # evs : otway" |
68 |
72 |
69 (*Alice checks her Nonce, then sends a dummy message to Bob, |
73 (*This message models possible leaks of session keys. Alice's Nonce |
70 using the new session key.*) |
74 identifies the protocol run.*) |
71 OR5 "[| evs: otway; |
75 Reveal "[| evs: otway; A ~= Enemy; |
72 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
76 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} |
73 : set_of_list evs; |
77 : set_of_list evs; |
74 Says A B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |] |
78 Says A B {|Nonce NA, Agent A, Agent B, |
75 ==> Says A B (Crypt (Agent A) K) # evs : otway" |
79 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} |
|
80 : set_of_list evs |] |
|
81 ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway" |
76 |
82 |
77 end |
83 end |