33 ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost" |
33 ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost" |
34 |
34 |
35 (*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 |
36 the sender is, hence the A' in the sender field.*) |
36 the sender is, hence the A' in the sender field.*) |
37 YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs; |
37 YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs; |
38 Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] |
38 Says A' B {|Agent A, Nonce NA|} : set evs |] |
39 ==> Says B Server |
39 ==> Says B Server |
40 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
40 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
41 # evs : yahalom lost" |
41 # evs : yahalom lost" |
42 |
42 |
43 (*The Server receives Bob's message. He responds by sending a |
43 (*The Server receives Bob's message. He responds by sending a |
44 new session key to Alice, with a packet for forwarding to Bob. |
44 new session key to Alice, with a packet for forwarding to Bob. |
45 !! Fields are reversed in the 2nd packet to prevent attacks!! *) |
45 !! Fields are reversed in the 2nd packet to prevent attacks!! *) |
46 YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs; |
46 YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs; |
47 Says B' Server {|Agent B, Nonce NB, |
47 Says B' Server {|Agent B, Nonce NB, |
48 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
48 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
49 : set_of_list evs |] |
49 : set evs |] |
50 ==> Says Server A |
50 ==> Says Server A |
51 {|Nonce NB, |
51 {|Nonce NB, |
52 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|}, |
52 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|}, |
53 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} |
53 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} |
54 # evs : yahalom lost" |
54 # evs : yahalom lost" |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
57 uses the new session key to send Bob his Nonce.*) |
57 uses the new session key to send Bob his Nonce.*) |
58 YM4 "[| evs: yahalom lost; A ~= Server; A ~= B; |
58 YM4 "[| evs: yahalom lost; A ~= Server; A ~= B; |
59 Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
59 Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
60 X|} |
60 X|} |
61 : set_of_list evs; |
61 : set evs; |
62 Says A B {|Agent A, Nonce NA|} : set_of_list evs |] |
62 Says A B {|Agent A, Nonce NA|} : set evs |] |
63 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost" |
63 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost" |
64 |
64 |
65 (*This message models possible leaks of session keys. The nonces |
65 (*This message models possible leaks of session keys. The nonces |
66 identify the protocol run. Quoting Server here ensures they are |
66 identify the protocol run. Quoting Server here ensures they are |
67 correct. *) |
67 correct. *) |
68 Oops "[| evs: yahalom lost; A ~= Spy; |
68 Oops "[| evs: yahalom lost; A ~= Spy; |
69 Says Server A {|Nonce NB, |
69 Says Server A {|Nonce NB, |
70 Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
70 Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
71 X|} : set_of_list evs |] |
71 X|} : set evs |] |
72 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" |
72 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" |
73 |
73 |
74 end |
74 end |