9 |
9 |
10 header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*} |
10 header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*} |
11 |
11 |
12 theory NS_Public imports Public begin |
12 theory NS_Public imports Public begin |
13 |
13 |
14 consts ns_public :: "event list set" |
14 inductive_set ns_public :: "event list set" |
15 |
15 where |
16 inductive ns_public |
|
17 intros |
|
18 (*Initial trace is empty*) |
16 (*Initial trace is empty*) |
19 Nil: "[] \<in> ns_public" |
17 Nil: "[] \<in> ns_public" |
20 |
18 |
21 (*The spy MAY say anything he CAN say. We do not expect him to |
19 (*The spy MAY say anything he CAN say. We do not expect him to |
22 invent new nonces here, but he can also use NS1. Common to |
20 invent new nonces here, but he can also use NS1. Common to |
23 all similar protocols.*) |
21 all similar protocols.*) |
24 Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (spies evsf))\<rbrakk> |
22 | Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (spies evsf))\<rbrakk> |
25 \<Longrightarrow> Says Spy B X # evsf \<in> ns_public" |
23 \<Longrightarrow> Says Spy B X # evsf \<in> ns_public" |
26 |
24 |
27 (*Alice initiates a protocol run, sending a nonce to Bob*) |
25 (*Alice initiates a protocol run, sending a nonce to Bob*) |
28 NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
26 | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
29 \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
27 \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
30 # evs1 \<in> ns_public" |
28 # evs1 \<in> ns_public" |
31 |
29 |
32 (*Bob responds to Alice's message with a further nonce*) |
30 (*Bob responds to Alice's message with a further nonce*) |
33 NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
31 | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
34 Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
32 Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
35 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
33 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
36 # evs2 \<in> ns_public" |
34 # evs2 \<in> ns_public" |
37 |
35 |
38 (*Alice proves her existence by sending NB back to Bob.*) |
36 (*Alice proves her existence by sending NB back to Bob.*) |
39 NS3: "\<lbrakk>evs3 \<in> ns_public; |
37 | NS3: "\<lbrakk>evs3 \<in> ns_public; |
40 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
38 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
41 Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
39 Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) |
42 \<in> set evs3\<rbrakk> |
40 \<in> set evs3\<rbrakk> |
43 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
41 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
44 |
42 |