65 Kb1: "[| evs1 \<in> kerberos_ban |] |
66 Kb1: "[| evs1 \<in> kerberos_ban |] |
66 ==> Says A Server {|Agent A, Agent B|} # evs1 |
67 ==> Says A Server {|Agent A, Agent B|} # evs1 |
67 \<in> kerberos_ban" |
68 \<in> kerberos_ban" |
68 |
69 |
69 |
70 |
70 Kb2: "[| evs2 \<in> kerberos_ban; Key KAB \<notin> used evs2; |
71 Kb2: "[| evs2 \<in> kerberos_ban; Key KAB \<notin> used evs2; KAB \<in> symKeys; |
71 Says A' Server {|Agent A, Agent B|} \<in> set evs2 |] |
72 Says A' Server {|Agent A, Agent B|} \<in> set evs2 |] |
72 ==> Says Server A |
73 ==> Says Server A |
73 (Crypt (shrK A) |
74 (Crypt (shrK A) |
74 {|Number (CT evs2), Agent B, Key KAB, |
75 {|Number (CT evs2), Agent B, Key KAB, |
75 (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) |
76 (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) |
76 # evs2 \<in> kerberos_ban" |
77 # evs2 \<in> kerberos_ban" |
77 |
78 |
78 |
79 |
79 Kb3: "[| evs3 \<in> kerberos_ban; |
80 Kb3: "[| evs3 \<in> kerberos_ban; |
80 Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
81 Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
81 \<in> set evs3; |
82 \<in> set evs3; |
82 Says A Server {|Agent A, Agent B|} \<in> set evs3; |
83 Says A Server {|Agent A, Agent B|} \<in> set evs3; |
83 ~ Expired Ts evs3 |] |
84 ~ Expired Ts evs3 |] |
84 ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} |
85 ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} |
85 # evs3 \<in> kerberos_ban" |
86 # evs3 \<in> kerberos_ban" |
86 |
87 |
87 |
88 |
88 Kb4: "[| evs4 \<in> kerberos_ban; |
89 Kb4: "[| evs4 \<in> kerberos_ban; |
89 Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), |
90 Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), |
90 (Crypt K {|Agent A, Number Ta|}) |}: set evs4; |
91 (Crypt K {|Agent A, Number Ta|}) |}: set evs4; |
91 ~ Expired Ts evs4; RecentAuth Ta evs4 |] |
92 ~ Expired Ts evs4; RecentAuth Ta evs4 |] |
92 ==> Says B A (Crypt K (Number Ta)) # evs4 |
93 ==> Says B A (Crypt K (Number Ta)) # evs4 |
93 \<in> kerberos_ban" |
94 \<in> kerberos_ban" |
94 |
95 |
95 (*Old session keys may become compromised*) |
96 (*Old session keys may become compromised*) |
96 Oops: "[| evso \<in> kerberos_ban; |
97 Oops: "[| evso \<in> kerberos_ban; |
97 Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
98 Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
98 \<in> set evso; |
99 \<in> set evso; |
99 Expired Ts evso |] |
100 Expired Ts evso |] |
100 ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban" |
101 ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban" |
101 |
102 |
102 |
103 |
103 declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
104 declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
104 declare parts.Body [dest] |
105 declare parts.Body [dest] |
105 declare analz_into_parts [dest] |
106 declare analz_into_parts [dest] |
106 declare Fake_parts_insert_in_Un [dest] |
107 declare Fake_parts_insert_in_Un [dest] |
107 |
108 |
108 (*A "possibility property": there are traces that reach the end.*) |
109 text{*A "possibility property": there are traces that reach the end.*} |
109 lemma "Key K \<notin> used [] |
110 lemma "[|Key K \<notin> used []; K \<in> symKeys|] |
110 ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban. |
111 ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban. |
111 Says B A (Crypt K (Number Timestamp)) |
112 Says B A (Crypt K (Number Timestamp)) |
112 \<in> set evs" |
113 \<in> set evs" |
113 apply (cut_tac SesKeyLife_LB) |
114 apply (cut_tac SesKeyLife_LB) |
114 apply (intro exI bexI) |
115 apply (intro exI bexI) |
115 apply (rule_tac [2] |
116 apply (rule_tac [2] |
116 kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, |
117 kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, |
117 THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4]) |
118 THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4]) |
118 apply (possibility, simp_all (no_asm_simp) add: used_Cons) |
119 apply (possibility, simp_all (no_asm_simp) add: used_Cons) |
119 done |
120 done |
120 |
121 |
121 |
122 |
122 (**** Inductive proofs about kerberos_ban ****) |
123 (**** Inductive proofs about kerberos_ban ****) |
123 |
124 |
124 (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*) |
125 text{*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*} |
125 lemma Kb3_msg_in_parts_spies: |
126 lemma Kb3_msg_in_parts_spies: |
126 "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs |
127 "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs |
127 ==> X \<in> parts (spies evs)" |
128 ==> X \<in> parts (spies evs)" |
128 by blast |
129 by blast |
129 |
130 |
130 lemma Oops_parts_spies: |
131 lemma Oops_parts_spies: |
131 "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs |
132 "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs |
132 ==> K \<in> parts (spies evs)" |
133 ==> K \<in> parts (spies evs)" |
133 by blast |
134 by blast |
134 |
135 |
135 |
136 |
136 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
137 text{*Spy never sees another agent's shared key! (unless it's bad at start)*} |
137 lemma Spy_see_shrK [simp]: |
138 lemma Spy_see_shrK [simp]: |
138 "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
139 "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
139 apply (erule kerberos_ban.induct) |
140 apply (erule kerberos_ban.induct) |
140 apply (frule_tac [7] Oops_parts_spies) |
141 apply (frule_tac [7] Oops_parts_spies) |
141 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
142 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast+) |
142 apply blast+ |
|
143 done |
143 done |
144 |
144 |
145 |
145 |
146 lemma Spy_analz_shrK [simp]: |
146 lemma Spy_analz_shrK [simp]: |
147 "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
147 "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
148 apply auto |
148 by auto |
149 done |
|
150 |
|
151 |
149 |
152 lemma Spy_see_shrK_D [dest!]: |
150 lemma Spy_see_shrK_D [dest!]: |
153 "[| Key (shrK A) \<in> parts (spies evs); |
151 "[| Key (shrK A) \<in> parts (spies evs); |
154 evs \<in> kerberos_ban |] ==> A:bad" |
152 evs \<in> kerberos_ban |] ==> A:bad" |
155 apply (blast dest: Spy_see_shrK) |
153 by (blast dest: Spy_see_shrK) |
156 done |
|
157 |
154 |
158 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] |
155 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] |
159 |
156 |
160 |
157 |
161 (*Nobody can have used non-existent keys!*) |
158 text{*Nobody can have used non-existent keys!*} |
162 lemma new_keys_not_used [rule_format, simp]: |
159 lemma new_keys_not_used [simp]: |
163 "evs \<in> kerberos_ban ==> |
160 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerberos_ban|] |
164 Key K \<notin> used evs --> K \<notin> keysFor (parts (spies evs))" |
161 ==> K \<notin> keysFor (parts (spies evs))" |
165 apply (erule kerberos_ban.induct) |
162 apply (erule rev_mp) |
166 apply (frule_tac [7] Oops_parts_spies) |
163 apply (erule kerberos_ban.induct) |
167 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
164 apply (frule_tac [7] Oops_parts_spies) |
168 (*Fake*) |
165 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
|
166 txt{*Fake*} |
169 apply (force dest!: keysFor_parts_insert) |
167 apply (force dest!: keysFor_parts_insert) |
170 (*Kb2, Kb3, Kb4*) |
168 txt{*Kb2, Kb3, Kb4*} |
171 apply blast+ |
169 apply (force dest!: analz_shrK_Decrypt)+ |
172 done |
170 done |
173 |
171 |
174 (** Lemmas concerning the form of items passed in messages **) |
172 subsection{* Lemmas concerning the form of items passed in messages *} |
175 |
173 |
176 (*Describes the form of K, X and K' when the Server sends this message.*) |
174 text{*Describes the form of K, X and K' when the Server sends this message.*} |
177 lemma Says_Server_message_form: |
175 lemma Says_Server_message_form: |
178 "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) |
176 "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) |
179 \<in> set evs; evs \<in> kerberos_ban |] |
177 \<in> set evs; evs \<in> kerberos_ban |] |
180 ==> K \<notin> range shrK & |
178 ==> K \<notin> range shrK & |
181 X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & |
179 X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & |
182 K' = shrK A" |
180 K' = shrK A" |
183 apply (erule rev_mp) |
181 apply (erule rev_mp) |
184 apply (erule kerberos_ban.induct, auto) |
182 apply (erule kerberos_ban.induct, auto) |
185 done |
183 done |
186 |
184 |
187 |
185 |
188 (*If the encrypted message appears then it originated with the Server |
186 text{*If the encrypted message appears then it originated with the Server |
189 PROVIDED that A is NOT compromised! |
187 PROVIDED that A is NOT compromised! |
190 |
188 |
191 This shows implicitly the FRESHNESS OF THE SESSION KEY to A |
189 This shows implicitly the FRESHNESS OF THE SESSION KEY to A |
192 *) |
190 *} |
193 lemma A_trusts_K_by_Kb2: |
191 lemma A_trusts_K_by_Kb2: |
194 "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} |
192 "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} |
195 \<in> parts (spies evs); |
193 \<in> parts (spies evs); |
196 A \<notin> bad; evs \<in> kerberos_ban |] |
194 A \<notin> bad; evs \<in> kerberos_ban |] |
197 ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
195 ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
198 \<in> set evs" |
196 \<in> set evs" |
199 apply (erule rev_mp) |
197 apply (erule rev_mp) |
200 apply (erule kerberos_ban.induct) |
198 apply (erule kerberos_ban.induct) |
201 apply (frule_tac [7] Oops_parts_spies) |
199 apply (frule_tac [7] Oops_parts_spies) |
202 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
200 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast) |
203 apply blast |
201 done |
204 done |
202 |
205 |
203 |
206 |
204 text{*If the TICKET appears then it originated with the Server*} |
207 (*If the TICKET appears then it originated with the Server*) |
205 text{*FRESHNESS OF THE SESSION KEY to B*} |
208 (*FRESHNESS OF THE SESSION KEY to B*) |
|
209 lemma B_trusts_K_by_Kb3: |
206 lemma B_trusts_K_by_Kb3: |
210 "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs); |
207 "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs); |
211 B \<notin> bad; evs \<in> kerberos_ban |] |
208 B \<notin> bad; evs \<in> kerberos_ban |] |
212 ==> Says Server A |
209 ==> Says Server A |
213 (Crypt (shrK A) {|Number Ts, Agent B, Key K, |
210 (Crypt (shrK A) {|Number Ts, Agent B, Key K, |
214 Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) |
211 Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) |
215 \<in> set evs" |
212 \<in> set evs" |
216 apply (erule rev_mp) |
213 apply (erule rev_mp) |
217 apply (erule kerberos_ban.induct) |
214 apply (erule kerberos_ban.induct) |
218 apply (frule_tac [7] Oops_parts_spies) |
215 apply (frule_tac [7] Oops_parts_spies) |
219 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
216 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast) |
220 apply blast |
217 done |
221 done |
218 |
222 |
219 |
223 |
220 text{*EITHER describes the form of X when the following message is sent, |
224 (*EITHER describes the form of X when the following message is sent, |
|
225 OR reduces it to the Fake case. |
221 OR reduces it to the Fake case. |
226 Use Says_Server_message_form if applicable.*) |
222 Use @{text Says_Server_message_form} if applicable.*} |
227 lemma Says_S_message_form: |
223 lemma Says_S_message_form: |
228 "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
224 "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
229 \<in> set evs; |
225 \<in> set evs; |
230 evs \<in> kerberos_ban |] |
226 evs \<in> kerberos_ban |] |
231 ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|})) |
227 ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|})) |
232 | X \<in> analz (spies evs)" |
228 | X \<in> analz (spies evs)" |
233 apply (case_tac "A \<in> bad") |
229 apply (case_tac "A \<in> bad") |
234 apply (force dest!: Says_imp_spies [THEN analz.Inj]) |
230 apply (force dest!: Says_imp_spies [THEN analz.Inj]) |
235 apply (frule Says_imp_spies [THEN parts.Inj]) |
231 apply (frule Says_imp_spies [THEN parts.Inj]) |
236 apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form) |
232 apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form) |
246 |
242 |
247 A more general formula must be proved inductively. |
243 A more general formula must be proved inductively. |
248 |
244 |
249 ****) |
245 ****) |
250 |
246 |
251 |
247 text{* Session keys are not used to encrypt other session keys *} |
252 (** Session keys are not used to encrypt other session keys **) |
|
253 |
|
254 lemma analz_image_freshK [rule_format (no_asm)]: |
248 lemma analz_image_freshK [rule_format (no_asm)]: |
255 "evs \<in> kerberos_ban ==> |
249 "evs \<in> kerberos_ban ==> |
256 \<forall>K KK. KK \<subseteq> - (range shrK) --> |
250 \<forall>K KK. KK \<subseteq> - (range shrK) --> |
257 (Key K \<in> analz (Key`KK Un (spies evs))) = |
251 (Key K \<in> analz (Key`KK Un (spies evs))) = |
258 (K \<in> KK | Key K \<in> analz (spies evs))" |
252 (K \<in> KK | Key K \<in> analz (spies evs))" |
259 apply (erule kerberos_ban.induct) |
253 apply (erule kerberos_ban.induct) |
260 apply (drule_tac [7] Says_Server_message_form) |
254 apply (drule_tac [7] Says_Server_message_form) |
261 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz) |
255 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) |
262 done |
256 done |
263 |
|
264 |
257 |
265 |
258 |
266 lemma analz_insert_freshK: |
259 lemma analz_insert_freshK: |
267 "[| evs \<in> kerberos_ban; KAB \<notin> range shrK |] ==> |
260 "[| evs \<in> kerberos_ban; KAB \<notin> range shrK |] ==> |
268 (Key K \<in> analz (insert (Key KAB) (spies evs))) = |
261 (Key K \<in> analz (insert (Key KAB) (spies evs))) = |
269 (K = KAB | Key K \<in> analz (spies evs))" |
262 (K = KAB | Key K \<in> analz (spies evs))" |
270 by (simp only: analz_image_freshK analz_image_freshK_simps) |
263 by (simp only: analz_image_freshK analz_image_freshK_simps) |
271 |
264 |
272 |
265 |
273 (** The session key K uniquely identifies the message **) |
266 text{* The session key K uniquely identifies the message *} |
274 |
|
275 lemma unique_session_keys: |
267 lemma unique_session_keys: |
276 "[| Says Server A |
268 "[| Says Server A |
277 (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs; |
269 (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs; |
278 Says Server A' |
270 Says Server A' |
279 (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs; |
271 (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs; |
280 evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'" |
272 evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'" |
281 apply (erule rev_mp) |
273 apply (erule rev_mp) |
282 apply (erule rev_mp) |
274 apply (erule rev_mp) |
283 apply (erule kerberos_ban.induct) |
275 apply (erule kerberos_ban.induct) |
284 apply (frule_tac [7] Oops_parts_spies) |
276 apply (frule_tac [7] Oops_parts_spies) |
285 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
277 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
286 (*Kb2: it can't be a new key*) |
278 txt{*Kb2: it can't be a new key*} |
287 apply blast |
279 apply blast |
288 done |
280 done |
289 |
281 |
290 |
282 |
291 (** Lemma: the session key sent in msg Kb2 would be EXPIRED |
283 text{* Lemma: the session key sent in msg Kb2 would be EXPIRED |
292 if the spy could see it! |
284 if the spy could see it! *} |
293 **) |
|
294 |
285 |
295 lemma lemma2 [rule_format (no_asm)]: |
286 lemma lemma2 [rule_format (no_asm)]: |
296 "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
287 "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
297 ==> Says Server A |
288 ==> Says Server A |
298 (Crypt (shrK A) {|Number Ts, Agent B, Key K, |
289 (Crypt (shrK A) {|Number Ts, Agent B, Key K, |
299 Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) |
290 Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) |
300 \<in> set evs --> |
291 \<in> set evs --> |
301 Key K \<in> analz (spies evs) --> Expired Ts evs" |
292 Key K \<in> analz (spies evs) --> Expired Ts evs" |
302 apply (erule kerberos_ban.induct) |
293 apply (erule kerberos_ban.induct) |
303 apply (frule_tac [7] Says_Server_message_form) |
294 apply (frule_tac [7] Says_Server_message_form) |
304 apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
295 apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
305 apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) |
296 apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) |
314 txt{*Oops: PROOF FAILED if addIs below*} |
305 txt{*Oops: PROOF FAILED if addIs below*} |
315 apply (blast dest: unique_session_keys intro!: less_SucI) |
306 apply (blast dest: unique_session_keys intro!: less_SucI) |
316 done |
307 done |
317 |
308 |
318 |
309 |
319 (** CONFIDENTIALITY for the SERVER: |
310 text{*Confidentiality for the Server: Spy does not see the keys sent in msg Kb2 |
320 Spy does not see the keys sent in msg Kb2 |
311 as long as they have not expired.*} |
321 as long as they have NOT EXPIRED |
|
322 **) |
|
323 lemma Confidentiality_S: |
312 lemma Confidentiality_S: |
324 "[| Says Server A |
313 "[| Says Server A |
325 (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs; |
314 (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs; |
326 ~ Expired T evs; |
315 ~ Expired T evs; |
327 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
316 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
328 |] ==> Key K \<notin> analz (spies evs)" |
317 |] ==> Key K \<notin> analz (spies evs)" |
329 apply (frule Says_Server_message_form, assumption) |
318 apply (frule Says_Server_message_form, assumption) |
330 apply (blast intro: lemma2) |
319 apply (blast intro: lemma2) |
331 done |
320 done |
332 |
321 |
333 (**** THE COUNTERPART OF CONFIDENTIALITY |
322 (**** THE COUNTERPART OF CONFIDENTIALITY |
334 [|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs) |
323 [|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs) |
335 WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) |
324 WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) |
336 |
325 |
337 |
326 |
338 (** CONFIDENTIALITY for ALICE: **) |
327 text{*Confidentiality for Alice*} |
339 (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **) |
|
340 lemma Confidentiality_A: |
328 lemma Confidentiality_A: |
341 "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs); |
329 "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs); |
342 ~ Expired T evs; |
330 ~ Expired T evs; |
343 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
331 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
344 |] ==> Key K \<notin> analz (spies evs)" |
332 |] ==> Key K \<notin> analz (spies evs)" |
345 apply (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S) |
333 by (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S) |
346 done |
334 |
347 |
335 |
348 |
336 text{*Confidentiality for Bob*} |
349 (** CONFIDENTIALITY for BOB: **) |
|
350 (** Also B_trusts_K_by_Kb3 RS Confidentiality_S **) |
|
351 lemma Confidentiality_B: |
337 lemma Confidentiality_B: |
352 "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} |
338 "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} |
353 \<in> parts (spies evs); |
339 \<in> parts (spies evs); |
354 ~ Expired Tk evs; |
340 ~ Expired Tk evs; |
355 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
341 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
356 |] ==> Key K \<notin> analz (spies evs)" |
342 |] ==> Key K \<notin> analz (spies evs)" |
357 apply (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S) |
343 by (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S) |
358 done |
|
359 |
344 |
360 |
345 |
361 lemma lemma_B [rule_format]: |
346 lemma lemma_B [rule_format]: |
362 "[| B \<notin> bad; evs \<in> kerberos_ban |] |
347 "[| B \<notin> bad; evs \<in> kerberos_ban |] |
363 ==> Key K \<notin> analz (spies evs) --> |
348 ==> Key K \<notin> analz (spies evs) --> |
364 Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
349 Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
365 \<in> set evs --> |
350 \<in> set evs --> |
366 Crypt K (Number Ta) \<in> parts (spies evs) --> |
351 Crypt K (Number Ta) \<in> parts (spies evs) --> |
367 Says B A (Crypt K (Number Ta)) \<in> set evs" |
352 Says B A (Crypt K (Number Ta)) \<in> set evs" |
368 apply (erule kerberos_ban.induct) |
353 apply (erule kerberos_ban.induct) |
369 apply (frule_tac [7] Oops_parts_spies) |
354 apply (frule_tac [7] Oops_parts_spies) |
370 apply (frule_tac [5] Says_S_message_form) |
355 apply (frule_tac [5] Says_S_message_form) |
371 apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) |
356 apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) |
372 apply (simp_all (no_asm_simp) add: all_conj_distrib) |
357 apply (simp_all (no_asm_simp) add: all_conj_distrib) |
373 txt{*Fake*} |
358 txt{*Fake*} |
374 apply blast |
359 apply blast |
375 txt{*Kb2*} |
360 txt{*Kb2*} |
376 apply (force dest: Crypt_imp_invKey_keysFor) |
361 apply (force dest: Crypt_imp_invKey_keysFor) |
377 txt{*Kb4*} |
362 txt{*Kb4*} |
378 apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys |
363 apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys |
379 Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad) |
364 Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad) |
380 done |
365 done |
381 |
366 |
382 |
367 |
383 (*AUTHENTICATION OF B TO A*) |
368 text{*Authentication of B to A*} |
384 lemma Authentication_B: |
369 lemma Authentication_B: |
385 "[| Crypt K (Number Ta) \<in> parts (spies evs); |
370 "[| Crypt K (Number Ta) \<in> parts (spies evs); |
386 Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} |
371 Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} |
387 \<in> parts (spies evs); |
372 \<in> parts (spies evs); |
388 ~ Expired Ts evs; |
373 ~ Expired Ts evs; |
389 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
374 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
390 ==> Says B A (Crypt K (Number Ta)) \<in> set evs" |
375 ==> Says B A (Crypt K (Number Ta)) \<in> set evs" |
391 by (blast dest!: A_trusts_K_by_Kb2 |
376 by (blast dest!: A_trusts_K_by_Kb2 |
392 intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) |
377 intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) |
393 |
378 |
394 |
|
395 |
|
396 lemma lemma_A [rule_format]: |
379 lemma lemma_A [rule_format]: |
397 "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
380 "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
398 ==> |
381 ==> |
399 Key K \<notin> analz (spies evs) --> |
382 Key K \<notin> analz (spies evs) --> |
400 Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
383 Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
401 \<in> set evs --> |
384 \<in> set evs --> |
402 Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) --> |
385 Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) --> |
403 Says A B {|X, Crypt K {|Agent A, Number Ta|}|} |
386 Says A B {|X, Crypt K {|Agent A, Number Ta|}|} |
404 \<in> set evs" |
387 \<in> set evs" |
405 apply (erule kerberos_ban.induct) |
388 apply (erule kerberos_ban.induct) |
406 apply (frule_tac [7] Oops_parts_spies) |
389 apply (frule_tac [7] Oops_parts_spies) |
407 apply (frule_tac [5] Says_S_message_form) |
390 apply (frule_tac [5] Says_S_message_form) |
408 apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) |
391 apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) |
409 apply (simp_all (no_asm_simp) add: all_conj_distrib) |
392 apply (simp_all (no_asm_simp) add: all_conj_distrib) |
410 txt{*Fake*} |
393 txt{*Fake*} |
411 apply blast |
394 apply blast |
412 txt{*Kb2*} |
395 txt{*Kb2*} |
413 apply (force dest: Crypt_imp_invKey_keysFor) |
396 apply (force dest: Crypt_imp_invKey_keysFor) |
414 txt{*Kb3*} |
397 txt{*Kb3*} |
415 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys) |
398 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys) |
416 done |
399 done |
417 |
400 |
418 |
401 text{*Authentication of A to B*} |
419 (*AUTHENTICATION OF A TO B*) |
|
420 lemma Authentication_A: |
402 lemma Authentication_A: |
421 "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs); |
403 "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs); |
422 Crypt (shrK B) {|Number Ts, Agent A, Key K|} |
404 Crypt (shrK B) {|Number Ts, Agent A, Key K|} |
423 \<in> parts (spies evs); |
405 \<in> parts (spies evs); |
424 ~ Expired Ts evs; |
406 ~ Expired Ts evs; |
425 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
407 A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
426 ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, |
408 ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, |
427 Crypt K {|Agent A, Number Ta|}|} \<in> set evs" |
409 Crypt K {|Agent A, Number Ta|}|} \<in> set evs" |
428 by (blast dest!: B_trusts_K_by_Kb3 |
410 by (blast dest!: B_trusts_K_by_Kb3 |
429 intro!: lemma_A |
411 intro!: lemma_A |
430 elim!: Confidentiality_S [THEN [2] rev_notE]) |
412 elim!: Confidentiality_S [THEN [2] rev_notE]) |
431 |
413 |
432 end |
414 end |