28 ==> Says Spy B X # evs : otway lost" |
28 ==> Says Spy B X # evs : otway lost" |
29 |
29 |
30 (*Alice initiates a protocol run*) |
30 (*Alice initiates a protocol run*) |
31 OR1 "[| evs: otway lost; A ~= B; B ~= Server |] |
31 OR1 "[| evs: otway lost; A ~= B; B ~= Server |] |
32 ==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
32 ==> Says A B {|Nonce (newN evs), Agent A, Agent B, |
33 Crypt {|Nonce (newN evs), Agent A, Agent B|} |
33 Crypt (shrK A) |
34 (shrK A) |} |
34 {|Nonce (newN evs), Agent A, Agent B|} |} |
35 # evs : otway lost" |
35 # evs : otway lost" |
36 |
36 |
37 (*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 |
38 the sender is, hence the A' in the sender field. |
38 the sender is, hence the A' in the sender field. |
39 Note that NB is encrypted.*) |
39 Note that NB is encrypted.*) |
40 OR2 "[| evs: otway lost; B ~= Server; |
40 OR2 "[| evs: otway lost; B ~= Server; |
41 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 |] |
42 ==> Says B Server |
42 ==> Says B Server |
43 {|Nonce NA, Agent A, Agent B, X, |
43 {|Nonce NA, Agent A, Agent B, X, |
44 Crypt {|Nonce NA, Nonce (newN evs), |
44 Crypt |
45 Agent A, Agent B|} (shrK B)|} |
45 (shrK B){|Nonce NA, Nonce (newN evs), Agent A, Agent B|}|} |
46 # evs : otway lost" |
46 # evs : otway lost" |
47 |
47 |
48 (*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 |
49 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 |
50 forwarding to Alice.*) |
50 forwarding to Alice.*) |
51 OR3 "[| evs: otway lost; B ~= Server; |
51 OR3 "[| evs: otway lost; B ~= Server; |
52 Says B' Server |
52 Says B' Server |
53 {|Nonce NA, Agent A, Agent B, |
53 {|Nonce NA, Agent A, Agent B, |
54 Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), |
54 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
55 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|} |
55 Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
56 : set_of_list evs |] |
56 : set_of_list evs |] |
57 ==> Says Server B |
57 ==> Says Server B |
58 {|Nonce NA, |
58 {|Nonce NA, |
59 Crypt {|Nonce NA, Key (newK evs)|} (shrK A), |
59 Crypt (shrK A) {|Nonce NA, Key (newK evs)|}, |
60 Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} |
60 Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|} |
61 # evs : otway lost" |
61 # evs : otway lost" |
62 |
62 |
63 (*Bob receives the Server's (?) message and compares the Nonces with |
63 (*Bob receives the Server's (?) message and compares the Nonces with |
64 those in the message he previously sent the Server.*) |
64 those in the message he previously sent the Server.*) |
65 OR4 "[| evs: otway lost; A ~= B; |
65 OR4 "[| evs: otway lost; A ~= B; |
66 Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
66 Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
67 : set_of_list evs; |
67 : set_of_list evs; |
68 Says B Server {|Nonce NA, Agent A, Agent B, X', |
68 Says B Server {|Nonce NA, Agent A, Agent B, X', |
69 Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} |
69 Crypt (shrK B) |
70 (shrK B)|} |
70 {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
71 : set_of_list evs |] |
71 : set_of_list evs |] |
72 ==> Says B A {|Nonce NA, X|} # evs : otway lost" |
72 ==> Says B A {|Nonce NA, X|} # evs : otway lost" |
73 |
73 |
74 (*This message models possible leaks of session keys. The nonces |
74 (*This message models possible leaks of session keys. The nonces |
75 identify the protocol run.*) |
75 identify the protocol run.*) |
76 Oops "[| evs: otway lost; B ~= Spy; |
76 Oops "[| evs: otway lost; B ~= Spy; |
77 Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} |
77 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
78 : set_of_list evs |] |
78 : set_of_list evs |] |
79 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" |
79 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" |
80 |
80 |
81 end |
81 end |