20 inductive woolam |
20 inductive woolam |
21 intrs |
21 intrs |
22 (*Initial trace is empty*) |
22 (*Initial trace is empty*) |
23 Nil "[]: woolam" |
23 Nil "[]: woolam" |
24 |
24 |
|
25 (** These rules allow agents to send messages to themselves **) |
|
26 |
25 (*The spy MAY say anything he CAN say. We do not expect him to |
27 (*The spy MAY say anything he CAN say. We do not expect him to |
26 invent new nonces here, but he can also use NS1. Common to |
28 invent new nonces here, but he can also use NS1. Common to |
27 all similar protocols.*) |
29 all similar protocols.*) |
28 Fake "[| evs: woolam; B ~= Spy; |
30 Fake "[| evs: woolam; X: synth (analz (spies evs)) |] |
29 X: synth (analz (spies evs)) |] |
|
30 ==> Says Spy B X # evs : woolam" |
31 ==> Says Spy B X # evs : woolam" |
31 |
32 |
32 (*Alice initiates a protocol run*) |
33 (*Alice initiates a protocol run*) |
33 WL1 "[| evs1: woolam; A ~= B |] |
34 WL1 "[| evs1: woolam |] |
34 ==> Says A B (Agent A) # evs1 : woolam" |
35 ==> Says A B (Agent A) # evs1 : woolam" |
35 |
36 |
36 (*Bob responds to Alice's message with a challenge.*) |
37 (*Bob responds to Alice's message with a challenge.*) |
37 WL2 "[| evs2: woolam; A ~= B; |
38 WL2 "[| evs2: woolam; Says A' B (Agent A) : set evs2 |] |
38 Says A' B (Agent A) : set evs2 |] |
|
39 ==> Says B A (Nonce NB) # evs2 : woolam" |
39 ==> Says B A (Nonce NB) # evs2 : woolam" |
40 |
40 |
41 (*Alice responds to Bob's challenge by encrypting NB with her key. |
41 (*Alice responds to Bob's challenge by encrypting NB with her key. |
42 B is *not* properly determined -- Alice essentially broadcasts |
42 B is *not* properly determined -- Alice essentially broadcasts |
43 her reply.*) |
43 her reply.*) |
48 |
48 |
49 (*Bob forwards Alice's response to the Server. NOTE: usually |
49 (*Bob forwards Alice's response to the Server. NOTE: usually |
50 the messages are shown in chronological order, for clarity. |
50 the messages are shown in chronological order, for clarity. |
51 But here, exchanging the two events would cause the lemma |
51 But here, exchanging the two events would cause the lemma |
52 WL4_analz_spies to pick up the wrong assumption!*) |
52 WL4_analz_spies to pick up the wrong assumption!*) |
53 WL4 "[| evs4: woolam; B ~= Server; |
53 WL4 "[| evs4: woolam; |
54 Says A' B X : set evs4; |
54 Says A' B X : set evs4; |
55 Says A'' B (Agent A) : set evs4 |] |
55 Says A'' B (Agent A) : set evs4 |] |
56 ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam" |
56 ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam" |
57 |
57 |
58 (*Server decrypts Alice's response for Bob.*) |
58 (*Server decrypts Alice's response for Bob.*) |
59 WL5 "[| evs5: woolam; B ~= Server; |
59 WL5 "[| evs5: woolam; |
60 Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} |
60 Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} |
61 : set evs5 |] |
61 : set evs5 |] |
62 ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) |
62 ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) |
63 # evs5 : woolam" |
63 # evs5 : woolam" |
64 |
64 |