12 Demonstrates of why Oops is necessary. This protocol can be attacked because |
12 Demonstrates of why Oops is necessary. This protocol can be attacked because |
13 it doesn't keep NB secret, but without Oops it can be "verified" anyway. |
13 it doesn't keep NB secret, but without Oops it can be "verified" anyway. |
14 The issues are discussed in lcp's LICS 2000 invited lecture. |
14 The issues are discussed in lcp's LICS 2000 invited lecture. |
15 *} |
15 *} |
16 |
16 |
17 consts yahalom :: "event list set" |
17 inductive_set yahalom :: "event list set" |
18 inductive "yahalom" |
18 where |
19 intros |
|
20 (*Initial trace is empty*) |
19 (*Initial trace is empty*) |
21 Nil: "[] \<in> yahalom" |
20 Nil: "[] \<in> yahalom" |
22 |
21 |
23 (*The spy MAY say anything he CAN say. We do not expect him to |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
24 invent new nonces here, but he can also use NS1. Common to |
23 invent new nonces here, but he can also use NS1. Common to |
25 all similar protocols.*) |
24 all similar protocols.*) |
26 Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] |
25 | Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] |
27 ==> Says Spy B X # evsf \<in> yahalom" |
26 ==> Says Spy B X # evsf \<in> yahalom" |
28 |
27 |
29 (*A message that has been sent can be received by the |
28 (*A message that has been sent can be received by the |
30 intended recipient.*) |
29 intended recipient.*) |
31 Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] |
30 | Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] |
32 ==> Gets B X # evsr \<in> yahalom" |
31 ==> Gets B X # evsr \<in> yahalom" |
33 |
32 |
34 (*Alice initiates a protocol run*) |
33 (*Alice initiates a protocol run*) |
35 YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] |
34 | YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] |
36 ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom" |
35 ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom" |
37 |
36 |
38 (*Bob's response to Alice's message.*) |
37 (*Bob's response to Alice's message.*) |
39 YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
38 | YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; |
40 Gets B {|Agent A, Nonce NA|} \<in> set evs2 |] |
39 Gets B {|Agent A, Nonce NA|} \<in> set evs2 |] |
41 ==> Says B Server |
40 ==> Says B Server |
42 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
41 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
43 # evs2 \<in> yahalom" |
42 # evs2 \<in> yahalom" |
44 |
43 |
45 (*The Server receives Bob's message. He responds by sending a |
44 (*The Server receives Bob's message. He responds by sending a |
46 new session key to Alice, with a packet for forwarding to Bob.*) |
45 new session key to Alice, with a packet for forwarding to Bob.*) |
47 YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; |
46 | YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; |
48 Gets Server |
47 Gets Server |
49 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
48 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
50 \<in> set evs3 |] |
49 \<in> set evs3 |] |
51 ==> Says Server A |
50 ==> Says Server A |
52 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
51 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
54 # evs3 \<in> yahalom" |
53 # evs3 \<in> yahalom" |
55 |
54 |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
55 (*Alice receives the Server's (?) message, checks her Nonce, and |
57 uses the new session key to send Bob his Nonce. The premise |
56 uses the new session key to send Bob his Nonce. The premise |
58 A \<noteq> Server is needed to prove Says_Server_not_range.*) |
57 A \<noteq> Server is needed to prove Says_Server_not_range.*) |
59 YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; |
58 | YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; |
60 Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
59 Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} |
61 \<in> set evs4; |
60 \<in> set evs4; |
62 Says A B {|Agent A, Nonce NA|} \<in> set evs4 |] |
61 Says A B {|Agent A, Nonce NA|} \<in> set evs4 |] |
63 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom" |
62 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom" |
64 |
63 |