16 Note: this differs from the Woo-Lam protocol discussed by Lowe (1996): |
16 Note: this differs from the Woo-Lam protocol discussed by Lowe (1996): |
17 Some New Attacks upon Security Protocols. |
17 Some New Attacks upon Security Protocols. |
18 Computer Security Foundations Workshop |
18 Computer Security Foundations Workshop |
19 *} |
19 *} |
20 |
20 |
21 consts woolam :: "event list set" |
21 inductive_set woolam :: "event list set" |
22 inductive woolam |
22 where |
23 intros |
|
24 (*Initial trace is empty*) |
23 (*Initial trace is empty*) |
25 Nil: "[] \<in> woolam" |
24 Nil: "[] \<in> woolam" |
26 |
25 |
27 (** These rules allow agents to send messages to themselves **) |
26 (** These rules allow agents to send messages to themselves **) |
28 |
27 |
29 (*The spy MAY say anything he CAN say. We do not expect him to |
28 (*The spy MAY say anything he CAN say. We do not expect him to |
30 invent new nonces here, but he can also use NS1. Common to |
29 invent new nonces here, but he can also use NS1. Common to |
31 all similar protocols.*) |
30 all similar protocols.*) |
32 Fake: "[| evsf \<in> woolam; X \<in> synth (analz (spies evsf)) |] |
31 | Fake: "[| evsf \<in> woolam; X \<in> synth (analz (spies evsf)) |] |
33 ==> Says Spy B X # evsf \<in> woolam" |
32 ==> Says Spy B X # evsf \<in> woolam" |
34 |
33 |
35 (*Alice initiates a protocol run*) |
34 (*Alice initiates a protocol run*) |
36 WL1: "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam" |
35 | WL1: "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam" |
37 |
36 |
38 (*Bob responds to Alice's message with a challenge.*) |
37 (*Bob responds to Alice's message with a challenge.*) |
39 WL2: "[| evs2 \<in> woolam; Says A' B (Agent A) \<in> set evs2 |] |
38 | WL2: "[| evs2 \<in> woolam; Says A' B (Agent A) \<in> set evs2 |] |
40 ==> Says B A (Nonce NB) # evs2 \<in> woolam" |
39 ==> Says B A (Nonce NB) # evs2 \<in> woolam" |
41 |
40 |
42 (*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. |
43 B is *not* properly determined -- Alice essentially broadcasts |
42 B is *not* properly determined -- Alice essentially broadcasts |
44 her reply.*) |
43 her reply.*) |
45 WL3: "[| evs3 \<in> woolam; |
44 | WL3: "[| evs3 \<in> woolam; |
46 Says A B (Agent A) \<in> set evs3; |
45 Says A B (Agent A) \<in> set evs3; |
47 Says B' A (Nonce NB) \<in> set evs3 |] |
46 Says B' A (Nonce NB) \<in> set evs3 |] |
48 ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam" |
47 ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam" |
49 |
48 |
50 (*Bob forwards Alice's response to the Server. NOTE: usually |
49 (*Bob forwards Alice's response to the Server. NOTE: usually |
51 the messages are shown in chronological order, for clarity. |
50 the messages are shown in chronological order, for clarity. |
52 But here, exchanging the two events would cause the lemma |
51 But here, exchanging the two events would cause the lemma |
53 WL4_analz_spies to pick up the wrong assumption!*) |
52 WL4_analz_spies to pick up the wrong assumption!*) |
54 WL4: "[| evs4 \<in> woolam; |
53 | WL4: "[| evs4 \<in> woolam; |
55 Says A' B X \<in> set evs4; |
54 Says A' B X \<in> set evs4; |
56 Says A'' B (Agent A) \<in> set evs4 |] |
55 Says A'' B (Agent A) \<in> set evs4 |] |
57 ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam" |
56 ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam" |
58 |
57 |
59 (*Server decrypts Alice's response for Bob.*) |
58 (*Server decrypts Alice's response for Bob.*) |
60 WL5: "[| evs5 \<in> woolam; |
59 | WL5: "[| evs5 \<in> woolam; |
61 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)|} |
62 \<in> set evs5 |] |
61 \<in> set evs5 |] |
63 ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) |
62 ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) |
64 # evs5 \<in> woolam" |
63 # evs5 \<in> woolam" |
65 |
64 |