35 |
35 |
36 (*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 |
37 the sender is, hence the A' in the sender field. |
37 the sender is, hence the A' in the sender field. |
38 Note that NB is encrypted.*) |
38 Note that NB is encrypted.*) |
39 OR2 "[| evs: otway lost; B ~= Server; Nonce NB ~: used evs; |
39 OR2 "[| evs: otway lost; B ~= Server; Nonce NB ~: used evs; |
40 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 evs |] |
41 ==> Says B Server |
41 ==> Says B Server |
42 {|Nonce NA, Agent A, Agent B, X, |
42 {|Nonce NA, Agent A, Agent B, X, |
43 Crypt (shrK B) |
43 Crypt (shrK B) |
44 {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
44 {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
45 # evs : otway lost" |
45 # evs : otway lost" |
50 OR3 "[| evs: otway lost; B ~= Server; Key KAB ~: used evs; |
50 OR3 "[| evs: otway lost; B ~= Server; Key KAB ~: used evs; |
51 Says B' Server |
51 Says B' Server |
52 {|Nonce NA, Agent A, Agent B, |
52 {|Nonce NA, Agent A, Agent B, |
53 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
53 Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
54 Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
54 Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
55 : set_of_list evs |] |
55 : set evs |] |
56 ==> Says Server B |
56 ==> Says Server B |
57 {|Nonce NA, |
57 {|Nonce NA, |
58 Crypt (shrK A) {|Nonce NA, Key KAB|}, |
58 Crypt (shrK A) {|Nonce NA, Key KAB|}, |
59 Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
59 Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
60 # evs : otway lost" |
60 # evs : otway lost" |
63 those in the message he previously sent the Server.*) |
63 those in the message he previously sent the Server.*) |
64 OR4 "[| evs: otway lost; A ~= B; |
64 OR4 "[| evs: otway lost; A ~= B; |
65 Says B Server {|Nonce NA, Agent A, Agent B, X', |
65 Says B Server {|Nonce NA, Agent A, Agent B, X', |
66 Crypt (shrK B) |
66 Crypt (shrK B) |
67 {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
67 {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
68 : set_of_list evs; |
68 : set evs; |
69 Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
69 Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
70 : set_of_list evs |] |
70 : set evs |] |
71 ==> Says B A {|Nonce NA, X|} # evs : otway lost" |
71 ==> Says B A {|Nonce NA, X|} # evs : otway lost" |
72 |
72 |
73 (*This message models possible leaks of session keys. The nonces |
73 (*This message models possible leaks of session keys. The nonces |
74 identify the protocol run.*) |
74 identify the protocol run.*) |
75 Oops "[| evs: otway lost; B ~= Spy; |
75 Oops "[| evs: otway lost; B ~= Spy; |
76 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
76 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
77 : set_of_list evs |] |
77 : set evs |] |
78 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" |
78 ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" |
79 |
79 |
80 end |
80 end |