|
1 (* ID: $Id$ |
|
2 Author: Giampaolo Bella, Catania University |
|
3 *) |
|
4 |
|
5 header{*The Kerberos Protocol, BAN Version, with Gets event*} |
|
6 |
|
7 theory Kerberos_BAN_Gets imports Public begin |
|
8 |
|
9 text{*From page 251 of |
|
10 Burrows, Abadi and Needham (1989). A Logic of Authentication. |
|
11 Proc. Royal Soc. 426 |
|
12 |
|
13 Confidentiality (secrecy) and authentication properties rely on |
|
14 temporal checks: strong guarantees in a little abstracted - but |
|
15 very realistic - model. |
|
16 *} |
|
17 |
|
18 (* Temporal modelization: session keys can be leaked |
|
19 ONLY when they have expired *) |
|
20 |
|
21 syntax |
|
22 CT :: "event list=>nat" |
|
23 expiredK :: "[nat, event list] => bool" |
|
24 expiredA :: "[nat, event list] => bool" |
|
25 |
|
26 consts |
|
27 |
|
28 (*Duration of the session key*) |
|
29 sesKlife :: nat |
|
30 |
|
31 (*Duration of the authenticator*) |
|
32 authlife :: nat |
|
33 |
|
34 text{*The ticket should remain fresh for two journeys on the network at least*} |
|
35 text{*The Gets event causes longer traces for the protocol to reach its end*} |
|
36 specification (sesKlife) |
|
37 sesKlife_LB [iff]: "4 \<le> sesKlife" |
|
38 by blast |
|
39 |
|
40 text{*The authenticator only for one journey*} |
|
41 text{*The Gets event causes longer traces for the protocol to reach its end*} |
|
42 specification (authlife) |
|
43 authlife_LB [iff]: "2 \<le> authlife" |
|
44 by blast |
|
45 |
|
46 |
|
47 translations |
|
48 "CT" == "length " |
|
49 |
|
50 "expiredK T evs" == "sesKlife + T < CT evs" |
|
51 |
|
52 "expiredA T evs" == "authlife + T < CT evs" |
|
53 |
|
54 |
|
55 constdefs |
|
56 (* Yields the subtrace of a given trace from its beginning to a given event *) |
|
57 before :: "[event, event list] => event list" ("before _ on _") |
|
58 "before ev on evs == takeWhile (% z. z ~= ev) (rev evs)" |
|
59 |
|
60 (* States than an event really appears only once on a trace *) |
|
61 Unique :: "[event, event list] => bool" ("Unique _ on _") |
|
62 "Unique ev on evs == |
|
63 ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))" |
|
64 |
|
65 |
|
66 consts bankerb_gets :: "event list set" |
|
67 inductive "bankerb_gets" |
|
68 intros |
|
69 |
|
70 Nil: "[] \<in> bankerb_gets" |
|
71 |
|
72 Fake: "\<lbrakk> evsf \<in> bankerb_gets; X \<in> synth (analz (knows Spy evsf)) \<rbrakk> |
|
73 \<Longrightarrow> Says Spy B X # evsf \<in> bankerb_gets" |
|
74 |
|
75 Reception: "\<lbrakk> evsr\<in> bankerb_gets; Says A B X \<in> set evsr \<rbrakk> |
|
76 \<Longrightarrow> Gets B X # evsr \<in> bankerb_gets" |
|
77 |
|
78 BK1: "\<lbrakk> evs1 \<in> bankerb_gets \<rbrakk> |
|
79 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1 |
|
80 \<in> bankerb_gets" |
|
81 |
|
82 |
|
83 BK2: "\<lbrakk> evs2 \<in> bankerb_gets; Key K \<notin> used evs2; K \<in> symKeys; |
|
84 Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
|
85 \<Longrightarrow> Says Server A |
|
86 (Crypt (shrK A) |
|
87 \<lbrace>Number (CT evs2), Agent B, Key K, |
|
88 (Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>) |
|
89 # evs2 \<in> bankerb_gets" |
|
90 |
|
91 |
|
92 BK3: "\<lbrakk> evs3 \<in> bankerb_gets; |
|
93 Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
94 \<in> set evs3; |
|
95 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
|
96 \<not> expiredK Tk evs3 \<rbrakk> |
|
97 \<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace> |
|
98 # evs3 \<in> bankerb_gets" |
|
99 |
|
100 |
|
101 BK4: "\<lbrakk> evs4 \<in> bankerb_gets; |
|
102 Gets B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>), |
|
103 (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4; |
|
104 \<not> expiredK Tk evs4; \<not> expiredA Ta evs4 \<rbrakk> |
|
105 \<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4 |
|
106 \<in> bankerb_gets" |
|
107 |
|
108 (*Old session keys may become compromised*) |
|
109 Oops: "\<lbrakk> evso \<in> bankerb_gets; |
|
110 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
111 \<in> set evso; |
|
112 expiredK Tk evso \<rbrakk> |
|
113 \<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerb_gets" |
|
114 |
|
115 |
|
116 declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
|
117 declare parts.Body [dest] |
|
118 declare analz_into_parts [dest] |
|
119 declare Fake_parts_insert_in_Un [dest] |
|
120 declare knows_Spy_partsEs [elim] |
|
121 |
|
122 |
|
123 text{*A "possibility property": there are traces that reach the end.*} |
|
124 lemma "\<lbrakk>Key K \<notin> used []; K \<in> symKeys\<rbrakk> |
|
125 \<Longrightarrow> \<exists>Timestamp. \<exists>evs \<in> bankerb_gets. |
|
126 Says B A (Crypt K (Number Timestamp)) |
|
127 \<in> set evs" |
|
128 apply (cut_tac sesKlife_LB) |
|
129 apply (cut_tac authlife_LB) |
|
130 apply (intro exI bexI) |
|
131 apply (rule_tac [2] |
|
132 bankerb_gets.Nil [THEN bankerb_gets.BK1, THEN bankerb_gets.Reception, |
|
133 THEN bankerb_gets.BK2, THEN bankerb_gets.Reception, |
|
134 THEN bankerb_gets.BK3, THEN bankerb_gets.Reception, |
|
135 THEN bankerb_gets.BK4]) |
|
136 apply (possibility, simp_all (no_asm_simp) add: used_Cons) |
|
137 done |
|
138 |
|
139 |
|
140 text{*Lemmas about reception invariant: if a message is received it certainly |
|
141 was sent*} |
|
142 lemma Gets_imp_Says : |
|
143 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" |
|
144 apply (erule rev_mp) |
|
145 apply (erule bankerb_gets.induct) |
|
146 apply auto |
|
147 done |
|
148 |
|
149 lemma Gets_imp_knows_Spy: |
|
150 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" |
|
151 apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
|
152 done |
|
153 |
|
154 lemma Gets_imp_knows_Spy_parts[dest]: |
|
155 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> parts (knows Spy evs)" |
|
156 apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj]) |
|
157 done |
|
158 |
|
159 lemma Gets_imp_knows: |
|
160 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> knows B evs" |
|
161 apply (case_tac "B = Spy") |
|
162 apply (blast dest!: Gets_imp_knows_Spy) |
|
163 apply (blast dest!: Gets_imp_knows_agents) |
|
164 done |
|
165 |
|
166 lemma Gets_imp_knows_analz: |
|
167 "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> analz (knows B evs)" |
|
168 apply (blast dest: Gets_imp_knows [THEN analz.Inj]) |
|
169 done |
|
170 |
|
171 text{*Lemmas for reasoning about predicate "before"*} |
|
172 lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"; |
|
173 apply (induct_tac "evs") |
|
174 apply simp |
|
175 apply (induct_tac "a") |
|
176 apply auto |
|
177 done |
|
178 |
|
179 lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"; |
|
180 apply (induct_tac "evs") |
|
181 apply simp |
|
182 apply (induct_tac "a") |
|
183 apply auto |
|
184 done |
|
185 |
|
186 lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"; |
|
187 apply (induct_tac "evs") |
|
188 apply simp |
|
189 apply (induct_tac "a") |
|
190 apply auto |
|
191 done |
|
192 |
|
193 lemma used_evs_rev: "used evs = used (rev evs)" |
|
194 apply (induct_tac "evs") |
|
195 apply simp |
|
196 apply (induct_tac "a") |
|
197 apply (simp add: used_Says_rev) |
|
198 apply (simp add: used_Gets_rev) |
|
199 apply (simp add: used_Notes_rev) |
|
200 done |
|
201 |
|
202 lemma used_takeWhile_used [rule_format]: |
|
203 "x : used (takeWhile P X) --> x : used X" |
|
204 apply (induct_tac "X") |
|
205 apply simp |
|
206 apply (induct_tac "a") |
|
207 apply (simp_all add: used_Nil) |
|
208 apply (blast dest!: initState_into_used)+ |
|
209 done |
|
210 |
|
211 lemma set_evs_rev: "set evs = set (rev evs)" |
|
212 apply auto |
|
213 done |
|
214 |
|
215 lemma takeWhile_void [rule_format]: |
|
216 "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs" |
|
217 apply auto |
|
218 done |
|
219 |
|
220 (**** Inductive proofs about bankerb_gets ****) |
|
221 |
|
222 text{*Forwarding Lemma for reasoning about the encrypted portion of message BK3*} |
|
223 lemma BK3_msg_in_parts_knows_Spy: |
|
224 "\<lbrakk>Gets A (Crypt KA \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs; evs \<in> bankerb_gets \<rbrakk> |
|
225 \<Longrightarrow> X \<in> parts (knows Spy evs)" |
|
226 apply blast |
|
227 done |
|
228 |
|
229 lemma Oops_parts_knows_Spy: |
|
230 "Says Server A (Crypt (shrK A) \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs |
|
231 \<Longrightarrow> K \<in> parts (knows Spy evs)" |
|
232 apply blast |
|
233 done |
|
234 |
|
235 |
|
236 text{*Spy never sees another agent's shared key! (unless it's bad at start)*} |
|
237 lemma Spy_see_shrK [simp]: |
|
238 "evs \<in> bankerb_gets \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
239 apply (erule bankerb_gets.induct) |
|
240 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
241 apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast+) |
|
242 done |
|
243 |
|
244 |
|
245 lemma Spy_analz_shrK [simp]: |
|
246 "evs \<in> bankerb_gets \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
247 by auto |
|
248 |
|
249 lemma Spy_see_shrK_D [dest!]: |
|
250 "\<lbrakk> Key (shrK A) \<in> parts (knows Spy evs); |
|
251 evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> A:bad" |
|
252 by (blast dest: Spy_see_shrK) |
|
253 |
|
254 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] |
|
255 |
|
256 |
|
257 text{*Nobody can have used non-existent keys!*} |
|
258 lemma new_keys_not_used [simp]: |
|
259 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> bankerb_gets\<rbrakk> |
|
260 \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))" |
|
261 apply (erule rev_mp) |
|
262 apply (erule bankerb_gets.induct) |
|
263 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
264 apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all) |
|
265 txt{*Fake*} |
|
266 apply (force dest!: keysFor_parts_insert) |
|
267 txt{*BK2, BK3, BK4*} |
|
268 apply (force dest!: analz_shrK_Decrypt)+ |
|
269 done |
|
270 |
|
271 subsection{* Lemmas concerning the form of items passed in messages *} |
|
272 |
|
273 text{*Describes the form of K, X and K' when the Server sends this message.*} |
|
274 lemma Says_Server_message_form: |
|
275 "\<lbrakk> Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
276 \<in> set evs; evs \<in> bankerb_gets \<rbrakk> |
|
277 \<Longrightarrow> K' = shrK A & K \<notin> range shrK & |
|
278 Ticket = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>) & |
|
279 Key K \<notin> used(before |
|
280 Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
281 on evs) & |
|
282 Tk = CT(before |
|
283 Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
284 on evs)" |
|
285 apply (unfold before_def) |
|
286 apply (erule rev_mp) |
|
287 apply (erule bankerb_gets.induct, simp_all) |
|
288 txt{*We need this simplification only for Message 2*} |
|
289 apply (simp (no_asm) add: takeWhile_tail) |
|
290 apply auto |
|
291 txt{*Two subcases of Message 2. Subcase: used before*} |
|
292 apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] |
|
293 used_takeWhile_used) |
|
294 txt{*subcase: CT before*} |
|
295 apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void]) |
|
296 done |
|
297 |
|
298 |
|
299 text{*If the encrypted message appears then it originated with the Server |
|
300 PROVIDED that A is NOT compromised! |
|
301 This allows A to verify freshness of the session key. |
|
302 *} |
|
303 lemma Kab_authentic: |
|
304 "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> |
|
305 \<in> parts (knows Spy evs); |
|
306 A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
307 \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
308 \<in> set evs" |
|
309 apply (erule rev_mp) |
|
310 apply (erule bankerb_gets.induct) |
|
311 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
312 apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast) |
|
313 done |
|
314 |
|
315 |
|
316 text{*If the TICKET appears then it originated with the Server*} |
|
317 text{*FRESHNESS OF THE SESSION KEY to B*} |
|
318 lemma ticket_authentic: |
|
319 "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); |
|
320 B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
321 \<Longrightarrow> Says Server A |
|
322 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
323 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
324 \<in> set evs" |
|
325 apply (erule rev_mp) |
|
326 apply (erule bankerb_gets.induct) |
|
327 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
328 apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast) |
|
329 done |
|
330 |
|
331 |
|
332 text{*EITHER describes the form of X when the following message is sent, |
|
333 OR reduces it to the Fake case. |
|
334 Use @{text Says_Server_message_form} if applicable.*} |
|
335 lemma Gets_Server_message_form: |
|
336 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
337 \<in> set evs; |
|
338 evs \<in> bankerb_gets \<rbrakk> |
|
339 \<Longrightarrow> (K \<notin> range shrK & X = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>)) |
|
340 | X \<in> analz (knows Spy evs)" |
|
341 apply (case_tac "A \<in> bad") |
|
342 apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj]) |
|
343 apply (blast dest!: Kab_authentic Says_Server_message_form) |
|
344 done |
|
345 |
|
346 |
|
347 text{*Reliability guarantees: honest agents act as we expect*} |
|
348 |
|
349 lemma BK3_imp_Gets: |
|
350 "\<lbrakk> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs; |
|
351 A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
352 \<Longrightarrow> \<exists> Tk. Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
353 \<in> set evs" |
|
354 apply (erule rev_mp) |
|
355 apply (erule bankerb_gets.induct) |
|
356 apply auto |
|
357 done |
|
358 |
|
359 lemma BK4_imp_Gets: |
|
360 "\<lbrakk> Says B A (Crypt K (Number Ta)) \<in> set evs; |
|
361 B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
362 \<Longrightarrow> \<exists> Tk. Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
363 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
364 apply (erule rev_mp) |
|
365 apply (erule bankerb_gets.induct) |
|
366 apply auto |
|
367 done |
|
368 |
|
369 lemma Gets_A_knows_K: |
|
370 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
371 evs \<in> bankerb_gets \<rbrakk> |
|
372 \<Longrightarrow> Key K \<in> analz (knows A evs)" |
|
373 apply (force dest: Gets_imp_knows_analz) |
|
374 done |
|
375 |
|
376 lemma Gets_B_knows_K: |
|
377 "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
378 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs; |
|
379 evs \<in> bankerb_gets \<rbrakk> |
|
380 \<Longrightarrow> Key K \<in> analz (knows B evs)" |
|
381 apply (force dest: Gets_imp_knows_analz) |
|
382 done |
|
383 |
|
384 |
|
385 (**** |
|
386 The following is to prove theorems of the form |
|
387 |
|
388 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> |
|
389 Key K \<in> analz (knows Spy evs) |
|
390 |
|
391 A more general formula must be proved inductively. |
|
392 |
|
393 ****) |
|
394 |
|
395 |
|
396 text{* Session keys are not used to encrypt other session keys *} |
|
397 lemma analz_image_freshK [rule_format (no_asm)]: |
|
398 "evs \<in> bankerb_gets \<Longrightarrow> |
|
399 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> |
|
400 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
401 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
402 apply (erule bankerb_gets.induct) |
|
403 apply (drule_tac [8] Says_Server_message_form) |
|
404 apply (erule_tac [6] Gets_Server_message_form [THEN disjE], analz_freshK, spy_analz, auto) |
|
405 done |
|
406 |
|
407 |
|
408 lemma analz_insert_freshK: |
|
409 "\<lbrakk> evs \<in> bankerb_gets; KAB \<notin> range shrK \<rbrakk> \<Longrightarrow> |
|
410 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
|
411 (K = KAB | Key K \<in> analz (knows Spy evs))" |
|
412 by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
413 |
|
414 |
|
415 text{* The session key K uniquely identifies the message *} |
|
416 lemma unique_session_keys: |
|
417 "\<lbrakk> Says Server A |
|
418 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
419 Says Server A' |
|
420 (Crypt (shrK A') \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs; |
|
421 evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> A=A' & Tk=Tk' & B=B' & X = X'" |
|
422 apply (erule rev_mp) |
|
423 apply (erule rev_mp) |
|
424 apply (erule bankerb_gets.induct) |
|
425 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
426 apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all) |
|
427 txt{*BK2: it can't be a new key*} |
|
428 apply blast |
|
429 done |
|
430 |
|
431 lemma unique_session_keys_Gets: |
|
432 "\<lbrakk> Gets A |
|
433 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
434 Gets A |
|
435 (Crypt (shrK A) \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs; |
|
436 A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> Tk=Tk' & B=B' & X = X'" |
|
437 apply (blast dest!: Kab_authentic unique_session_keys) |
|
438 done |
|
439 |
|
440 |
|
441 lemma Server_Unique: |
|
442 "\<lbrakk> Says Server A |
|
443 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
444 evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> |
|
445 Unique Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
446 on evs" |
|
447 apply (erule rev_mp, erule bankerb_gets.induct, simp_all add: Unique_def) |
|
448 apply blast |
|
449 done |
|
450 |
|
451 |
|
452 |
|
453 subsection{*Non-temporal guarantees, explicitly relying on non-occurrence of |
|
454 oops events - refined below by temporal guarantees*} |
|
455 |
|
456 text{*Non temporal treatment of confidentiality*} |
|
457 |
|
458 text{* Lemma: the session key sent in msg BK2 would be lost by oops |
|
459 if the spy could see it! *} |
|
460 lemma lemma_conf [rule_format (no_asm)]: |
|
461 "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
462 \<Longrightarrow> Says Server A |
|
463 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
464 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
465 \<in> set evs \<longrightarrow> |
|
466 Key K \<in> analz (knows Spy evs) \<longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<in> set evs" |
|
467 apply (erule bankerb_gets.induct) |
|
468 apply (frule_tac [8] Says_Server_message_form) |
|
469 apply (frule_tac [6] Gets_Server_message_form [THEN disjE]) |
|
470 apply (simp_all (no_asm_simp) add: analz_insert_eq analz_insert_freshK pushes) |
|
471 txt{*Fake*} |
|
472 apply spy_analz |
|
473 txt{*BK2*} |
|
474 apply (blast intro: parts_insertI) |
|
475 txt{*BK3*} |
|
476 apply (case_tac "Aa \<in> bad") |
|
477 prefer 2 apply (blast dest: Kab_authentic unique_session_keys) |
|
478 apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz) |
|
479 txt{*Oops*} |
|
480 apply (blast dest: unique_session_keys) |
|
481 done |
|
482 |
|
483 |
|
484 text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2 |
|
485 as long as they have not expired.*} |
|
486 lemma Confidentiality_S: |
|
487 "\<lbrakk> Says Server A |
|
488 (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
489 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
490 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets |
|
491 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
|
492 apply (frule Says_Server_message_form, assumption) |
|
493 apply (blast intro: lemma_conf) |
|
494 done |
|
495 |
|
496 text{*Confidentiality for Alice*} |
|
497 lemma Confidentiality_A: |
|
498 "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs); |
|
499 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
500 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets |
|
501 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
|
502 by (blast dest!: Kab_authentic Confidentiality_S) |
|
503 |
|
504 text{*Confidentiality for Bob*} |
|
505 lemma Confidentiality_B: |
|
506 "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
507 \<in> parts (knows Spy evs); |
|
508 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
509 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets |
|
510 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
|
511 by (blast dest!: ticket_authentic Confidentiality_S) |
|
512 |
|
513 |
|
514 text{*Non temporal treatment of authentication*} |
|
515 |
|
516 text{*Lemmas @{text lemma_A} and @{text lemma_B} in fact are common to both temporal and non-temporal treatments*} |
|
517 lemma lemma_A [rule_format]: |
|
518 "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
519 \<Longrightarrow> |
|
520 Key K \<notin> analz (knows Spy evs) \<longrightarrow> |
|
521 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
522 \<in> set evs \<longrightarrow> |
|
523 Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> |
|
524 Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> |
|
525 \<in> set evs" |
|
526 apply (erule bankerb_gets.induct) |
|
527 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
528 apply (frule_tac [6] Gets_Server_message_form) |
|
529 apply (frule_tac [7] BK3_msg_in_parts_knows_Spy, analz_mono_contra) |
|
530 apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
531 txt{*Fake*} |
|
532 apply blast |
|
533 txt{*BK2*} |
|
534 apply (force dest: Crypt_imp_invKey_keysFor) |
|
535 txt{*BK3*} |
|
536 apply (blast dest: Kab_authentic unique_session_keys) |
|
537 done |
|
538 lemma lemma_B [rule_format]: |
|
539 "\<lbrakk> B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
540 \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow> |
|
541 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
542 \<in> set evs \<longrightarrow> |
|
543 Crypt K (Number Ta) \<in> parts (knows Spy evs) \<longrightarrow> |
|
544 Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
545 apply (erule bankerb_gets.induct) |
|
546 apply (frule_tac [8] Oops_parts_knows_Spy) |
|
547 apply (frule_tac [6] Gets_Server_message_form) |
|
548 apply (drule_tac [7] BK3_msg_in_parts_knows_Spy, analz_mono_contra) |
|
549 apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
550 txt{*Fake*} |
|
551 apply blast |
|
552 txt{*BK2*} |
|
553 apply (force dest: Crypt_imp_invKey_keysFor) |
|
554 txt{*BK4*} |
|
555 apply (blast dest: ticket_authentic unique_session_keys |
|
556 Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad) |
|
557 done |
|
558 |
|
559 |
|
560 text{*The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
|
561 |
|
562 text{*Authentication of A to B*} |
|
563 lemma B_authenticates_A_r: |
|
564 "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs); |
|
565 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); |
|
566 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
567 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
568 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
569 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
570 by (blast dest!: ticket_authentic |
|
571 intro!: lemma_A |
|
572 elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
573 |
|
574 text{*Authentication of B to A*} |
|
575 lemma A_authenticates_B_r: |
|
576 "\<lbrakk> Crypt K (Number Ta) \<in> parts (knows Spy evs); |
|
577 Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs); |
|
578 Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
579 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
580 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
581 by (blast dest!: Kab_authentic |
|
582 intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
583 |
|
584 lemma B_authenticates_A: |
|
585 "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
586 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
587 Key K \<notin> analz (spies evs); |
|
588 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
589 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
590 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
591 apply (blast dest!: ticket_authentic intro!: lemma_A) |
|
592 done |
|
593 |
|
594 lemma A_authenticates_B: |
|
595 "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
596 Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
597 Key K \<notin> analz (spies evs); |
|
598 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
599 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
600 apply (blast dest!: Kab_authentic intro!: lemma_B) |
|
601 done |
|
602 |
|
603 |
|
604 subsection{*Temporal guarantees, relying on a temporal check that insures that |
|
605 no oops event occurred. These are available in the sense of goal availability*} |
|
606 |
|
607 |
|
608 text{*Temporal treatment of confidentiality*} |
|
609 |
|
610 text{* Lemma: the session key sent in msg BK2 would be EXPIRED |
|
611 if the spy could see it! *} |
|
612 lemma lemma_conf_temporal [rule_format (no_asm)]: |
|
613 "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
614 \<Longrightarrow> Says Server A |
|
615 (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
616 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
617 \<in> set evs \<longrightarrow> |
|
618 Key K \<in> analz (knows Spy evs) \<longrightarrow> expiredK Tk evs" |
|
619 apply (erule bankerb_gets.induct) |
|
620 apply (frule_tac [8] Says_Server_message_form) |
|
621 apply (frule_tac [6] Gets_Server_message_form [THEN disjE]) |
|
622 apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) |
|
623 txt{*Fake*} |
|
624 apply spy_analz |
|
625 txt{*BK2*} |
|
626 apply (blast intro: parts_insertI less_SucI) |
|
627 txt{*BK3*} |
|
628 apply (case_tac "Aa \<in> bad") |
|
629 prefer 2 apply (blast dest: Kab_authentic unique_session_keys) |
|
630 apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) |
|
631 txt{*Oops: PROOF FAILS if unsafe intro below*} |
|
632 apply (blast dest: unique_session_keys intro!: less_SucI) |
|
633 done |
|
634 |
|
635 |
|
636 text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2 |
|
637 as long as they have not expired.*} |
|
638 lemma Confidentiality_S_temporal: |
|
639 "\<lbrakk> Says Server A |
|
640 (Crypt K' \<lbrace>Number T, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
641 \<not> expiredK T evs; |
|
642 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets |
|
643 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
|
644 apply (frule Says_Server_message_form, assumption) |
|
645 apply (blast intro: lemma_conf_temporal) |
|
646 done |
|
647 |
|
648 text{*Confidentiality for Alice*} |
|
649 lemma Confidentiality_A_temporal: |
|
650 "\<lbrakk> Crypt (shrK A) \<lbrace>Number T, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs); |
|
651 \<not> expiredK T evs; |
|
652 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets |
|
653 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
|
654 by (blast dest!: Kab_authentic Confidentiality_S_temporal) |
|
655 |
|
656 text{*Confidentiality for Bob*} |
|
657 lemma Confidentiality_B_temporal: |
|
658 "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
659 \<in> parts (knows Spy evs); |
|
660 \<not> expiredK Tk evs; |
|
661 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets |
|
662 \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
|
663 by (blast dest!: ticket_authentic Confidentiality_S_temporal) |
|
664 |
|
665 |
|
666 text{*Temporal treatment of authentication*} |
|
667 |
|
668 text{*Authentication of A to B*} |
|
669 lemma B_authenticates_A_temporal: |
|
670 "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs); |
|
671 Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
672 \<in> parts (knows Spy evs); |
|
673 \<not> expiredK Tk evs; |
|
674 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
675 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
676 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
677 by (blast dest!: ticket_authentic |
|
678 intro!: lemma_A |
|
679 elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) |
|
680 |
|
681 text{*Authentication of B to A*} |
|
682 lemma A_authenticates_B_temporal: |
|
683 "\<lbrakk> Crypt K (Number Ta) \<in> parts (knows Spy evs); |
|
684 Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> |
|
685 \<in> parts (knows Spy evs); |
|
686 \<not> expiredK Tk evs; |
|
687 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
688 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
689 by (blast dest!: Kab_authentic |
|
690 intro!: lemma_B elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) |
|
691 |
|
692 |
|
693 subsection{*Combined guarantees of key distribution and non-injective agreement on the session keys*} |
|
694 |
|
695 lemma B_authenticates_and_keydist_to_A: |
|
696 "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
697 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs; |
|
698 Key K \<notin> analz (spies evs); |
|
699 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
700 \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
701 Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs |
|
702 \<and> Key K \<in> analz (knows A evs)" |
|
703 apply (blast dest: B_authenticates_A BK3_imp_Gets Gets_A_knows_K) |
|
704 done |
|
705 |
|
706 lemma A_authenticates_and_keydist_to_B: |
|
707 "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
708 Gets A (Crypt K (Number Ta)) \<in> set evs; |
|
709 Key K \<notin> analz (spies evs); |
|
710 A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk> |
|
711 \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs |
|
712 \<and> Key K \<in> analz (knows B evs)" |
|
713 apply (blast dest: A_authenticates_B BK4_imp_Gets Gets_B_knows_K) |
|
714 done |
|
715 |
|
716 |
|
717 |
|
718 |
|
719 |
|
720 end |