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