24 Fake "[| evs: ns_shared lost; B ~= Spy; |
24 Fake "[| evs: ns_shared lost; B ~= Spy; |
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; Nonce NA ~: used evs |] |
30 ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|} |
30 ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs |
31 # evs : ns_shared lost" |
31 : 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; Key KAB ~: used evs; |
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 |
39 ==> Says Server A |
40 (Crypt (shrK A) |
40 (Crypt (shrK A) |
41 {|Nonce NA, Agent B, Key (newK(length evs)), |
41 {|Nonce NA, Agent B, Key KAB, |
42 (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) |
42 (Crypt (shrK B) {|Key KAB, Agent A|})|}) |
43 # evs : ns_shared lost" |
43 # evs : ns_shared lost" |
44 |
44 |
45 (*We can't assume S=Server. Agent A "remembers" her nonce. |
45 (*We can't assume S=Server. Agent A "remembers" her nonce. |
46 Can inductively show A ~= Server*) |
46 Can inductively show A ~= Server*) |
47 NS3 "[| evs: ns_shared lost; A ~= B; |
47 NS3 "[| evs: ns_shared lost; A ~= B; |
50 Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
50 Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] |
51 ==> Says A B X # evs : ns_shared lost" |
51 ==> Says A B X # evs : ns_shared lost" |
52 |
52 |
53 (*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 |
54 from, but responds to A because she is mentioned inside.*) |
54 from, but responds to A because she is mentioned inside.*) |
55 NS4 "[| evs: ns_shared lost; A ~= B; |
55 NS4 "[| evs: ns_shared lost; A ~= B; Nonce NB ~: used evs; |
56 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 |] |
57 ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs |
57 ==> Says B A (Crypt K (Nonce NB)) # evs |
58 : ns_shared lost" |
58 : ns_shared lost" |
59 |
59 |
60 (*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. |
61 Maybe should somehow check Nonce NA again. |
61 Maybe should somehow check Nonce NA again. |
62 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. |