author | wenzelm |
Wed, 03 Oct 2001 20:54:16 +0200 | |
changeset 11655 | 923e4d0d36d5 |
parent 11465 | 45d156ede468 |
child 13507 | febb8e5d2a9d |
permissions | -rw-r--r-- |
1934 | 1 |
(* Title: HOL/Auth/NS_Shared |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol. |
|
7 |
||
8 |
From page 247 of |
|
9 |
Burrows, Abadi and Needham. A Logic of Authentication. |
|
10 |
Proc. Royal Soc. 426 (1989) |
|
11 |
*) |
|
12 |
||
11104 | 13 |
theory NS_Shared = Shared: |
1934 | 14 |
|
11104 | 15 |
consts ns_shared :: "event list set" |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset
|
16 |
inductive "ns_shared" |
11104 | 17 |
intros |
18 |
(*Initial trace is empty*) |
|
11465 | 19 |
Nil: "[] \\<in> ns_shared" |
11104 | 20 |
(*The spy MAY say anything he CAN say. We do not expect him to |
21 |
invent new nonces here, but he can also use NS1. Common to |
|
22 |
all similar protocols.*) |
|
11465 | 23 |
Fake: "\\<lbrakk>evsf \\<in> ns_shared; X \\<in> synth (analz (spies evsf))\\<rbrakk> |
24 |
\\<Longrightarrow> Says Spy B X # evsf \\<in> ns_shared" |
|
11104 | 25 |
|
26 |
(*Alice initiates a protocol run, requesting to talk to any B*) |
|
11465 | 27 |
NS1: "\\<lbrakk>evs1 \\<in> ns_shared; Nonce NA \\<notin> used evs1\\<rbrakk> |
28 |
\\<Longrightarrow> Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> # evs1 \\<in> ns_shared" |
|
11104 | 29 |
|
30 |
(*Server's response to Alice's message. |
|
31 |
!! It may respond more than once to A's request !! |
|
32 |
Server doesn't know who the true sender is, hence the A' in |
|
33 |
the sender field.*) |
|
11465 | 34 |
NS2: "\\<lbrakk>evs2 \\<in> ns_shared; Key KAB \\<notin> used evs2; |
35 |
Says A' Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs2\\<rbrakk> |
|
36 |
\\<Longrightarrow> Says Server A |
|
11104 | 37 |
(Crypt (shrK A) |
11465 | 38 |
\\<lbrace>Nonce NA, Agent B, Key KAB, |
39 |
(Crypt (shrK B) \\<lbrace>Key KAB, Agent A\\<rbrace>)\\<rbrace>) |
|
40 |
# evs2 \\<in> ns_shared" |
|
11104 | 41 |
|
42 |
(*We can't assume S=Server. Agent A "remembers" her nonce. |
|
11465 | 43 |
Need A \\<noteq> Server because we allow messages to self.*) |
44 |
NS3: "\\<lbrakk>evs3 \\<in> ns_shared; A \\<noteq> Server; |
|
45 |
Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs3; |
|
46 |
Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs3\\<rbrakk> |
|
47 |
\\<Longrightarrow> Says A B X # evs3 \\<in> ns_shared" |
|
11104 | 48 |
|
49 |
(*Bob's nonce exchange. He does not know who the message came |
|
50 |
from, but responds to A because she is mentioned inside.*) |
|
11465 | 51 |
NS4: "\\<lbrakk>evs4 \\<in> ns_shared; Nonce NB \\<notin> used evs4; |
52 |
Says A' B (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<in> set evs4\\<rbrakk> |
|
53 |
\\<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \\<in> ns_shared" |
|
1934 | 54 |
|
11104 | 55 |
(*Alice responds with Nonce NB if she has seen the key before. |
56 |
Maybe should somehow check Nonce NA again. |
|
57 |
We do NOT send NB-1 or similar as the Spy cannot spoof such things. |
|
11465 | 58 |
Letting the Spy add or subtract 1 lets him send all nonces. |
11104 | 59 |
Instead we distinguish the messages by sending the nonce twice.*) |
11465 | 60 |
NS5: "\\<lbrakk>evs5 \\<in> ns_shared; |
61 |
Says B' A (Crypt K (Nonce NB)) \\<in> set evs5; |
|
62 |
Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) |
|
63 |
\\<in> set evs5\\<rbrakk> |
|
64 |
\\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) # evs5 \\<in> ns_shared" |
|
11104 | 65 |
|
66 |
(*This message models possible leaks of session keys. |
|
67 |
The two Nonces identify the protocol run: the rule insists upon |
|
68 |
the true senders in order to make them accurate.*) |
|
11465 | 69 |
Oops: "\\<lbrakk>evso \\<in> ns_shared; Says B A (Crypt K (Nonce NB)) \\<in> set evso; |
70 |
Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) |
|
71 |
\\<in> set evso\\<rbrakk> |
|
72 |
\\<Longrightarrow> Notes Spy \\<lbrace>Nonce NA, Nonce NB, Key K\\<rbrace> # evso \\<in> ns_shared" |
|
11104 | 73 |
|
11150 | 74 |
|
75 |
declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
|
76 |
declare parts.Body [dest] |
|
11251 | 77 |
declare Fake_parts_insert_in_Un [dest] |
78 |
declare analz_into_parts [dest] |
|
11104 | 79 |
declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |
80 |
||
81 |
||
82 |
(*A "possibility property": there are traces that reach the end*) |
|
11465 | 83 |
lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared. |
84 |
Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs" |
|
11104 | 85 |
apply (intro exI bexI) |
86 |
apply (rule_tac [2] ns_shared.Nil |
|
87 |
[THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3, |
|
88 |
THEN ns_shared.NS4, THEN ns_shared.NS5]) |
|
89 |
apply possibility |
|
90 |
done |
|
91 |
||
92 |
(*This version is similar, while instantiating ?K and ?N to epsilon-terms |
|
11465 | 93 |
lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared. |
94 |
Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs" |
|
11104 | 95 |
*) |
96 |
||
97 |
||
98 |
(**** Inductive proofs about ns_shared ****) |
|
99 |
||
11280 | 100 |
(** Forwarding lemmas, to aid simplification **) |
1934 | 101 |
|
11104 | 102 |
(*For reasoning about the encrypted portion of message NS3*) |
103 |
lemma NS3_msg_in_parts_spies: |
|
11465 | 104 |
"Says S A (Crypt KA \\<lbrace>N, B, K, X\\<rbrace>) \\<in> set evs \\<Longrightarrow> X \\<in> parts (spies evs)" |
11104 | 105 |
by blast |
11280 | 106 |
|
11104 | 107 |
(*For reasoning about the Oops message*) |
108 |
lemma Oops_parts_spies: |
|
11465 | 109 |
"Says Server A (Crypt (shrK A) \\<lbrace>NA, B, K, X\\<rbrace>) \\<in> set evs |
110 |
\\<Longrightarrow> K \\<in> parts (spies evs)" |
|
11104 | 111 |
by blast |
112 |
||
11465 | 113 |
(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY |
11104 | 114 |
sends messages containing X! **) |
115 |
||
116 |
(*Spy never sees another agent's shared key! (unless it's bad at start)*) |
|
117 |
lemma Spy_see_shrK [simp]: |
|
11465 | 118 |
"evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)" |
11280 | 119 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
11104 | 120 |
apply simp_all |
121 |
apply blast+; |
|
122 |
done |
|
123 |
||
124 |
lemma Spy_analz_shrK [simp]: |
|
11465 | 125 |
"evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)" |
11104 | 126 |
by auto |
127 |
||
128 |
||
129 |
(*Nobody can have used non-existent keys!*) |
|
130 |
lemma new_keys_not_used [rule_format, simp]: |
|
11465 | 131 |
"evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))" |
11280 | 132 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
11104 | 133 |
apply simp_all |
134 |
(*Fake, NS2, NS4, NS5*) |
|
135 |
apply (blast dest!: keysFor_parts_insert)+ |
|
136 |
done |
|
137 |
||
138 |
||
139 |
(** Lemmas concerning the form of items passed in messages **) |
|
140 |
||
141 |
(*Describes the form of K, X and K' when the Server sends this message.*) |
|
142 |
lemma Says_Server_message_form: |
|
11465 | 143 |
"\\<lbrakk>Says Server A (Crypt K' \\<lbrace>N, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
144 |
evs \\<in> ns_shared\\<rbrakk> |
|
145 |
\\<Longrightarrow> K \\<notin> range shrK \\<and> |
|
146 |
X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<and> |
|
11104 | 147 |
K' = shrK A" |
148 |
by (erule rev_mp, erule ns_shared.induct, auto) |
|
149 |
||
1934 | 150 |
|
11104 | 151 |
(*If the encrypted message appears then it originated with the Server*) |
152 |
lemma A_trusts_NS2: |
|
11465 | 153 |
"\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
154 |
A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
155 |
\\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs" |
|
11104 | 156 |
apply (erule rev_mp) |
157 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
|
158 |
apply auto |
|
159 |
done |
|
160 |
||
161 |
lemma cert_A_form: |
|
11465 | 162 |
"\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
163 |
A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
164 |
\\<Longrightarrow> K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>)" |
|
11104 | 165 |
by (blast dest!: A_trusts_NS2 Says_Server_message_form) |
166 |
||
167 |
(*EITHER describes the form of X when the following message is sent, |
|
168 |
OR reduces it to the Fake case. |
|
169 |
Use Says_Server_message_form if applicable.*) |
|
170 |
lemma Says_S_message_form: |
|
11465 | 171 |
"\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
172 |
evs \\<in> ns_shared\\<rbrakk> |
|
173 |
\\<Longrightarrow> (K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>)) |
|
174 |
\\<or> X \\<in> analz (spies evs)" |
|
11150 | 175 |
by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj) |
176 |
||
11104 | 177 |
|
178 |
(*Alternative version also provable |
|
179 |
lemma Says_S_message_form2: |
|
11465 | 180 |
"\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
181 |
evs \\<in> ns_shared\\<rbrakk> |
|
182 |
\\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs |
|
183 |
\\<or> X \\<in> analz (spies evs)" |
|
184 |
apply (case_tac "A \\<in> bad") |
|
11104 | 185 |
apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]); |
186 |
by (blast dest!: A_trusts_NS2 Says_Server_message_form) |
|
187 |
*) |
|
188 |
||
189 |
||
190 |
(**** |
|
191 |
SESSION KEY COMPROMISE THEOREM. To prove theorems of the form |
|
192 |
||
11465 | 193 |
Key K \\<in> analz (insert (Key KAB) (spies evs)) \\<Longrightarrow> |
194 |
Key K \\<in> analz (spies evs) |
|
11104 | 195 |
|
196 |
A more general formula must be proved inductively. |
|
197 |
****) |
|
1934 | 198 |
|
11104 | 199 |
(*NOT useful in this form, but it says that session keys are not used |
200 |
to encrypt messages containing other keys, in the actual protocol. |
|
201 |
We require that agents should behave like this subsequently also.*) |
|
11465 | 202 |
lemma "\\<lbrakk>evs \\<in> ns_shared; Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
203 |
(Crypt KAB X) \\<in> parts (spies evs) \\<and> |
|
204 |
Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)" |
|
11280 | 205 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
11104 | 206 |
apply simp_all |
207 |
(*Fake*) |
|
208 |
apply (blast dest: parts_insert_subset_Un) |
|
209 |
(*Base, NS4 and NS5*) |
|
210 |
apply auto |
|
211 |
done |
|
212 |
||
213 |
||
214 |
(** Session keys are not used to encrypt other session keys **) |
|
215 |
||
216 |
(*The equality makes the induction hypothesis easier to apply*) |
|
217 |
||
218 |
lemma analz_image_freshK [rule_format]: |
|
11465 | 219 |
"evs \\<in> ns_shared \\<Longrightarrow> |
220 |
\\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow> |
|
221 |
(Key K \\<in> analz (Key`KK \\<union> (spies evs))) = |
|
222 |
(K \\<in> KK \\<or> Key K \\<in> analz (spies evs))" |
|
11104 | 223 |
apply (erule ns_shared.induct, force) |
11280 | 224 |
apply (drule_tac [7] Says_Server_message_form) |
11104 | 225 |
apply (erule_tac [4] Says_S_message_form [THEN disjE]) |
11117 | 226 |
apply analz_freshK |
227 |
apply spy_analz |
|
11104 | 228 |
done |
229 |
||
230 |
||
231 |
lemma analz_insert_freshK: |
|
11465 | 232 |
"\\<lbrakk>evs \\<in> ns_shared; KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
11655 | 233 |
(Key K \\<in> analz (insert (Key KAB) (spies evs))) = |
11465 | 234 |
(K = KAB \\<or> Key K \\<in> analz (spies evs))" |
11104 | 235 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
236 |
||
237 |
||
238 |
(** The session key K uniquely identifies the message **) |
|
1934 | 239 |
|
11104 | 240 |
(*In messages of this form, the session key uniquely identifies the rest*) |
241 |
lemma unique_session_keys: |
|
11465 | 242 |
"\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
243 |
Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs; |
|
244 |
evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'" |
|
11104 | 245 |
apply (erule rev_mp, erule rev_mp, erule ns_shared.induct) |
246 |
apply simp_all |
|
247 |
apply blast+ |
|
248 |
done |
|
249 |
||
250 |
||
251 |
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) |
|
252 |
||
11150 | 253 |
(*Beware of [rule_format] and the universal quantifier!*) |
254 |
lemma secrecy_lemma: |
|
11465 | 255 |
"\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
256 |
Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) |
|
257 |
\\<in> set evs; |
|
258 |
A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
259 |
\\<Longrightarrow> (\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs) \\<longrightarrow> |
|
260 |
Key K \\<notin> analz (spies evs)" |
|
11104 | 261 |
apply (erule rev_mp) |
262 |
apply (erule ns_shared.induct, force) |
|
263 |
apply (frule_tac [7] Says_Server_message_form) |
|
264 |
apply (frule_tac [4] Says_S_message_form) |
|
265 |
apply (erule_tac [5] disjE) |
|
266 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs) |
|
11280 | 267 |
apply spy_analz (*Fake*) |
11104 | 268 |
apply blast (*NS2*) |
11188 | 269 |
(*NS3, Server sub-case*) (**LEVEL 8 **) |
270 |
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2 |
|
271 |
dest: Says_imp_knows_Spy analz.Inj unique_session_keys) |
|
11280 | 272 |
(*NS3, Spy sub-case; also Oops*) |
273 |
apply (blast dest: unique_session_keys)+ |
|
11104 | 274 |
done |
275 |
||
276 |
||
11188 | 277 |
|
11104 | 278 |
(*Final version: Server's message in the most abstract form*) |
279 |
lemma Spy_not_see_encrypted_key: |
|
11465 | 280 |
"\\<lbrakk>Says Server A (Crypt K' \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
281 |
\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs; |
|
282 |
A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
283 |
\\<Longrightarrow> Key K \\<notin> analz (spies evs)" |
|
11150 | 284 |
by (blast dest: Says_Server_message_form secrecy_lemma) |
11104 | 285 |
|
286 |
||
287 |
(**** Guarantees available at various stages of protocol ***) |
|
1934 | 288 |
|
11104 | 289 |
(*If the encrypted message appears then it originated with the Server*) |
290 |
lemma B_trusts_NS3: |
|
11465 | 291 |
"\\<lbrakk>Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs); |
292 |
B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
293 |
\\<Longrightarrow> \\<exists>NA. Says Server A |
|
294 |
(Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
|
295 |
Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) |
|
296 |
\\<in> set evs" |
|
11104 | 297 |
apply (erule rev_mp) |
298 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
|
299 |
apply auto |
|
300 |
done |
|
301 |
||
302 |
||
303 |
lemma A_trusts_NS4_lemma [rule_format]: |
|
11465 | 304 |
"evs \\<in> ns_shared \\<Longrightarrow> |
305 |
Key K \\<notin> analz (spies evs) \\<longrightarrow> |
|
306 |
Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow> |
|
307 |
Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow> |
|
308 |
Says B A (Crypt K (Nonce NB)) \\<in> set evs" |
|
11104 | 309 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
11251 | 310 |
apply (analz_mono_contra, simp_all) |
11104 | 311 |
apply blast (*Fake*) |
11280 | 312 |
(*NS2: contradiction from the assumptions |
11465 | 313 |
Key K \\<notin> used evs2 and Crypt K (Nonce NB) \\<in> parts (spies evs2) *) |
11280 | 314 |
apply (force dest!: Crypt_imp_keysFor) |
11104 | 315 |
apply blast (*NS3*) |
316 |
(*NS4*) |
|
11150 | 317 |
apply (blast dest!: B_trusts_NS3 |
11280 | 318 |
dest: Says_imp_knows_Spy [THEN analz.Inj] |
11150 | 319 |
Crypt_Spy_analz_bad unique_session_keys) |
11104 | 320 |
done |
321 |
||
322 |
(*This version no longer assumes that K is secure*) |
|
323 |
lemma A_trusts_NS4: |
|
11465 | 324 |
"\\<lbrakk>Crypt K (Nonce NB) \\<in> parts (spies evs); |
325 |
Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
|
326 |
\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs; |
|
327 |
A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
328 |
\\<Longrightarrow> Says B A (Crypt K (Nonce NB)) \\<in> set evs" |
|
11280 | 329 |
by (blast intro: A_trusts_NS4_lemma |
11104 | 330 |
dest: A_trusts_NS2 Spy_not_see_encrypted_key) |
331 |
||
332 |
(*If the session key has been used in NS4 then somebody has forwarded |
|
11280 | 333 |
component X in some instance of NS4. Perhaps an interesting property, |
11104 | 334 |
but not needed (after all) for the proofs below.*) |
335 |
theorem NS4_implies_NS3 [rule_format]: |
|
11465 | 336 |
"evs \\<in> ns_shared \\<Longrightarrow> |
337 |
Key K \\<notin> analz (spies evs) \\<longrightarrow> |
|
338 |
Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow> |
|
339 |
Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow> |
|
340 |
(\\<exists>A'. Says A' B X \\<in> set evs)" |
|
11104 | 341 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
342 |
apply analz_mono_contra |
|
343 |
apply (simp_all add: ex_disj_distrib) |
|
344 |
apply blast (*Fake*) |
|
345 |
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) |
|
346 |
apply blast (*NS3*) |
|
347 |
(*NS4*) |
|
11150 | 348 |
apply (blast dest!: B_trusts_NS3 |
11280 | 349 |
dest: Says_imp_knows_Spy [THEN analz.Inj] |
11150 | 350 |
unique_session_keys Crypt_Spy_analz_bad) |
11104 | 351 |
done |
352 |
||
353 |
||
354 |
lemma B_trusts_NS5_lemma [rule_format]: |
|
11465 | 355 |
"\\<lbrakk>B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> |
356 |
Key K \\<notin> analz (spies evs) \\<longrightarrow> |
|
11104 | 357 |
Says Server A |
11465 | 358 |
(Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
359 |
Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow> |
|
360 |
Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow> |
|
361 |
Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs" |
|
11104 | 362 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
363 |
apply analz_mono_contra |
|
11280 | 364 |
apply simp_all |
11104 | 365 |
apply blast (*Fake*) |
366 |
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) |
|
367 |
apply (blast dest!: cert_A_form) (*NS3*) |
|
368 |
(*NS5*) |
|
11150 | 369 |
apply (blast dest!: A_trusts_NS2 |
11280 | 370 |
dest: Says_imp_knows_Spy [THEN analz.Inj] |
11150 | 371 |
unique_session_keys Crypt_Spy_analz_bad) |
11104 | 372 |
done |
373 |
||
374 |
||
375 |
(*Very strong Oops condition reveals protocol's weakness*) |
|
376 |
lemma B_trusts_NS5: |
|
11465 | 377 |
"\\<lbrakk>Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs); |
378 |
Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs); |
|
379 |
\\<forall>NA NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs; |
|
380 |
A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
|
381 |
\\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs" |
|
11280 | 382 |
by (blast intro: B_trusts_NS5_lemma |
11150 | 383 |
dest: B_trusts_NS3 Spy_not_see_encrypted_key) |
1934 | 384 |
|
385 |
end |