29 X: synth (analz (sees lost Spy evs)) |] |
29 X: synth (analz (sees lost Spy evs)) |] |
30 ==> Says Spy B X # evs : yahalom lost" |
30 ==> Says Spy B X # evs : yahalom lost" |
31 |
31 |
32 (*Alice initiates a protocol run*) |
32 (*Alice initiates a protocol run*) |
33 YM1 "[| evs: yahalom lost; A ~= B |] |
33 YM1 "[| evs: yahalom lost; A ~= B |] |
34 ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost" |
34 ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost" |
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 YM2 "[| evs: yahalom lost; B ~= Server; |
38 YM2 "[| evs: yahalom lost; B ~= Server; |
39 Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] |
39 Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] |
40 ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|} |
40 ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|} |
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; |
46 YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; |
47 Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
47 Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
48 : set_of_list evs |] |
48 : set_of_list evs |] |
49 ==> Says Server A |
49 ==> Says Server A |
50 {|Nonce NB, |
50 {|Nonce NB, |
51 Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|}, |
51 Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|}, |
52 Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|} |
52 Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|} |
53 # evs : yahalom lost" |
53 # evs : yahalom lost" |
54 |
54 |
55 (*Alice receives the Server's (?) message, checks her Nonce, and |
55 (*Alice receives the Server's (?) message, checks her Nonce, and |
56 uses the new session key to send Bob his Nonce.*) |
56 uses the new session key to send Bob his Nonce.*) |
57 YM4 "[| evs: yahalom lost; A ~= Server; A ~= B; |
57 YM4 "[| evs: yahalom lost; A ~= Server; A ~= B; |