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