18886
|
1 |
(* Title: HOL/Auth/KerberosIV
|
|
2 |
ID: $Id$
|
|
3 |
Author: Giampaolo Bella, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
header{*The Kerberos Protocol, Version IV*}
|
|
8 |
|
|
9 |
theory KerberosIV_Gets imports Public begin
|
|
10 |
|
|
11 |
text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
|
|
12 |
|
20768
|
13 |
abbreviation
|
18886
|
14 |
Kas :: agent
|
20768
|
15 |
"Kas == Server"
|
18886
|
16 |
|
20768
|
17 |
Tgs :: agent
|
|
18 |
"Tgs == Friend 0"
|
18886
|
19 |
|
|
20 |
|
|
21 |
axioms
|
|
22 |
Tgs_not_bad [iff]: "Tgs \<notin> bad"
|
|
23 |
--{*Tgs is secure --- we already know that Kas is secure*}
|
|
24 |
|
|
25 |
constdefs
|
|
26 |
(* authKeys are those contained in an authTicket *)
|
|
27 |
authKeys :: "event list => key set"
|
|
28 |
"authKeys evs == {authK. \<exists>A Peer Ta. Says Kas A
|
|
29 |
(Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
|
|
30 |
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
|
|
31 |
\<rbrace>) \<in> set evs}"
|
|
32 |
|
|
33 |
(* States than an event really appears only once on a trace *)
|
|
34 |
Unique :: "[event, event list] => bool" ("Unique _ on _")
|
|
35 |
"Unique ev on evs ==
|
|
36 |
ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
|
|
37 |
|
|
38 |
|
|
39 |
consts
|
|
40 |
(*Duration of the authentication key*)
|
|
41 |
authKlife :: nat
|
|
42 |
|
|
43 |
(*Duration of the service key*)
|
|
44 |
servKlife :: nat
|
|
45 |
|
|
46 |
(*Duration of an authenticator*)
|
|
47 |
authlife :: nat
|
|
48 |
|
|
49 |
(*Upper bound on the time of reaction of a server*)
|
|
50 |
replylife :: nat
|
|
51 |
|
|
52 |
specification (authKlife)
|
|
53 |
authKlife_LB [iff]: "2 \<le> authKlife"
|
|
54 |
by blast
|
|
55 |
|
|
56 |
specification (servKlife)
|
|
57 |
servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
|
|
58 |
by blast
|
|
59 |
|
|
60 |
specification (authlife)
|
|
61 |
authlife_LB [iff]: "Suc 0 \<le> authlife"
|
|
62 |
by blast
|
|
63 |
|
|
64 |
specification (replylife)
|
|
65 |
replylife_LB [iff]: "Suc 0 \<le> replylife"
|
|
66 |
by blast
|
|
67 |
|
20768
|
68 |
abbreviation
|
|
69 |
(*The current time is just the length of the trace!*)
|
|
70 |
CT :: "event list=>nat"
|
|
71 |
"CT == length"
|
18886
|
72 |
|
20768
|
73 |
expiredAK :: "[nat, event list] => bool"
|
|
74 |
"expiredAK Ta evs == authKlife + Ta < CT evs"
|
18886
|
75 |
|
20768
|
76 |
expiredSK :: "[nat, event list] => bool"
|
|
77 |
"expiredSK Ts evs == servKlife + Ts < CT evs"
|
18886
|
78 |
|
20768
|
79 |
expiredA :: "[nat, event list] => bool"
|
|
80 |
"expiredA T evs == authlife + T < CT evs"
|
18886
|
81 |
|
20768
|
82 |
valid :: "[nat, nat] => bool" ("valid _ wrt _")
|
|
83 |
"valid T1 wrt T2 == T1 <= replylife + T2"
|
18886
|
84 |
|
|
85 |
(*---------------------------------------------------------------------*)
|
|
86 |
|
|
87 |
|
|
88 |
(* Predicate formalising the association between authKeys and servKeys *)
|
|
89 |
constdefs
|
|
90 |
AKcryptSK :: "[key, key, event list] => bool"
|
|
91 |
"AKcryptSK authK servK evs ==
|
|
92 |
\<exists>A B Ts.
|
|
93 |
Says Tgs A (Crypt authK
|
|
94 |
\<lbrace>Key servK, Agent B, Number Ts,
|
|
95 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
|
|
96 |
\<in> set evs"
|
|
97 |
|
|
98 |
consts
|
|
99 |
|
|
100 |
kerbIV_gets :: "event list set"
|
|
101 |
inductive "kerbIV_gets"
|
|
102 |
intros
|
|
103 |
|
|
104 |
Nil: "[] \<in> kerbIV_gets"
|
|
105 |
|
|
106 |
Fake: "\<lbrakk> evsf \<in> kerbIV_gets; X \<in> synth (analz (spies evsf)) \<rbrakk>
|
|
107 |
\<Longrightarrow> Says Spy B X # evsf \<in> kerbIV_gets"
|
|
108 |
|
|
109 |
Reception: "\<lbrakk> evsr \<in> kerbIV_gets; Says A B X \<in> set evsr \<rbrakk>
|
|
110 |
\<Longrightarrow> Gets B X # evsr \<in> kerbIV_gets"
|
|
111 |
|
|
112 |
(* FROM the initiator *)
|
|
113 |
K1: "\<lbrakk> evs1 \<in> kerbIV_gets \<rbrakk>
|
|
114 |
\<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
|
|
115 |
\<in> kerbIV_gets"
|
|
116 |
|
|
117 |
(* Adding the timestamp serves to A in K3 to check that
|
|
118 |
she doesn't get a reply too late. This kind of timeouts are ordinary.
|
|
119 |
If a server's reply is late, then it is likely to be fake. *)
|
|
120 |
|
|
121 |
(*---------------------------------------------------------------------*)
|
|
122 |
|
|
123 |
(*FROM Kas *)
|
|
124 |
K2: "\<lbrakk> evs2 \<in> kerbIV_gets; Key authK \<notin> used evs2; authK \<in> symKeys;
|
|
125 |
Gets Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
|
|
126 |
\<Longrightarrow> Says Kas A
|
|
127 |
(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2),
|
|
128 |
(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
|
|
129 |
Number (CT evs2)\<rbrace>)\<rbrace>) # evs2 \<in> kerbIV_gets"
|
|
130 |
(*
|
|
131 |
The internal encryption builds the authTicket.
|
|
132 |
The timestamp doesn't change inside the two encryptions: the external copy
|
|
133 |
will be used by the initiator in K3; the one inside the
|
|
134 |
authTicket by Tgs in K4.
|
|
135 |
*)
|
|
136 |
|
|
137 |
(*---------------------------------------------------------------------*)
|
|
138 |
|
|
139 |
(* FROM the initiator *)
|
|
140 |
K3: "\<lbrakk> evs3 \<in> kerbIV_gets;
|
|
141 |
Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
|
|
142 |
Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
143 |
authTicket\<rbrace>) \<in> set evs3;
|
|
144 |
valid Ta wrt T1
|
|
145 |
\<rbrakk>
|
|
146 |
\<Longrightarrow> Says A Tgs \<lbrace>authTicket,
|
|
147 |
(Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
|
|
148 |
Agent B\<rbrace> # evs3 \<in> kerbIV_gets"
|
|
149 |
(*The two events amongst the premises allow A to accept only those authKeys
|
|
150 |
that are not issued late. *)
|
|
151 |
|
|
152 |
(*---------------------------------------------------------------------*)
|
|
153 |
|
|
154 |
(* FROM Tgs *)
|
|
155 |
(* Note that the last temporal check is not mentioned in the original MIT
|
|
156 |
specification. Adding it makes many goals "available" to the peers.
|
|
157 |
Theorems that exploit it have the suffix `_u', which stands for updated
|
|
158 |
protocol.
|
|
159 |
*)
|
|
160 |
K4: "\<lbrakk> evs4 \<in> kerbIV_gets; Key servK \<notin> used evs4; servK \<in> symKeys;
|
|
161 |
B \<noteq> Tgs; authK \<in> symKeys;
|
|
162 |
Gets Tgs \<lbrace>
|
|
163 |
(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
|
|
164 |
Number Ta\<rbrace>),
|
|
165 |
(Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
|
|
166 |
\<in> set evs4;
|
|
167 |
\<not> expiredAK Ta evs4;
|
|
168 |
\<not> expiredA T2 evs4;
|
|
169 |
servKlife + (CT evs4) <= authKlife + Ta
|
|
170 |
\<rbrakk>
|
|
171 |
\<Longrightarrow> Says Tgs A
|
|
172 |
(Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4),
|
|
173 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK,
|
|
174 |
Number (CT evs4)\<rbrace> \<rbrace>)
|
|
175 |
# evs4 \<in> kerbIV_gets"
|
|
176 |
(* Tgs creates a new session key per each request for a service, without
|
|
177 |
checking if there is still a fresh one for that service.
|
|
178 |
The cipher under Tgs' key is the authTicket, the cipher under B's key
|
|
179 |
is the servTicket, which is built now.
|
|
180 |
NOTE that the last temporal check is not present in the MIT specification.
|
|
181 |
|
|
182 |
*)
|
|
183 |
|
|
184 |
(*---------------------------------------------------------------------*)
|
|
185 |
|
|
186 |
(* FROM the initiator *)
|
|
187 |
K5: "\<lbrakk> evs5 \<in> kerbIV_gets; authK \<in> symKeys; servK \<in> symKeys;
|
|
188 |
Says A Tgs
|
|
189 |
\<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
|
|
190 |
Agent B\<rbrace>
|
|
191 |
\<in> set evs5;
|
|
192 |
Gets A
|
|
193 |
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
194 |
\<in> set evs5;
|
|
195 |
valid Ts wrt T2 \<rbrakk>
|
|
196 |
\<Longrightarrow> Says A B \<lbrace>servTicket,
|
|
197 |
Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
|
|
198 |
# evs5 \<in> kerbIV_gets"
|
|
199 |
(* Checks similar to those in K3. *)
|
|
200 |
|
|
201 |
(*---------------------------------------------------------------------*)
|
|
202 |
|
|
203 |
(* FROM the responder*)
|
|
204 |
K6: "\<lbrakk> evs6 \<in> kerbIV_gets;
|
|
205 |
Gets B \<lbrace>
|
|
206 |
(Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
|
|
207 |
(Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
|
|
208 |
\<in> set evs6;
|
|
209 |
\<not> expiredSK Ts evs6;
|
|
210 |
\<not> expiredA T3 evs6
|
|
211 |
\<rbrakk>
|
|
212 |
\<Longrightarrow> Says B A (Crypt servK (Number T3))
|
|
213 |
# evs6 \<in> kerbIV_gets"
|
|
214 |
(* Checks similar to those in K4. *)
|
|
215 |
|
|
216 |
(*---------------------------------------------------------------------*)
|
|
217 |
|
|
218 |
(* Leaking an authK... *)
|
|
219 |
Oops1: "\<lbrakk> evsO1 \<in> kerbIV_gets; A \<noteq> Spy;
|
|
220 |
Says Kas A
|
|
221 |
(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
222 |
authTicket\<rbrace>) \<in> set evsO1;
|
|
223 |
expiredAK Ta evsO1 \<rbrakk>
|
|
224 |
\<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
|
|
225 |
# evsO1 \<in> kerbIV_gets"
|
|
226 |
|
|
227 |
(*---------------------------------------------------------------------*)
|
|
228 |
|
|
229 |
(*Leaking a servK... *)
|
|
230 |
Oops2: "\<lbrakk> evsO2 \<in> kerbIV_gets; A \<noteq> Spy;
|
|
231 |
Says Tgs A
|
|
232 |
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
233 |
\<in> set evsO2;
|
|
234 |
expiredSK Ts evsO2 \<rbrakk>
|
|
235 |
\<Longrightarrow> Says A Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
|
|
236 |
# evsO2 \<in> kerbIV_gets"
|
|
237 |
|
|
238 |
(*---------------------------------------------------------------------*)
|
|
239 |
|
|
240 |
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
|
|
241 |
declare parts.Body [dest]
|
|
242 |
declare analz_into_parts [dest]
|
|
243 |
declare Fake_parts_insert_in_Un [dest]
|
|
244 |
|
|
245 |
subsection{*Lemmas about reception event*}
|
|
246 |
|
|
247 |
lemma Gets_imp_Says :
|
|
248 |
"\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
|
|
249 |
apply (erule rev_mp)
|
|
250 |
apply (erule kerbIV_gets.induct)
|
|
251 |
apply auto
|
|
252 |
done
|
|
253 |
|
|
254 |
lemma Gets_imp_knows_Spy:
|
|
255 |
"\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs"
|
|
256 |
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
|
|
257 |
done
|
|
258 |
|
|
259 |
(*Needed for force to work for example in new_keys_not_used*)
|
|
260 |
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
|
|
261 |
|
|
262 |
lemma Gets_imp_knows:
|
|
263 |
"\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> X \<in> knows B evs"
|
|
264 |
apply (case_tac "B = Spy")
|
|
265 |
apply (blast dest!: Gets_imp_knows_Spy)
|
|
266 |
apply (blast dest!: Gets_imp_knows_agents)
|
|
267 |
done
|
|
268 |
|
|
269 |
subsection{*Lemmas about @{term authKeys}*}
|
|
270 |
|
|
271 |
lemma authKeys_empty: "authKeys [] = {}"
|
|
272 |
apply (unfold authKeys_def)
|
|
273 |
apply (simp (no_asm))
|
|
274 |
done
|
|
275 |
|
|
276 |
lemma authKeys_not_insert:
|
|
277 |
"(\<forall>A Ta akey Peer.
|
|
278 |
ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
|
|
279 |
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
|
|
280 |
\<Longrightarrow> authKeys (ev # evs) = authKeys evs"
|
|
281 |
by (unfold authKeys_def, auto)
|
|
282 |
|
|
283 |
lemma authKeys_insert:
|
|
284 |
"authKeys
|
|
285 |
(Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
|
|
286 |
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
|
|
287 |
= insert K (authKeys evs)"
|
|
288 |
by (unfold authKeys_def, auto)
|
|
289 |
|
|
290 |
lemma authKeys_simp:
|
|
291 |
"K \<in> authKeys
|
|
292 |
(Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
|
|
293 |
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
|
|
294 |
\<Longrightarrow> K = K' | K \<in> authKeys evs"
|
|
295 |
by (unfold authKeys_def, auto)
|
|
296 |
|
|
297 |
lemma authKeysI:
|
|
298 |
"Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
|
|
299 |
(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
|
|
300 |
\<Longrightarrow> K \<in> authKeys evs"
|
|
301 |
by (unfold authKeys_def, auto)
|
|
302 |
|
|
303 |
lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
|
|
304 |
by (simp add: authKeys_def, blast)
|
|
305 |
|
|
306 |
|
|
307 |
subsection{*Forwarding Lemmas*}
|
|
308 |
|
|
309 |
lemma Says_ticket_parts:
|
|
310 |
"Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
|
|
311 |
\<Longrightarrow> Ticket \<in> parts (spies evs)"
|
|
312 |
apply blast
|
|
313 |
done
|
|
314 |
|
|
315 |
lemma Gets_ticket_parts:
|
|
316 |
"\<lbrakk>Gets A (Crypt K \<lbrace>SesKey, Peer, Ta, Ticket\<rbrace>) \<in> set evs; evs \<in> kerbIV_gets \<rbrakk>
|
|
317 |
\<Longrightarrow> Ticket \<in> parts (spies evs)"
|
|
318 |
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj])
|
|
319 |
done
|
|
320 |
|
|
321 |
lemma Oops_range_spies1:
|
|
322 |
"\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
|
|
323 |
\<in> set evs ;
|
|
324 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
|
|
325 |
apply (erule rev_mp)
|
|
326 |
apply (erule kerbIV_gets.induct, auto)
|
|
327 |
done
|
|
328 |
|
|
329 |
lemma Oops_range_spies2:
|
|
330 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
|
|
331 |
\<in> set evs ;
|
|
332 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys"
|
|
333 |
apply (erule rev_mp)
|
|
334 |
apply (erule kerbIV_gets.induct, auto)
|
|
335 |
done
|
|
336 |
|
|
337 |
|
|
338 |
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
|
|
339 |
lemma Spy_see_shrK [simp]:
|
|
340 |
"evs \<in> kerbIV_gets \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
|
|
341 |
apply (erule kerbIV_gets.induct)
|
|
342 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
343 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
344 |
apply (blast+)
|
|
345 |
done
|
|
346 |
|
|
347 |
lemma Spy_analz_shrK [simp]:
|
|
348 |
"evs \<in> kerbIV_gets \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
|
|
349 |
by auto
|
|
350 |
|
|
351 |
lemma Spy_see_shrK_D [dest!]:
|
|
352 |
"\<lbrakk> Key (shrK A) \<in> parts (spies evs); evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A:bad"
|
|
353 |
by (blast dest: Spy_see_shrK)
|
|
354 |
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
|
|
355 |
|
|
356 |
text{*Nobody can have used non-existent keys!*}
|
|
357 |
lemma new_keys_not_used [simp]:
|
|
358 |
"\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbIV_gets\<rbrakk>
|
|
359 |
\<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
|
|
360 |
apply (erule rev_mp)
|
|
361 |
apply (erule kerbIV_gets.induct)
|
|
362 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
363 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
364 |
txt{*Fake*}
|
|
365 |
apply (force dest!: keysFor_parts_insert)
|
|
366 |
txt{*Others*}
|
|
367 |
apply (force dest!: analz_shrK_Decrypt)+
|
|
368 |
done
|
|
369 |
|
|
370 |
(*Earlier, all protocol proofs declared this theorem.
|
|
371 |
But few of them actually need it! (Another is Yahalom) *)
|
|
372 |
lemma new_keys_not_analzd:
|
|
373 |
"\<lbrakk>evs \<in> kerbIV_gets; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
|
|
374 |
\<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
|
|
375 |
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
|
|
376 |
|
|
377 |
|
|
378 |
subsection{*Regularity Lemmas*}
|
|
379 |
text{*These concern the form of items passed in messages*}
|
|
380 |
|
|
381 |
text{*Describes the form of all components sent by Kas*}
|
|
382 |
|
|
383 |
lemma Says_Kas_message_form:
|
|
384 |
"\<lbrakk> Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
|
|
385 |
\<in> set evs;
|
|
386 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow>
|
|
387 |
K = shrK A & Peer = Tgs &
|
|
388 |
authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
|
|
389 |
authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>)"
|
|
390 |
apply (erule rev_mp)
|
|
391 |
apply (erule kerbIV_gets.induct)
|
|
392 |
apply (simp_all (no_asm) add: authKeys_def authKeys_insert)
|
|
393 |
apply blast+
|
|
394 |
done
|
|
395 |
|
|
396 |
|
|
397 |
lemma SesKey_is_session_key:
|
|
398 |
"\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
|
|
399 |
\<in> parts (spies evs); Tgs_B \<notin> bad;
|
|
400 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
401 |
\<Longrightarrow> SesKey \<notin> range shrK"
|
|
402 |
apply (erule rev_mp)
|
|
403 |
apply (erule kerbIV_gets.induct)
|
|
404 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
405 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
|
|
406 |
done
|
|
407 |
|
|
408 |
lemma authTicket_authentic:
|
|
409 |
"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
|
|
410 |
\<in> parts (spies evs);
|
|
411 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
412 |
\<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
413 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
414 |
\<in> set evs"
|
|
415 |
apply (erule rev_mp)
|
|
416 |
apply (erule kerbIV_gets.induct)
|
|
417 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
418 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
419 |
txt{*Fake, K4*}
|
|
420 |
apply (blast+)
|
|
421 |
done
|
|
422 |
|
|
423 |
lemma authTicket_crypt_authK:
|
|
424 |
"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
|
|
425 |
\<in> parts (spies evs);
|
|
426 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
427 |
\<Longrightarrow> authK \<in> authKeys evs"
|
|
428 |
apply (frule authTicket_authentic, assumption)
|
|
429 |
apply (simp (no_asm) add: authKeys_def)
|
|
430 |
apply blast
|
|
431 |
done
|
|
432 |
|
|
433 |
lemma Says_Tgs_message_form:
|
|
434 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
435 |
\<in> set evs;
|
|
436 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
437 |
\<Longrightarrow> B \<noteq> Tgs &
|
|
438 |
authK \<notin> range shrK & authK \<in> authKeys evs & authK \<in> symKeys &
|
|
439 |
servK \<notin> range shrK & servK \<notin> authKeys evs & servK \<in> symKeys &
|
|
440 |
servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>)"
|
|
441 |
apply (erule rev_mp)
|
|
442 |
apply (erule kerbIV_gets.induct)
|
|
443 |
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast, auto)
|
|
444 |
txt{*Three subcases of Message 4*}
|
|
445 |
apply (blast dest!: SesKey_is_session_key)
|
|
446 |
apply (blast dest: authTicket_crypt_authK)
|
|
447 |
apply (blast dest!: authKeys_used Says_Kas_message_form)
|
|
448 |
done
|
|
449 |
|
|
450 |
|
|
451 |
lemma authTicket_form:
|
|
452 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>
|
|
453 |
\<in> parts (spies evs);
|
|
454 |
A \<notin> bad;
|
|
455 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
456 |
\<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys &
|
|
457 |
authTicket = Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>"
|
|
458 |
apply (erule rev_mp)
|
|
459 |
apply (erule kerbIV_gets.induct)
|
|
460 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
461 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
462 |
apply blast+
|
|
463 |
done
|
|
464 |
|
|
465 |
text{* This form holds also over an authTicket, but is not needed below.*}
|
|
466 |
lemma servTicket_form:
|
|
467 |
"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>
|
|
468 |
\<in> parts (spies evs);
|
|
469 |
Key authK \<notin> analz (spies evs);
|
|
470 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
471 |
\<Longrightarrow> servK \<notin> range shrK & servK \<in> symKeys &
|
|
472 |
(\<exists>A. servTicket = Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)"
|
|
473 |
apply (erule rev_mp)
|
|
474 |
apply (erule rev_mp)
|
|
475 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
476 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
477 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
|
|
478 |
done
|
|
479 |
|
|
480 |
text{* Essentially the same as @{text authTicket_form} *}
|
|
481 |
lemma Says_kas_message_form:
|
|
482 |
"\<lbrakk> Gets A (Crypt (shrK A)
|
|
483 |
\<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
|
|
484 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
485 |
\<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys &
|
|
486 |
authTicket =
|
|
487 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
|
|
488 |
| authTicket \<in> analz (spies evs)"
|
|
489 |
by (blast dest: analz_shrK_Decrypt authTicket_form
|
|
490 |
Gets_imp_knows_Spy [THEN analz.Inj])
|
|
491 |
|
|
492 |
lemma Says_tgs_message_form:
|
|
493 |
"\<lbrakk> Gets A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
|
|
494 |
\<in> set evs; authK \<in> symKeys;
|
|
495 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
496 |
\<Longrightarrow> servK \<notin> range shrK &
|
|
497 |
(\<exists>A. servTicket =
|
|
498 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)
|
|
499 |
| servTicket \<in> analz (spies evs)"
|
|
500 |
apply (frule Gets_imp_knows_Spy [THEN analz.Inj], auto)
|
|
501 |
apply (force dest!: servTicket_form)
|
|
502 |
apply (frule analz_into_parts)
|
|
503 |
apply (frule servTicket_form, auto)
|
|
504 |
done
|
|
505 |
|
|
506 |
|
|
507 |
subsection{*Authenticity theorems: confirm origin of sensitive messages*}
|
|
508 |
|
|
509 |
lemma authK_authentic:
|
|
510 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>
|
|
511 |
\<in> parts (spies evs);
|
|
512 |
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
513 |
\<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
|
|
514 |
\<in> set evs"
|
|
515 |
apply (erule rev_mp)
|
|
516 |
apply (erule kerbIV_gets.induct)
|
|
517 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
518 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
519 |
txt{*Fake*}
|
|
520 |
apply blast
|
|
521 |
txt{*K4*}
|
|
522 |
apply (blast dest!: authTicket_authentic [THEN Says_Kas_message_form])
|
|
523 |
done
|
|
524 |
|
|
525 |
text{*If a certain encrypted message appears then it originated with Tgs*}
|
|
526 |
lemma servK_authentic:
|
|
527 |
"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
528 |
\<in> parts (spies evs);
|
|
529 |
Key authK \<notin> analz (spies evs);
|
|
530 |
authK \<notin> range shrK;
|
|
531 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
532 |
\<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
533 |
\<in> set evs"
|
|
534 |
apply (erule rev_mp)
|
|
535 |
apply (erule rev_mp)
|
|
536 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
537 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
538 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
539 |
txt{*Fake*}
|
|
540 |
apply blast
|
|
541 |
txt{*K2*}
|
|
542 |
apply blast
|
|
543 |
txt{*K4*}
|
|
544 |
apply auto
|
|
545 |
done
|
|
546 |
|
|
547 |
lemma servK_authentic_bis:
|
|
548 |
"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
549 |
\<in> parts (spies evs);
|
|
550 |
Key authK \<notin> analz (spies evs);
|
|
551 |
B \<noteq> Tgs;
|
|
552 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
553 |
\<Longrightarrow> \<exists>A. Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
554 |
\<in> set evs"
|
|
555 |
apply (erule rev_mp)
|
|
556 |
apply (erule rev_mp)
|
|
557 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
558 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
559 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
560 |
txt{*Fake*}
|
|
561 |
apply blast
|
|
562 |
txt{*K4*}
|
|
563 |
apply blast
|
|
564 |
done
|
|
565 |
|
|
566 |
text{*Authenticity of servK for B*}
|
|
567 |
lemma servTicket_authentic_Tgs:
|
|
568 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
569 |
\<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad;
|
|
570 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
571 |
\<Longrightarrow> \<exists>authK.
|
|
572 |
Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
|
|
573 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
|
|
574 |
\<in> set evs"
|
|
575 |
apply (erule rev_mp)
|
|
576 |
apply (erule rev_mp)
|
|
577 |
apply (erule kerbIV_gets.induct)
|
|
578 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
579 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
580 |
apply blast+
|
|
581 |
done
|
|
582 |
|
|
583 |
text{*Anticipated here from next subsection*}
|
|
584 |
lemma K4_imp_K2:
|
|
585 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
586 |
\<in> set evs; evs \<in> kerbIV_gets\<rbrakk>
|
|
587 |
\<Longrightarrow> \<exists>Ta. Says Kas A
|
|
588 |
(Crypt (shrK A)
|
|
589 |
\<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
590 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
591 |
\<in> set evs"
|
|
592 |
apply (erule rev_mp)
|
|
593 |
apply (erule kerbIV_gets.induct)
|
|
594 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
595 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, auto)
|
|
596 |
apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
|
|
597 |
done
|
|
598 |
|
|
599 |
text{*Anticipated here from next subsection*}
|
|
600 |
lemma u_K4_imp_K2:
|
|
601 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
602 |
\<in> set evs; evs \<in> kerbIV_gets\<rbrakk>
|
|
603 |
\<Longrightarrow> \<exists>Ta. (Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
604 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
605 |
\<in> set evs
|
|
606 |
& servKlife + Ts <= authKlife + Ta)"
|
|
607 |
apply (erule rev_mp)
|
|
608 |
apply (erule kerbIV_gets.induct)
|
|
609 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
610 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, auto)
|
|
611 |
apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
|
|
612 |
done
|
|
613 |
|
|
614 |
lemma servTicket_authentic_Kas:
|
|
615 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
616 |
\<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad;
|
|
617 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
618 |
\<Longrightarrow> \<exists>authK Ta.
|
|
619 |
Says Kas A
|
|
620 |
(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
621 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
622 |
\<in> set evs"
|
|
623 |
apply (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
|
|
624 |
done
|
|
625 |
|
|
626 |
lemma u_servTicket_authentic_Kas:
|
|
627 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
628 |
\<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad;
|
|
629 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
630 |
\<Longrightarrow> \<exists>authK Ta. Says Kas A (Crypt(shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
631 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
632 |
\<in> set evs
|
|
633 |
& servKlife + Ts <= authKlife + Ta"
|
|
634 |
apply (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
|
|
635 |
done
|
|
636 |
|
|
637 |
lemma servTicket_authentic:
|
|
638 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
639 |
\<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad;
|
|
640 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
641 |
\<Longrightarrow> \<exists>Ta authK.
|
|
642 |
Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
643 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
644 |
\<in> set evs
|
|
645 |
& Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
|
|
646 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
|
|
647 |
\<in> set evs"
|
|
648 |
apply (blast dest: servTicket_authentic_Tgs K4_imp_K2)
|
|
649 |
done
|
|
650 |
|
|
651 |
lemma u_servTicket_authentic:
|
|
652 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
653 |
\<in> parts (spies evs); B \<noteq> Tgs; B \<notin> bad;
|
|
654 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
655 |
\<Longrightarrow> \<exists>Ta authK.
|
|
656 |
(Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
657 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
658 |
\<in> set evs
|
|
659 |
& Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
|
|
660 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
|
|
661 |
\<in> set evs
|
|
662 |
& servKlife + Ts <= authKlife + Ta)"
|
|
663 |
apply (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
|
|
664 |
done
|
|
665 |
|
|
666 |
lemma u_NotexpiredSK_NotexpiredAK:
|
|
667 |
"\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
|
|
668 |
\<Longrightarrow> \<not> expiredAK Ta evs"
|
|
669 |
apply (blast dest: leI le_trans dest: leD)
|
|
670 |
done
|
|
671 |
|
|
672 |
|
|
673 |
subsection{* Reliability: friendly agents send something if something else happened*}
|
|
674 |
|
|
675 |
lemma K3_imp_K2:
|
|
676 |
"\<lbrakk> Says A Tgs
|
|
677 |
\<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
|
|
678 |
\<in> set evs;
|
|
679 |
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
680 |
\<Longrightarrow> \<exists>Ta. Says Kas A (Crypt (shrK A)
|
|
681 |
\<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
|
|
682 |
\<in> set evs"
|
|
683 |
apply (erule rev_mp)
|
|
684 |
apply (erule kerbIV_gets.induct)
|
|
685 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
686 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast, blast)
|
|
687 |
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic])
|
|
688 |
done
|
|
689 |
|
|
690 |
text{*Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.*}
|
|
691 |
lemma Key_unique_SesKey:
|
|
692 |
"\<lbrakk> Crypt K \<lbrace>Key SesKey, Agent B, T, Ticket\<rbrace>
|
|
693 |
\<in> parts (spies evs);
|
|
694 |
Crypt K' \<lbrace>Key SesKey, Agent B', T', Ticket'\<rbrace>
|
|
695 |
\<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
|
|
696 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
697 |
\<Longrightarrow> K=K' & B=B' & T=T' & Ticket=Ticket'"
|
|
698 |
apply (erule rev_mp)
|
|
699 |
apply (erule rev_mp)
|
|
700 |
apply (erule rev_mp)
|
|
701 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
702 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
703 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
704 |
txt{*Fake, K2, K4*}
|
|
705 |
apply (blast+)
|
|
706 |
done
|
|
707 |
|
|
708 |
lemma Tgs_authenticates_A:
|
|
709 |
"\<lbrakk> Crypt authK \<lbrace>Agent A, Number T2\<rbrace> \<in> parts (spies evs);
|
|
710 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
|
|
711 |
\<in> parts (spies evs);
|
|
712 |
Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
713 |
\<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
|
|
714 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
|
|
715 |
Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs"
|
|
716 |
apply (drule authTicket_authentic, assumption, rotate_tac 4)
|
|
717 |
apply (erule rev_mp, erule rev_mp, erule rev_mp)
|
|
718 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
719 |
apply (frule_tac [6] Gets_ticket_parts)
|
|
720 |
apply (frule_tac [9] Gets_ticket_parts)
|
|
721 |
apply (simp_all (no_asm_simp) add: all_conj_distrib)
|
|
722 |
txt{*Fake*}
|
|
723 |
apply blast
|
|
724 |
txt{*K2*}
|
|
725 |
apply (force dest!: Crypt_imp_keysFor)
|
|
726 |
txt{*K3*}
|
|
727 |
apply (blast dest: Key_unique_SesKey)
|
|
728 |
txt{*K5*}
|
|
729 |
txt{*If authKa were compromised, so would be authK*}
|
|
730 |
apply (case_tac "Key authKa \<in> analz (spies evs5)")
|
|
731 |
apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
|
|
732 |
txt{*Besides, since authKa originated with Kas anyway...*}
|
|
733 |
apply (clarify, drule K3_imp_K2, assumption, assumption)
|
|
734 |
apply (clarify, drule Says_Kas_message_form, assumption)
|
|
735 |
txt{*...it cannot be a shared key*. Therefore @{term servK_authentic} applies.
|
|
736 |
Contradition: Tgs used authK as a servkey,
|
|
737 |
while Kas used it as an authkey*}
|
|
738 |
apply (blast dest: servK_authentic Says_Tgs_message_form)
|
|
739 |
done
|
|
740 |
|
|
741 |
lemma Says_K5:
|
|
742 |
"\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
|
|
743 |
Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
|
|
744 |
servTicket\<rbrace>) \<in> set evs;
|
|
745 |
Key servK \<notin> analz (spies evs);
|
|
746 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
747 |
\<Longrightarrow> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
|
|
748 |
apply (erule rev_mp)
|
|
749 |
apply (erule rev_mp)
|
|
750 |
apply (erule rev_mp)
|
|
751 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
752 |
apply (frule_tac [6] Gets_ticket_parts)
|
|
753 |
apply (frule_tac [9] Gets_ticket_parts)
|
|
754 |
apply (simp_all (no_asm_simp) add: all_conj_distrib)
|
|
755 |
apply blast
|
|
756 |
txt{*K3*}
|
|
757 |
apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
|
|
758 |
txt{*K4*}
|
|
759 |
apply (force dest!: Crypt_imp_keysFor)
|
|
760 |
txt{*K5*}
|
|
761 |
apply (blast dest: Key_unique_SesKey)
|
|
762 |
done
|
|
763 |
|
|
764 |
text{*Anticipated here from next subsection*}
|
|
765 |
lemma unique_CryptKey:
|
|
766 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SesKey, T\<rbrace>
|
|
767 |
\<in> parts (spies evs);
|
|
768 |
Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
|
|
769 |
\<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
|
|
770 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
771 |
\<Longrightarrow> A=A' & B=B' & T=T'"
|
|
772 |
apply (erule rev_mp)
|
|
773 |
apply (erule rev_mp)
|
|
774 |
apply (erule rev_mp)
|
|
775 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
776 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
777 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
778 |
txt{*Fake, K2, K4*}
|
|
779 |
apply (blast+)
|
|
780 |
done
|
|
781 |
|
|
782 |
lemma Says_K6:
|
|
783 |
"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
|
|
784 |
Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
|
|
785 |
servTicket\<rbrace>) \<in> set evs;
|
|
786 |
Key servK \<notin> analz (spies evs);
|
|
787 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
788 |
\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
|
|
789 |
apply (erule rev_mp)
|
|
790 |
apply (erule rev_mp)
|
|
791 |
apply (erule rev_mp)
|
|
792 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
793 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
794 |
apply (frule_tac [6] Gets_ticket_parts)
|
|
795 |
apply (simp_all (no_asm_simp))
|
|
796 |
apply blast
|
|
797 |
apply (force dest!: Crypt_imp_keysFor, clarify)
|
|
798 |
apply (frule Says_Tgs_message_form, assumption, clarify) (*PROOF FAILED if omitted*)
|
|
799 |
apply (blast dest: unique_CryptKey)
|
|
800 |
done
|
|
801 |
|
|
802 |
text{*Needs a unicity theorem, hence moved here*}
|
|
803 |
lemma servK_authentic_ter:
|
|
804 |
"\<lbrakk> Says Kas A
|
|
805 |
(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs;
|
|
806 |
Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
807 |
\<in> parts (spies evs);
|
|
808 |
Key authK \<notin> analz (spies evs);
|
|
809 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
810 |
\<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
811 |
\<in> set evs"
|
|
812 |
apply (frule Says_Kas_message_form, assumption)
|
|
813 |
apply (erule rev_mp)
|
|
814 |
apply (erule rev_mp)
|
|
815 |
apply (erule rev_mp)
|
|
816 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
817 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
818 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
|
|
819 |
txt{*K2 and K4 remain*}
|
|
820 |
prefer 2 apply (blast dest!: unique_CryptKey)
|
|
821 |
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
|
|
822 |
done
|
|
823 |
|
|
824 |
|
|
825 |
subsection{*Unicity Theorems*}
|
|
826 |
|
|
827 |
text{* The session key, if secure, uniquely identifies the Ticket
|
|
828 |
whether authTicket or servTicket. As a matter of fact, one can read
|
|
829 |
also Tgs in the place of B. *}
|
|
830 |
|
|
831 |
|
|
832 |
lemma unique_authKeys:
|
|
833 |
"\<lbrakk> Says Kas A
|
|
834 |
(Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, X\<rbrace>) \<in> set evs;
|
|
835 |
Says Kas A'
|
|
836 |
(Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta', X'\<rbrace>) \<in> set evs;
|
|
837 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A=A' & Ka=Ka' & Ta=Ta' & X=X'"
|
|
838 |
apply (erule rev_mp)
|
|
839 |
apply (erule rev_mp)
|
|
840 |
apply (erule kerbIV_gets.induct)
|
|
841 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
842 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
843 |
txt{*K2*}
|
|
844 |
apply blast
|
|
845 |
done
|
|
846 |
|
|
847 |
text{* servK uniquely identifies the message from Tgs *}
|
|
848 |
lemma unique_servKeys:
|
|
849 |
"\<lbrakk> Says Tgs A
|
|
850 |
(Crypt K \<lbrace>Key servK, Agent B, Ts, X\<rbrace>) \<in> set evs;
|
|
851 |
Says Tgs A'
|
|
852 |
(Crypt K' \<lbrace>Key servK, Agent B', Ts', X'\<rbrace>) \<in> set evs;
|
|
853 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> A=A' & B=B' & K=K' & Ts=Ts' & X=X'"
|
|
854 |
apply (erule rev_mp)
|
|
855 |
apply (erule rev_mp)
|
|
856 |
apply (erule kerbIV_gets.induct)
|
|
857 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
858 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
859 |
txt{*K4*}
|
|
860 |
apply blast
|
|
861 |
done
|
|
862 |
|
|
863 |
text{* Revised unicity theorems *}
|
|
864 |
|
|
865 |
lemma Kas_Unique:
|
|
866 |
"\<lbrakk> Says Kas A
|
|
867 |
(Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>) \<in> set evs;
|
|
868 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow>
|
|
869 |
Unique (Says Kas A (Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta, authTicket\<rbrace>))
|
|
870 |
on evs"
|
|
871 |
apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def)
|
|
872 |
apply blast
|
|
873 |
done
|
|
874 |
|
|
875 |
lemma Tgs_Unique:
|
|
876 |
"\<lbrakk> Says Tgs A
|
|
877 |
(Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>) \<in> set evs;
|
|
878 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow>
|
|
879 |
Unique (Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>))
|
|
880 |
on evs"
|
|
881 |
apply (erule rev_mp, erule kerbIV_gets.induct, simp_all add: Unique_def)
|
|
882 |
apply blast
|
|
883 |
done
|
|
884 |
|
|
885 |
|
|
886 |
subsection{*Lemmas About the Predicate @{term AKcryptSK}*}
|
|
887 |
|
|
888 |
lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
|
|
889 |
by (simp add: AKcryptSK_def)
|
|
890 |
|
|
891 |
lemma AKcryptSKI:
|
|
892 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
|
|
893 |
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
|
|
894 |
apply (unfold AKcryptSK_def)
|
|
895 |
apply (blast dest: Says_Tgs_message_form)
|
|
896 |
done
|
|
897 |
|
|
898 |
lemma AKcryptSK_Says [simp]:
|
|
899 |
"AKcryptSK authK servK (Says S A X # evs) =
|
|
900 |
(Tgs = S &
|
|
901 |
(\<exists>B Ts. X = Crypt authK
|
|
902 |
\<lbrace>Key servK, Agent B, Number Ts,
|
|
903 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
|
|
904 |
| AKcryptSK authK servK evs)"
|
|
905 |
apply (unfold AKcryptSK_def)
|
|
906 |
apply (simp (no_asm))
|
|
907 |
apply blast
|
|
908 |
done
|
|
909 |
|
|
910 |
(*A fresh authK cannot be associated with any other
|
|
911 |
(with respect to a given trace). *)
|
|
912 |
lemma Auth_fresh_not_AKcryptSK:
|
|
913 |
"\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV_gets \<rbrakk>
|
|
914 |
\<Longrightarrow> \<not> AKcryptSK authK servK evs"
|
|
915 |
apply (unfold AKcryptSK_def)
|
|
916 |
apply (erule rev_mp)
|
|
917 |
apply (erule kerbIV_gets.induct)
|
|
918 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
919 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
|
|
920 |
done
|
|
921 |
|
|
922 |
(*A fresh servK cannot be associated with any other
|
|
923 |
(with respect to a given trace). *)
|
|
924 |
lemma Serv_fresh_not_AKcryptSK:
|
|
925 |
"Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
|
|
926 |
apply (unfold AKcryptSK_def, blast)
|
|
927 |
done
|
|
928 |
|
|
929 |
lemma authK_not_AKcryptSK:
|
|
930 |
"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
|
|
931 |
\<in> parts (spies evs); evs \<in> kerbIV_gets \<rbrakk>
|
|
932 |
\<Longrightarrow> \<not> AKcryptSK K authK evs"
|
|
933 |
apply (erule rev_mp)
|
|
934 |
apply (erule kerbIV_gets.induct)
|
|
935 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
936 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
937 |
txt{*Fake*}
|
|
938 |
apply blast
|
|
939 |
txt{*Reception*}
|
|
940 |
apply (simp add: AKcryptSK_def)
|
|
941 |
txt{*K2: by freshness*}
|
|
942 |
apply (simp add: AKcryptSK_def)
|
|
943 |
txt{*K4*}
|
|
944 |
apply (blast+)
|
|
945 |
done
|
|
946 |
|
|
947 |
text{*A secure serverkey cannot have been used to encrypt others*}
|
|
948 |
lemma servK_not_AKcryptSK:
|
|
949 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, Number Ts\<rbrace> \<in> parts (spies evs);
|
|
950 |
Key SK \<notin> analz (spies evs); SK \<in> symKeys;
|
|
951 |
B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
|
|
952 |
\<Longrightarrow> \<not> AKcryptSK SK K evs"
|
|
953 |
apply (erule rev_mp)
|
|
954 |
apply (erule rev_mp)
|
|
955 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
956 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
957 |
apply (frule_tac [6] Gets_ticket_parts, simp_all, blast)
|
|
958 |
txt{*Reception*}
|
|
959 |
apply (simp add: AKcryptSK_def)
|
|
960 |
txt{*K4 splits into distinct subcases*}
|
|
961 |
apply auto
|
|
962 |
txt{*servK can't have been enclosed in two certificates*}
|
|
963 |
prefer 2 apply (blast dest: unique_CryptKey)
|
|
964 |
txt{*servK is fresh and so could not have been used, by
|
|
965 |
@{text new_keys_not_used}*}
|
|
966 |
apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
|
|
967 |
done
|
|
968 |
|
|
969 |
text{*Long term keys are not issued as servKeys*}
|
|
970 |
lemma shrK_not_AKcryptSK:
|
|
971 |
"evs \<in> kerbIV_gets \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
|
|
972 |
apply (unfold AKcryptSK_def)
|
|
973 |
apply (erule kerbIV_gets.induct)
|
|
974 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
975 |
apply (frule_tac [6] Gets_ticket_parts, auto)
|
|
976 |
done
|
|
977 |
|
|
978 |
text{*The Tgs message associates servK with authK and therefore not with any
|
|
979 |
other key authK.*}
|
|
980 |
lemma Says_Tgs_AKcryptSK:
|
|
981 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>)
|
|
982 |
\<in> set evs;
|
|
983 |
authK' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk>
|
|
984 |
\<Longrightarrow> \<not> AKcryptSK authK' servK evs"
|
|
985 |
apply (unfold AKcryptSK_def)
|
|
986 |
apply (blast dest: unique_servKeys)
|
|
987 |
done
|
|
988 |
|
|
989 |
text{*Equivalently*}
|
|
990 |
lemma not_different_AKcryptSK:
|
|
991 |
"\<lbrakk> AKcryptSK authK servK evs;
|
|
992 |
authK' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk>
|
|
993 |
\<Longrightarrow> \<not> AKcryptSK authK' servK evs \<and> servK \<in> symKeys"
|
|
994 |
apply (simp add: AKcryptSK_def)
|
|
995 |
apply (blast dest: unique_servKeys Says_Tgs_message_form)
|
|
996 |
done
|
|
997 |
|
|
998 |
lemma AKcryptSK_not_AKcryptSK:
|
|
999 |
"\<lbrakk> AKcryptSK authK servK evs; evs \<in> kerbIV_gets \<rbrakk>
|
|
1000 |
\<Longrightarrow> \<not> AKcryptSK servK K evs"
|
|
1001 |
apply (erule rev_mp)
|
|
1002 |
apply (erule kerbIV_gets.induct)
|
|
1003 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
1004 |
apply (frule_tac [6] Gets_ticket_parts)
|
|
1005 |
txt{*Reception*}
|
|
1006 |
prefer 3 apply (simp add: AKcryptSK_def)
|
|
1007 |
apply (simp_all, safe)
|
|
1008 |
txt{*K4 splits into subcases*}
|
|
1009 |
prefer 4 apply (blast dest!: authK_not_AKcryptSK)
|
|
1010 |
txt{*servK is fresh and so could not have been used, by
|
|
1011 |
@{text new_keys_not_used}*}
|
|
1012 |
prefer 2
|
|
1013 |
apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
|
|
1014 |
txt{*Others by freshness*}
|
|
1015 |
apply (blast+)
|
|
1016 |
done
|
|
1017 |
|
|
1018 |
text{*The only session keys that can be found with the help of session keys are
|
|
1019 |
those sent by Tgs in step K4. *}
|
|
1020 |
|
|
1021 |
text{*We take some pains to express the property
|
|
1022 |
as a logical equivalence so that the simplifier can apply it.*}
|
|
1023 |
lemma Key_analz_image_Key_lemma:
|
|
1024 |
"P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
|
|
1025 |
\<Longrightarrow>
|
|
1026 |
P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
|
|
1027 |
by (blast intro: analz_mono [THEN subsetD])
|
|
1028 |
|
|
1029 |
|
|
1030 |
lemma AKcryptSK_analz_insert:
|
|
1031 |
"\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV_gets \<rbrakk>
|
|
1032 |
\<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
|
|
1033 |
apply (simp add: AKcryptSK_def, clarify)
|
|
1034 |
apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
|
|
1035 |
done
|
|
1036 |
|
|
1037 |
lemma authKeys_are_not_AKcryptSK:
|
|
1038 |
"\<lbrakk> K \<in> authKeys evs Un range shrK; evs \<in> kerbIV_gets \<rbrakk>
|
|
1039 |
\<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
|
|
1040 |
apply (simp add: authKeys_def AKcryptSK_def)
|
|
1041 |
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
|
|
1042 |
done
|
|
1043 |
|
|
1044 |
lemma not_authKeys_not_AKcryptSK:
|
|
1045 |
"\<lbrakk> K \<notin> authKeys evs;
|
|
1046 |
K \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
|
|
1047 |
\<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
|
|
1048 |
apply (simp add: AKcryptSK_def)
|
|
1049 |
apply (blast dest: Says_Tgs_message_form)
|
|
1050 |
done
|
|
1051 |
|
|
1052 |
|
|
1053 |
subsection{*Secrecy Theorems*}
|
|
1054 |
|
|
1055 |
text{*For the Oops2 case of the next theorem*}
|
|
1056 |
lemma Oops2_not_AKcryptSK:
|
|
1057 |
"\<lbrakk> evs \<in> kerbIV_gets;
|
|
1058 |
Says Tgs A (Crypt authK
|
|
1059 |
\<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1060 |
\<in> set evs \<rbrakk>
|
|
1061 |
\<Longrightarrow> \<not> AKcryptSK servK SK evs"
|
|
1062 |
apply (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
|
|
1063 |
done
|
|
1064 |
|
|
1065 |
text{* Big simplification law for keys SK that are not crypted by keys in KK
|
|
1066 |
It helps prove three, otherwise hard, facts about keys. These facts are
|
|
1067 |
exploited as simplification laws for analz, and also "limit the damage"
|
|
1068 |
in case of loss of a key to the spy. See ESORICS98. *}
|
|
1069 |
lemma Key_analz_image_Key [rule_format (no_asm)]:
|
|
1070 |
"evs \<in> kerbIV_gets \<Longrightarrow>
|
|
1071 |
(\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
|
|
1072 |
(\<forall>K \<in> KK. \<not> AKcryptSK K SK evs) \<longrightarrow>
|
|
1073 |
(Key SK \<in> analz (Key`KK Un (spies evs))) =
|
|
1074 |
(SK \<in> KK | Key SK \<in> analz (spies evs)))"
|
|
1075 |
apply (erule kerbIV_gets.induct)
|
|
1076 |
apply (frule_tac [11] Oops_range_spies2)
|
|
1077 |
apply (frule_tac [10] Oops_range_spies1)
|
|
1078 |
apply (frule_tac [8] Says_tgs_message_form)
|
|
1079 |
apply (frule_tac [6] Says_kas_message_form)
|
|
1080 |
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
|
|
1081 |
txt{*Case-splits for Oops1 and message 5: the negated case simplifies using
|
|
1082 |
the induction hypothesis*}
|
|
1083 |
apply (case_tac [12] "AKcryptSK authK SK evsO1")
|
|
1084 |
apply (case_tac [9] "AKcryptSK servK SK evs5")
|
|
1085 |
apply (simp_all del: image_insert
|
|
1086 |
add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
|
|
1087 |
Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
|
|
1088 |
Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
|
|
1089 |
--{*18 seconds on a 1.8GHz machine??*}
|
|
1090 |
txt{*Fake*}
|
|
1091 |
apply spy_analz
|
|
1092 |
txt{*Reception*}
|
|
1093 |
apply (simp add: AKcryptSK_def)
|
|
1094 |
txt{*K2*}
|
|
1095 |
apply blast
|
|
1096 |
txt{*K3*}
|
|
1097 |
apply blast
|
|
1098 |
txt{*K4*}
|
|
1099 |
apply (blast dest!: authK_not_AKcryptSK)
|
|
1100 |
txt{*K5*}
|
|
1101 |
apply (case_tac "Key servK \<in> analz (spies evs5) ")
|
|
1102 |
txt{*If servK is compromised then the result follows directly...*}
|
|
1103 |
apply (simp (no_asm_simp) add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
|
|
1104 |
txt{*...therefore servK is uncompromised.*}
|
|
1105 |
txt{*The AKcryptSK servK SK evs5 case leads to a contradiction.*}
|
|
1106 |
apply (blast elim!: servK_not_AKcryptSK [THEN [2] rev_notE] del: allE ballE)
|
|
1107 |
txt{*Another K5 case*}
|
|
1108 |
apply blast
|
|
1109 |
txt{*Oops1*}
|
|
1110 |
apply simp
|
|
1111 |
apply (blast dest!: AKcryptSK_analz_insert)
|
|
1112 |
done
|
|
1113 |
|
|
1114 |
text{* First simplification law for analz: no session keys encrypt
|
|
1115 |
authentication keys or shared keys. *}
|
|
1116 |
lemma analz_insert_freshK1:
|
|
1117 |
"\<lbrakk> evs \<in> kerbIV_gets; K \<in> authKeys evs Un range shrK;
|
|
1118 |
SesKey \<notin> range shrK \<rbrakk>
|
|
1119 |
\<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
|
|
1120 |
(K = SesKey | Key K \<in> analz (spies evs))"
|
|
1121 |
apply (frule authKeys_are_not_AKcryptSK, assumption)
|
|
1122 |
apply (simp del: image_insert
|
|
1123 |
add: analz_image_freshK_simps add: Key_analz_image_Key)
|
|
1124 |
done
|
|
1125 |
|
|
1126 |
|
|
1127 |
text{* Second simplification law for analz: no service keys encrypt any other keys.*}
|
|
1128 |
lemma analz_insert_freshK2:
|
|
1129 |
"\<lbrakk> evs \<in> kerbIV_gets; servK \<notin> (authKeys evs); servK \<notin> range shrK;
|
|
1130 |
K \<in> symKeys \<rbrakk>
|
|
1131 |
\<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
|
|
1132 |
(K = servK | Key K \<in> analz (spies evs))"
|
|
1133 |
apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
|
|
1134 |
apply (simp del: image_insert
|
|
1135 |
add: analz_image_freshK_simps add: Key_analz_image_Key)
|
|
1136 |
done
|
|
1137 |
|
|
1138 |
|
|
1139 |
text{* Third simplification law for analz: only one authentication key encrypts a certain service key.*}
|
|
1140 |
|
|
1141 |
lemma analz_insert_freshK3:
|
|
1142 |
"\<lbrakk> AKcryptSK authK servK evs;
|
|
1143 |
authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
|
|
1144 |
\<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
|
|
1145 |
(servK = authK' | Key servK \<in> analz (spies evs))"
|
|
1146 |
apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
|
|
1147 |
apply (simp del: image_insert
|
|
1148 |
add: analz_image_freshK_simps add: Key_analz_image_Key)
|
|
1149 |
done
|
|
1150 |
|
|
1151 |
lemma analz_insert_freshK3_bis:
|
|
1152 |
"\<lbrakk> Says Tgs A
|
|
1153 |
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1154 |
\<in> set evs;
|
|
1155 |
authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
|
|
1156 |
\<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
|
|
1157 |
(servK = authK' | Key servK \<in> analz (spies evs))"
|
|
1158 |
apply (frule AKcryptSKI, assumption)
|
|
1159 |
apply (simp add: analz_insert_freshK3)
|
|
1160 |
done
|
|
1161 |
|
|
1162 |
text{*a weakness of the protocol*}
|
|
1163 |
lemma authK_compromises_servK:
|
|
1164 |
"\<lbrakk> Says Tgs A
|
|
1165 |
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1166 |
\<in> set evs; authK \<in> symKeys;
|
|
1167 |
Key authK \<in> analz (spies evs); evs \<in> kerbIV_gets \<rbrakk>
|
|
1168 |
\<Longrightarrow> Key servK \<in> analz (spies evs)"
|
|
1169 |
by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
|
|
1170 |
|
|
1171 |
lemma servK_notin_authKeysD:
|
|
1172 |
"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts,
|
|
1173 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
|
|
1174 |
\<in> parts (spies evs);
|
|
1175 |
Key servK \<notin> analz (spies evs);
|
|
1176 |
B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
|
|
1177 |
\<Longrightarrow> servK \<notin> authKeys evs"
|
|
1178 |
apply (erule rev_mp)
|
|
1179 |
apply (erule rev_mp)
|
|
1180 |
apply (simp add: authKeys_def)
|
|
1181 |
apply (erule kerbIV_gets.induct, analz_mono_contra)
|
|
1182 |
apply (frule_tac [8] Gets_ticket_parts)
|
|
1183 |
apply (frule_tac [6] Gets_ticket_parts, simp_all)
|
|
1184 |
apply (blast+)
|
|
1185 |
done
|
|
1186 |
|
|
1187 |
|
|
1188 |
text{*If Spy sees the Authentication Key sent in msg K2, then
|
|
1189 |
the Key has expired.*}
|
|
1190 |
lemma Confidentiality_Kas_lemma [rule_format]:
|
|
1191 |
"\<lbrakk> authK \<in> symKeys; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1192 |
\<Longrightarrow> Says Kas A
|
|
1193 |
(Crypt (shrK A)
|
|
1194 |
\<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
1195 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
1196 |
\<in> set evs \<longrightarrow>
|
|
1197 |
Key authK \<in> analz (spies evs) \<longrightarrow>
|
|
1198 |
expiredAK Ta evs"
|
|
1199 |
apply (erule kerbIV_gets.induct)
|
|
1200 |
apply (frule_tac [11] Oops_range_spies2)
|
|
1201 |
apply (frule_tac [10] Oops_range_spies1)
|
|
1202 |
apply (frule_tac [8] Says_tgs_message_form)
|
|
1203 |
apply (frule_tac [6] Says_kas_message_form)
|
|
1204 |
apply (safe del: impI conjI impCE)
|
|
1205 |
apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
|
|
1206 |
txt{*Fake*}
|
|
1207 |
apply spy_analz
|
|
1208 |
txt{*K2*}
|
|
1209 |
apply blast
|
|
1210 |
txt{*K4*}
|
|
1211 |
apply blast
|
|
1212 |
txt{*Level 8: K5*}
|
|
1213 |
apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
|
|
1214 |
txt{*Oops1*}
|
|
1215 |
apply (blast dest!: unique_authKeys intro: less_SucI)
|
|
1216 |
txt{*Oops2*}
|
|
1217 |
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
|
|
1218 |
done
|
|
1219 |
|
|
1220 |
lemma Confidentiality_Kas:
|
|
1221 |
"\<lbrakk> Says Kas A
|
|
1222 |
(Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
|
|
1223 |
\<in> set evs;
|
|
1224 |
\<not> expiredAK Ta evs;
|
|
1225 |
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1226 |
\<Longrightarrow> Key authK \<notin> analz (spies evs)"
|
|
1227 |
by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
|
|
1228 |
|
|
1229 |
text{*If Spy sees the Service Key sent in msg K4, then
|
|
1230 |
the Key has expired.*}
|
|
1231 |
|
|
1232 |
lemma Confidentiality_lemma [rule_format]:
|
|
1233 |
"\<lbrakk> Says Tgs A
|
|
1234 |
(Crypt authK
|
|
1235 |
\<lbrace>Key servK, Agent B, Number Ts,
|
|
1236 |
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
|
|
1237 |
\<in> set evs;
|
|
1238 |
Key authK \<notin> analz (spies evs);
|
|
1239 |
servK \<in> symKeys;
|
|
1240 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1241 |
\<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
|
|
1242 |
expiredSK Ts evs"
|
|
1243 |
apply (erule rev_mp)
|
|
1244 |
apply (erule rev_mp)
|
|
1245 |
apply (erule kerbIV_gets.induct)
|
|
1246 |
apply (rule_tac [10] impI)+;
|
|
1247 |
--{*The Oops1 case is unusual: must simplify
|
|
1248 |
@{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
|
|
1249 |
@{text analz_mono_contra} weaken it to
|
|
1250 |
@{term "Authkey \<notin> analz (spies evs)"},
|
|
1251 |
for we then conclude @{term "authK \<noteq> authKa"}.*}
|
|
1252 |
apply analz_mono_contra
|
|
1253 |
apply (frule_tac [11] Oops_range_spies2)
|
|
1254 |
apply (frule_tac [10] Oops_range_spies1)
|
|
1255 |
apply (frule_tac [8] Says_tgs_message_form)
|
|
1256 |
apply (frule_tac [6] Says_kas_message_form)
|
|
1257 |
apply (safe del: impI conjI impCE)
|
|
1258 |
apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
|
|
1259 |
txt{*Fake*}
|
|
1260 |
apply spy_analz
|
|
1261 |
txt{*K2*}
|
|
1262 |
apply (blast intro: parts_insertI less_SucI)
|
|
1263 |
txt{*K4*}
|
|
1264 |
apply (blast dest: authTicket_authentic Confidentiality_Kas)
|
|
1265 |
txt{*Oops2*}
|
|
1266 |
prefer 3
|
|
1267 |
apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
|
|
1268 |
txt{*Oops1*}
|
|
1269 |
prefer 2
|
|
1270 |
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
|
|
1271 |
txt{*K5. Not clear how this step could be integrated with the main
|
|
1272 |
simplification step. Done in KerberosV.thy*}
|
|
1273 |
apply clarify
|
|
1274 |
apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl)
|
|
1275 |
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD])
|
|
1276 |
apply (assumption, assumption, blast, assumption)
|
|
1277 |
apply (simp add: analz_insert_freshK2)
|
|
1278 |
apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
|
|
1279 |
done
|
|
1280 |
|
|
1281 |
|
|
1282 |
text{* In the real world Tgs can't check wheter authK is secure! *}
|
|
1283 |
lemma Confidentiality_Tgs:
|
|
1284 |
"\<lbrakk> Says Tgs A
|
|
1285 |
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1286 |
\<in> set evs;
|
|
1287 |
Key authK \<notin> analz (spies evs);
|
|
1288 |
\<not> expiredSK Ts evs;
|
|
1289 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1290 |
\<Longrightarrow> Key servK \<notin> analz (spies evs)"
|
|
1291 |
apply (blast dest: Says_Tgs_message_form Confidentiality_lemma)
|
|
1292 |
done
|
|
1293 |
|
|
1294 |
text{* In the real world Tgs CAN check what Kas sends! *}
|
|
1295 |
lemma Confidentiality_Tgs_bis:
|
|
1296 |
"\<lbrakk> Says Kas A
|
|
1297 |
(Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
|
|
1298 |
\<in> set evs;
|
|
1299 |
Says Tgs A
|
|
1300 |
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1301 |
\<in> set evs;
|
|
1302 |
\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
|
|
1303 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1304 |
\<Longrightarrow> Key servK \<notin> analz (spies evs)"
|
|
1305 |
apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
|
|
1306 |
done
|
|
1307 |
|
|
1308 |
text{*Most general form*}
|
|
1309 |
lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
|
|
1310 |
|
|
1311 |
lemmas Confidentiality_Auth_A = authK_authentic [THEN Confidentiality_Kas]
|
|
1312 |
|
|
1313 |
text{*Needs a confidentiality guarantee, hence moved here.
|
|
1314 |
Authenticity of servK for A*}
|
|
1315 |
lemma servK_authentic_bis_r:
|
|
1316 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
|
|
1317 |
\<in> parts (spies evs);
|
|
1318 |
Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
1319 |
\<in> parts (spies evs);
|
|
1320 |
\<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1321 |
\<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1322 |
\<in> set evs"
|
|
1323 |
apply (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
|
|
1324 |
done
|
|
1325 |
|
|
1326 |
lemma Confidentiality_Serv_A:
|
|
1327 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
|
|
1328 |
\<in> parts (spies evs);
|
|
1329 |
Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
1330 |
\<in> parts (spies evs);
|
|
1331 |
\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
|
|
1332 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1333 |
\<Longrightarrow> Key servK \<notin> analz (spies evs)"
|
|
1334 |
apply (drule authK_authentic, assumption, assumption)
|
|
1335 |
apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
|
|
1336 |
done
|
|
1337 |
|
|
1338 |
lemma Confidentiality_B:
|
|
1339 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
1340 |
\<in> parts (spies evs);
|
|
1341 |
Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
1342 |
\<in> parts (spies evs);
|
|
1343 |
Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
|
|
1344 |
\<in> parts (spies evs);
|
|
1345 |
\<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
|
|
1346 |
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
|
|
1347 |
\<Longrightarrow> Key servK \<notin> analz (spies evs)"
|
|
1348 |
apply (frule authK_authentic)
|
|
1349 |
apply (frule_tac [3] Confidentiality_Kas)
|
|
1350 |
apply (frule_tac [6] servTicket_authentic, auto)
|
|
1351 |
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
|
|
1352 |
done
|
|
1353 |
|
|
1354 |
lemma u_Confidentiality_B:
|
|
1355 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
|
|
1356 |
\<in> parts (spies evs);
|
|
1357 |
\<not> expiredSK Ts evs;
|
|
1358 |
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
|
|
1359 |
\<Longrightarrow> Key servK \<notin> analz (spies evs)"
|
|
1360 |
apply (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
|
|
1361 |
done
|
|
1362 |
|
|
1363 |
|
|
1364 |
|
|
1365 |
subsection{*2. Parties' strong authentication:
|
|
1366 |
non-injective agreement on the session key. The same guarantees also
|
|
1367 |
express key distribution, hence their names*}
|
|
1368 |
|
|
1369 |
text{*Authentication here still is weak agreement - of B with A*}
|
|
1370 |
lemma A_authenticates_B:
|
|
1371 |
"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
|
|
1372 |
Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
|
|
1373 |
\<in> parts (spies evs);
|
|
1374 |
Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
|
|
1375 |
\<in> parts (spies evs);
|
|
1376 |
Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
|
|
1377 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1378 |
\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
|
|
1379 |
apply (frule authK_authentic)
|
|
1380 |
apply assumption+
|
|
1381 |
apply (frule servK_authentic)
|
|
1382 |
prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form)
|
|
1383 |
apply assumption+
|
|
1384 |
apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6)
|
|
1385 |
(*Single command proof: slower!
|
|
1386 |
apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6)
|
|
1387 |
*)
|
|
1388 |
done
|
|
1389 |
|
|
1390 |
(*These two have never been proved, because never were they needed before!*)
|
|
1391 |
lemma shrK_in_initState_Server[iff]: "Key (shrK A) \<in> initState Kas"
|
|
1392 |
by (induct_tac "A", auto)
|
|
1393 |
lemma shrK_in_knows_Server [iff]: "Key (shrK A) \<in> knows Kas evs"
|
|
1394 |
by (simp add: initState_subset_knows [THEN subsetD])
|
|
1395 |
(*Because of our simple model of Tgs, the equivalent for it required an axiom*)
|
|
1396 |
|
|
1397 |
|
|
1398 |
lemma A_authenticates_and_keydist_to_Kas:
|
|
1399 |
"\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs;
|
|
1400 |
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1401 |
\<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs
|
|
1402 |
\<and> Key authK \<in> analz(knows Kas evs)"
|
|
1403 |
apply (force dest!: authK_authentic Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
|
|
1404 |
done
|
|
1405 |
|
|
1406 |
|
|
1407 |
lemma K3_imp_Gets:
|
|
1408 |
"\<lbrakk> Says A Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
|
|
1409 |
Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
|
|
1410 |
\<in> set evs; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1411 |
\<Longrightarrow> Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
|
|
1412 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
|
|
1413 |
\<in> set evs"
|
|
1414 |
apply (erule rev_mp)
|
|
1415 |
apply (erule kerbIV_gets.induct)
|
|
1416 |
apply auto
|
|
1417 |
apply (blast dest: authTicket_form)
|
|
1418 |
done
|
|
1419 |
|
|
1420 |
lemma Tgs_authenticates_and_keydist_to_A:
|
|
1421 |
"\<lbrakk> Gets Tgs \<lbrace>
|
|
1422 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
|
|
1423 |
Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs;
|
|
1424 |
Key authK \<notin> analz (spies evs); A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1425 |
\<Longrightarrow> \<exists> B. Says A Tgs \<lbrace>
|
|
1426 |
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>,
|
|
1427 |
Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B \<rbrace> \<in> set evs
|
|
1428 |
\<and> Key authK \<in> analz (knows A evs)"
|
|
1429 |
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
|
|
1430 |
apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN parts.Fst], assumption)
|
|
1431 |
apply (drule Tgs_authenticates_A, assumption+, simp)
|
|
1432 |
apply (force dest!: K3_imp_Gets Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
|
|
1433 |
done
|
|
1434 |
|
|
1435 |
lemma K4_imp_Gets:
|
|
1436 |
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1437 |
\<in> set evs; evs \<in> kerbIV_gets \<rbrakk>
|
|
1438 |
\<Longrightarrow> \<exists> Ta X.
|
|
1439 |
Gets Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>, X\<rbrace>
|
|
1440 |
\<in> set evs"
|
|
1441 |
apply (erule rev_mp)
|
|
1442 |
apply (erule kerbIV_gets.induct)
|
|
1443 |
apply auto
|
|
1444 |
done
|
|
1445 |
|
|
1446 |
lemma A_authenticates_and_keydist_to_Tgs:
|
|
1447 |
"\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
|
|
1448 |
\<in> set evs;
|
|
1449 |
Gets A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1450 |
\<in> set evs;
|
|
1451 |
Key authK \<notin> analz (spies evs); A \<notin> bad;
|
|
1452 |
evs \<in> kerbIV_gets \<rbrakk>
|
|
1453 |
\<Longrightarrow> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
|
|
1454 |
\<in> set evs
|
|
1455 |
\<and> Key authK \<in> analz (knows Tgs evs)
|
|
1456 |
\<and> Key servK \<in> analz (knows Tgs evs)"
|
|
1457 |
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
|
|
1458 |
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
|
|
1459 |
apply (frule authK_authentic, assumption+)
|
|
1460 |
apply (drule servK_authentic_ter, assumption+)
|
|
1461 |
apply (frule K4_imp_Gets, assumption, erule exE, erule exE)
|
|
1462 |
apply (drule Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst], assumption, force)
|
|
1463 |
apply (frule Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
|
|
1464 |
apply (force dest!: authK_authentic Says_Kas_message_form)
|
|
1465 |
apply simp
|
|
1466 |
done
|
|
1467 |
|
|
1468 |
lemma K5_imp_Gets:
|
|
1469 |
"\<lbrakk> Says A B \<lbrace>servTicket, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs;
|
|
1470 |
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1471 |
\<Longrightarrow> \<exists> authK Ts authTicket T2.
|
|
1472 |
Gets A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>) \<in> set evs
|
|
1473 |
\<and> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace> \<in> set evs"
|
|
1474 |
apply (erule rev_mp)
|
|
1475 |
apply (erule kerbIV_gets.induct)
|
|
1476 |
apply auto
|
|
1477 |
done
|
|
1478 |
|
|
1479 |
lemma K3_imp_Gets:
|
|
1480 |
"\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
|
|
1481 |
\<in> set evs;
|
|
1482 |
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1483 |
\<Longrightarrow> \<exists> Ta. Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs";
|
|
1484 |
apply (erule rev_mp)
|
|
1485 |
apply (erule kerbIV_gets.induct)
|
|
1486 |
apply auto
|
|
1487 |
done
|
|
1488 |
|
|
1489 |
lemma B_authenticates_and_keydist_to_A:
|
|
1490 |
"\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
|
|
1491 |
Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs;
|
|
1492 |
Key servK \<notin> analz (spies evs);
|
|
1493 |
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
|
|
1494 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
|
|
1495 |
Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs
|
|
1496 |
\<and> Key servK \<in> analz (knows A evs)"
|
|
1497 |
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst, THEN servTicket_authentic_Tgs], assumption+)
|
|
1498 |
apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption)
|
|
1499 |
apply (erule exE, drule Says_K5, assumption+)
|
|
1500 |
apply (frule K5_imp_Gets, assumption+)
|
|
1501 |
apply clarify
|
|
1502 |
apply (drule K3_imp_Gets, assumption+)
|
|
1503 |
apply (erule exE)
|
|
1504 |
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN authK_authentic, THEN Says_Kas_message_form], assumption+, clarify)
|
|
1505 |
apply (force dest!: Gets_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
|
|
1506 |
done
|
|
1507 |
|
|
1508 |
|
|
1509 |
lemma K6_imp_Gets:
|
|
1510 |
"\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
|
|
1511 |
B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1512 |
\<Longrightarrow> \<exists> Ts X. Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,X\<rbrace>
|
|
1513 |
\<in> set evs"
|
|
1514 |
apply (erule rev_mp)
|
|
1515 |
apply (erule kerbIV_gets.induct)
|
|
1516 |
apply auto
|
|
1517 |
done
|
|
1518 |
|
|
1519 |
|
|
1520 |
lemma A_authenticates_and_keydist_to_B:
|
|
1521 |
"\<lbrakk> Gets A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>,
|
|
1522 |
Crypt servK (Number T3)\<rbrace> \<in> set evs;
|
|
1523 |
Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>)
|
|
1524 |
\<in> set evs;
|
|
1525 |
Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
|
|
1526 |
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
|
|
1527 |
\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs
|
|
1528 |
\<and> Key servK \<in> analz (knows B evs)"
|
|
1529 |
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst], assumption)
|
|
1530 |
apply (drule Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd], assumption)
|
|
1531 |
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
|
|
1532 |
apply (drule A_authenticates_B, assumption+)
|
|
1533 |
apply (force dest!: K6_imp_Gets Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
|
|
1534 |
done
|
|
1535 |
|
|
1536 |
|
|
1537 |
|
|
1538 |
end
|
|
1539 |
|