25 X: synth (analz (sees lost Spy evs)) |] |
25 X: synth (analz (sees lost Spy evs)) |] |
26 ==> Says Spy B X # evs : ns_shared lost" |
26 ==> Says Spy B X # evs : ns_shared lost" |
27 |
27 |
28 (*Alice initiates a protocol run, requesting to talk to any B*) |
28 (*Alice initiates a protocol run, requesting to talk to any B*) |
29 NS1 "[| evs: ns_shared lost; A ~= Server |] |
29 NS1 "[| evs: ns_shared lost; A ~= Server |] |
30 ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs |
30 ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|} |
31 : ns_shared lost" |
31 # evs : ns_shared lost" |
32 |
32 |
33 (*Server's response to Alice's message. |
33 (*Server's response to Alice's message. |
34 !! It may respond more than once to A's request !! |
34 !! It may respond more than once to A's request !! |
35 Server doesn't know who the true sender is, hence the A' in |
35 Server doesn't know who the true sender is, hence the A' in |
36 the sender field.*) |
36 the sender field.*) |
37 NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; |
37 NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server; |
38 Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
38 Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
39 ==> Says Server A (Crypt (shrK A) |
39 ==> Says Server A |
40 {|Nonce NA, Agent B, Key (newK evs), |
40 (Crypt (shrK A) |
41 (Crypt (shrK B) {|Key (newK evs), Agent A|})|}) |
41 {|Nonce NA, Agent B, Key (newK(length evs)), |
|
42 (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) |
42 # evs : ns_shared lost" |
43 # evs : ns_shared lost" |
43 |
44 |
44 (*We can't assume S=Server. Agent A "remembers" her nonce. |
45 (*We can't assume S=Server. Agent A "remembers" her nonce. |
45 Can inductively show A ~= Server*) |
46 Can inductively show A ~= Server*) |
46 NS3 "[| evs: ns_shared lost; A ~= B; |
47 NS3 "[| evs: ns_shared lost; A ~= B; |
51 |
52 |
52 (*Bob's nonce exchange. He does not know who the message came |
53 (*Bob's nonce exchange. He does not know who the message came |
53 from, but responds to A because she is mentioned inside.*) |
54 from, but responds to A because she is mentioned inside.*) |
54 NS4 "[| evs: ns_shared lost; A ~= B; |
55 NS4 "[| evs: ns_shared lost; A ~= B; |
55 Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |] |
56 Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |] |
56 ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost" |
57 ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs |
|
58 : ns_shared lost" |
57 |
59 |
58 (*Alice responds with Nonce NB if she has seen the key before. |
60 (*Alice responds with Nonce NB if she has seen the key before. |
59 Maybe should somehow check Nonce NA again. |
61 Maybe should somehow check Nonce NA again. |
60 We do NOT send NB-1 or similar as the Spy cannot spoof such things. |
62 We do NOT send NB-1 or similar as the Spy cannot spoof such things. |
61 Letting the Spy add or subtract 1 lets him send ALL nonces. |
63 Letting the Spy add or subtract 1 lets him send ALL nonces. |