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