18886
|
1 |
(* ID: $Id$
|
|
2 |
Author: Giampaolo Bella, Catania University
|
|
3 |
*)
|
|
4 |
|
|
5 |
header{*Theory of smartcards*}
|
|
6 |
|
|
7 |
theory Smartcard imports EventSC begin
|
|
8 |
|
|
9 |
text{*
|
|
10 |
As smartcards handle long-term (symmetric) keys, this theoy extends and
|
|
11 |
supersedes theory Private.thy
|
|
12 |
|
|
13 |
An agent is bad if she reveals her PIN to the spy, not the shared key that
|
|
14 |
is embedded in her card. An agent's being bad implies nothing about her
|
|
15 |
smartcard, which independently may be stolen or cloned.
|
|
16 |
*}
|
|
17 |
|
|
18 |
consts
|
|
19 |
shrK :: "agent => key" (*long-term keys saved in smart cards*)
|
|
20 |
crdK :: "card => key" (*smart cards' symmetric keys*)
|
|
21 |
pin :: "agent => key" (*pin to activate the smart cards*)
|
|
22 |
|
|
23 |
(*Mostly for Shoup-Rubin*)
|
|
24 |
Pairkey :: "agent * agent => nat"
|
|
25 |
pairK :: "agent * agent => key"
|
|
26 |
|
|
27 |
axioms
|
|
28 |
inj_shrK: "inj shrK" --{*No two smartcards store the same key*}
|
|
29 |
inj_crdK: "inj crdK" --{*Nor do two cards*}
|
|
30 |
inj_pin : "inj pin" --{*Nor do two agents have the same pin*}
|
|
31 |
|
|
32 |
(*pairK is injective on each component, if we assume encryption to be a PRF
|
|
33 |
or at least collision free *)
|
|
34 |
inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
|
|
35 |
comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
|
|
36 |
|
|
37 |
(*long-term keys differ from each other*)
|
|
38 |
pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
|
|
39 |
pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
|
|
40 |
pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P"
|
|
41 |
shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C"
|
|
42 |
shrK_disj_pin [iff]: "shrK P \<noteq> pin Q"
|
|
43 |
crdK_disj_pin [iff]: "crdK C \<noteq> pin P"
|
|
44 |
|
|
45 |
|
|
46 |
text{*All keys are symmetric*}
|
|
47 |
defs all_symmetric_def: "all_symmetric == True"
|
|
48 |
|
|
49 |
lemma isSym_keys: "K \<in> symKeys"
|
|
50 |
by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
|
|
51 |
|
|
52 |
|
|
53 |
constdefs
|
|
54 |
legalUse :: "card => bool" ("legalUse (_)")
|
|
55 |
"legalUse C == C \<notin> stolen"
|
|
56 |
|
|
57 |
consts
|
|
58 |
illegalUse :: "card => bool"
|
|
59 |
primrec
|
|
60 |
illegalUse_def:
|
|
61 |
"illegalUse (Card A) = ( (Card A \<in> stolen \<and> A \<in> bad) \<or> Card A \<in> cloned )"
|
|
62 |
|
|
63 |
|
|
64 |
text{*initState must be defined with care*}
|
|
65 |
primrec
|
|
66 |
(*Server knows all long-term keys; adding cards' keys may be redundant but
|
|
67 |
helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
|
|
68 |
from fresh (session) keys*)
|
|
69 |
initState_Server: "initState Server =
|
|
70 |
(Key`(range shrK \<union> range crdK \<union> range pin \<union> range pairK)) \<union>
|
|
71 |
(Nonce`(range Pairkey))"
|
|
72 |
|
|
73 |
(*Other agents know only their own*)
|
|
74 |
initState_Friend: "initState (Friend i) = {Key (pin (Friend i))}"
|
|
75 |
|
|
76 |
(*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
|
|
77 |
initState_Spy: "initState Spy =
|
|
78 |
(Key`((pin`bad) \<union> (pin `{A. Card A \<in> cloned}) \<union>
|
|
79 |
(shrK`{A. Card A \<in> cloned}) \<union>
|
|
80 |
(crdK`cloned) \<union>
|
|
81 |
(pairK`{(X,A). Card A \<in> cloned})))
|
|
82 |
\<union> (Nonce`(Pairkey`{(A,B). Card A \<in> cloned & Card B \<in> cloned}))"
|
|
83 |
|
|
84 |
|
|
85 |
text{*Still relying on axioms*}
|
|
86 |
axioms
|
|
87 |
Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
|
|
88 |
|
|
89 |
(*Needed because of Spy's knowledge of Pairkeys*)
|
|
90 |
Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
|
|
91 |
|
|
92 |
|
|
93 |
|
|
94 |
|
|
95 |
|
|
96 |
|
|
97 |
|
|
98 |
subsection{*Basic properties of shrK*}
|
|
99 |
|
|
100 |
(*Injectiveness: Agents' long-term keys are distinct.*)
|
|
101 |
declare inj_shrK [THEN inj_eq, iff]
|
|
102 |
declare inj_crdK [THEN inj_eq, iff]
|
|
103 |
declare inj_pin [THEN inj_eq, iff]
|
|
104 |
|
|
105 |
lemma invKey_K [simp]: "invKey K = K"
|
|
106 |
apply (insert isSym_keys)
|
|
107 |
apply (simp add: symKeys_def)
|
|
108 |
done
|
|
109 |
|
|
110 |
|
|
111 |
lemma analz_Decrypt' [dest]:
|
|
112 |
"\<lbrakk> Crypt K X \<in> analz H; Key K \<in> analz H \<rbrakk> \<Longrightarrow> X \<in> analz H"
|
|
113 |
by auto
|
|
114 |
|
|
115 |
text{*Now cancel the @{text dest} attribute given to
|
|
116 |
@{text analz.Decrypt} in its declaration.*}
|
|
117 |
declare analz.Decrypt [rule del]
|
|
118 |
|
|
119 |
text{*Rewrites should not refer to @{term "initState(Friend i)"} because
|
|
120 |
that expression is not in normal form.*}
|
|
121 |
|
|
122 |
text{*Added to extend initstate with set of nonces*}
|
|
123 |
lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N"
|
|
124 |
apply auto
|
|
125 |
apply (erule parts.induct)
|
|
126 |
apply auto
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
|
|
130 |
apply (unfold keysFor_def)
|
|
131 |
apply (induct_tac "C", auto)
|
|
132 |
done
|
|
133 |
|
|
134 |
(*Specialized to shared-key model: no @{term invKey}*)
|
|
135 |
lemma keysFor_parts_insert:
|
|
136 |
"\<lbrakk> K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) \<rbrakk>
|
|
137 |
\<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
|
|
138 |
by (force dest: EventSC.keysFor_parts_insert)
|
|
139 |
|
|
140 |
lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
|
|
141 |
by (drule Crypt_imp_invKey_keysFor, simp)
|
|
142 |
|
|
143 |
|
|
144 |
subsection{*Function "knows"*}
|
|
145 |
|
|
146 |
(*Spy knows the pins of bad agents!*)
|
|
147 |
lemma Spy_knows_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
|
|
148 |
apply (induct_tac "evs")
|
|
149 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
|
|
150 |
done
|
|
151 |
|
|
152 |
(*Spy knows the long-term keys of cloned cards!*)
|
|
153 |
lemma Spy_knows_cloned [intro!]:
|
|
154 |
"Card A \<in> cloned \<Longrightarrow> Key (crdK (Card A)) \<in> knows Spy evs &
|
|
155 |
Key (shrK A) \<in> knows Spy evs &
|
|
156 |
Key (pin A) \<in> knows Spy evs &
|
|
157 |
(\<forall> B. Key (pairK(B,A)) \<in> knows Spy evs)"
|
|
158 |
apply (induct_tac "evs")
|
|
159 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
|
|
160 |
done
|
|
161 |
|
|
162 |
lemma Spy_knows_cloned1 [intro!]: "C \<in> cloned \<Longrightarrow> Key (crdK C) \<in> knows Spy evs"
|
|
163 |
apply (induct_tac "evs")
|
|
164 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
|
|
165 |
done
|
|
166 |
|
|
167 |
lemma Spy_knows_cloned2 [intro!]: "\<lbrakk> Card A \<in> cloned; Card B \<in> cloned \<rbrakk>
|
|
168 |
\<Longrightarrow> Nonce (Pairkey(A,B))\<in> knows Spy evs"
|
|
169 |
apply (induct_tac "evs")
|
|
170 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
|
|
171 |
done
|
|
172 |
|
|
173 |
(*Spy only knows pins of bad agents!*)
|
|
174 |
lemma Spy_knows_Spy_bad [intro!]: "A\<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
|
|
175 |
apply (induct_tac "evs")
|
|
176 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
|
|
177 |
done
|
|
178 |
|
|
179 |
|
|
180 |
(*For case analysis on whether or not an agent is compromised*)
|
|
181 |
lemma Crypt_Spy_analz_bad:
|
|
182 |
"\<lbrakk> Crypt (pin A) X \<in> analz (knows Spy evs); A\<in>bad \<rbrakk>
|
|
183 |
\<Longrightarrow> X \<in> analz (knows Spy evs)"
|
|
184 |
apply (force dest!: analz.Decrypt)
|
|
185 |
done
|
|
186 |
|
|
187 |
(** Fresh keys never clash with other keys **)
|
|
188 |
|
|
189 |
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState Server"
|
|
190 |
apply (induct_tac "A")
|
|
191 |
apply auto
|
|
192 |
done
|
|
193 |
|
|
194 |
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
|
|
195 |
apply (rule initState_into_used)
|
|
196 |
apply blast
|
|
197 |
done
|
|
198 |
|
|
199 |
lemma crdK_in_initState [iff]: "Key (crdK A) \<in> initState Server"
|
|
200 |
apply (induct_tac "A")
|
|
201 |
apply auto
|
|
202 |
done
|
|
203 |
|
|
204 |
lemma crdK_in_used [iff]: "Key (crdK A) \<in> used evs"
|
|
205 |
apply (rule initState_into_used)
|
|
206 |
apply blast
|
|
207 |
done
|
|
208 |
|
|
209 |
lemma pin_in_initState [iff]: "Key (pin A) \<in> initState A"
|
|
210 |
apply (induct_tac "A")
|
|
211 |
apply auto
|
|
212 |
done
|
|
213 |
|
|
214 |
lemma pin_in_used [iff]: "Key (pin A) \<in> used evs"
|
|
215 |
apply (rule initState_into_used)
|
|
216 |
apply blast
|
|
217 |
done
|
|
218 |
|
|
219 |
lemma pairK_in_initState [iff]: "Key (pairK X) \<in> initState Server"
|
|
220 |
apply (induct_tac "X")
|
|
221 |
apply auto
|
|
222 |
done
|
|
223 |
|
|
224 |
lemma pairK_in_used [iff]: "Key (pairK X) \<in> used evs"
|
|
225 |
apply (rule initState_into_used)
|
|
226 |
apply blast
|
|
227 |
done
|
|
228 |
|
|
229 |
|
|
230 |
|
|
231 |
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
|
|
232 |
from long-term shared keys*)
|
|
233 |
lemma Key_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range shrK"
|
|
234 |
by blast
|
|
235 |
|
|
236 |
lemma shrK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> shrK B \<noteq> K"
|
|
237 |
by blast
|
|
238 |
|
|
239 |
lemma crdK_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range crdK"
|
|
240 |
apply clarify
|
|
241 |
done
|
|
242 |
|
|
243 |
lemma crdK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> crdK C \<noteq> K"
|
|
244 |
apply clarify
|
|
245 |
done
|
|
246 |
|
|
247 |
lemma pin_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range pin"
|
|
248 |
apply clarify
|
|
249 |
done
|
|
250 |
|
|
251 |
lemma pin_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> pin A \<noteq> K"
|
|
252 |
apply clarify
|
|
253 |
done
|
|
254 |
|
|
255 |
lemma pairK_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range pairK"
|
|
256 |
apply clarify
|
|
257 |
done
|
|
258 |
|
|
259 |
lemma pairK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> pairK(A,B) \<noteq> K"
|
|
260 |
apply clarify
|
|
261 |
done
|
|
262 |
|
|
263 |
declare shrK_neq [THEN not_sym, simp]
|
|
264 |
declare crdK_neq [THEN not_sym, simp]
|
|
265 |
declare pin_neq [THEN not_sym, simp]
|
|
266 |
declare pairK_neq [THEN not_sym, simp]
|
|
267 |
|
|
268 |
|
|
269 |
subsection{*Fresh nonces*}
|
|
270 |
|
|
271 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState (Friend i))"
|
|
272 |
by auto
|
|
273 |
|
|
274 |
|
|
275 |
(*This lemma no longer holds of smartcard protocols, where the cards can store
|
|
276 |
nonces.
|
|
277 |
|
|
278 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
|
|
279 |
apply (simp (no_asm) add: used_Nil)
|
|
280 |
done
|
|
281 |
|
|
282 |
So, we must use old-style supply fresh nonce theorems relying on the appropriate axiom*)
|
|
283 |
|
|
284 |
|
|
285 |
subsection{*Supply fresh nonces for possibility theorems.*}
|
|
286 |
|
|
287 |
|
|
288 |
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
|
|
289 |
apply (rule Finites.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
|
|
290 |
done
|
|
291 |
|
|
292 |
lemma Nonce_supply2:
|
|
293 |
"\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
|
|
294 |
apply (cut_tac evs = evs in Finites.emptyI [THEN Nonce_supply_ax])
|
|
295 |
apply (erule exE)
|
|
296 |
apply (cut_tac evs = evs' in Finites.emptyI [THEN Finites.insertI, THEN Nonce_supply_ax])
|
|
297 |
apply auto
|
|
298 |
done
|
|
299 |
|
|
300 |
|
|
301 |
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &
|
|
302 |
Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
|
|
303 |
apply (cut_tac evs = evs in Finites.emptyI [THEN Nonce_supply_ax])
|
|
304 |
apply (erule exE)
|
|
305 |
apply (cut_tac evs = evs' and a1 = N in Finites.emptyI [THEN Finites.insertI, THEN Nonce_supply_ax])
|
|
306 |
apply (erule exE)
|
|
307 |
apply (cut_tac evs = evs'' and a1 = Na and a2 = N in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Nonce_supply_ax])
|
|
308 |
apply blast
|
|
309 |
done
|
|
310 |
|
|
311 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
|
|
312 |
apply (rule Finites.emptyI [THEN Nonce_supply_ax, THEN exE])
|
|
313 |
apply (rule someI, blast)
|
|
314 |
done
|
|
315 |
|
|
316 |
|
|
317 |
|
|
318 |
text{*Unlike the corresponding property of nonces, we cannot prove
|
|
319 |
@{term "finite KK \<Longrightarrow> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
|
|
320 |
We have infinitely many agents and there is nothing to stop their
|
|
321 |
long-term keys from exhausting all the natural numbers. Instead,
|
|
322 |
possibility theorems must assume the existence of a few keys.*}
|
|
323 |
|
|
324 |
|
|
325 |
subsection{*Tactics for possibility theorems*}
|
|
326 |
|
|
327 |
ML
|
|
328 |
{*
|
|
329 |
val inj_shrK = thm "inj_shrK";
|
|
330 |
val isSym_keys = thm "isSym_keys";
|
|
331 |
val Nonce_supply = thm "Nonce_supply";
|
|
332 |
val invKey_K = thm "invKey_K";
|
|
333 |
val analz_Decrypt' = thm "analz_Decrypt'";
|
|
334 |
val keysFor_parts_initState = thm "keysFor_parts_initState";
|
|
335 |
val keysFor_parts_insert = thm "keysFor_parts_insert";
|
|
336 |
val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
|
|
337 |
val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
|
|
338 |
val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
|
|
339 |
val shrK_in_initState = thm "shrK_in_initState";
|
|
340 |
val shrK_in_used = thm "shrK_in_used";
|
|
341 |
val Key_not_used = thm "Key_not_used";
|
|
342 |
val shrK_neq = thm "shrK_neq";
|
|
343 |
val Nonce_notin_initState = thm "Nonce_notin_initState";
|
|
344 |
val Nonce_supply1 = thm "Nonce_supply1";
|
|
345 |
val Nonce_supply2 = thm "Nonce_supply2";
|
|
346 |
val Nonce_supply3 = thm "Nonce_supply3";
|
|
347 |
val Nonce_supply = thm "Nonce_supply";
|
|
348 |
val used_Says = thm "used_Says";
|
|
349 |
val used_Gets = thm "used_Gets";
|
|
350 |
val used_Notes = thm "used_Notes";
|
|
351 |
val used_Inputs = thm "used_Inputs";
|
|
352 |
val used_C_Gets = thm "used_C_Gets";
|
|
353 |
val used_Outpts = thm "used_Outpts";
|
|
354 |
val used_A_Gets = thm "used_A_Gets";
|
|
355 |
*}
|
|
356 |
|
|
357 |
|
|
358 |
ML
|
|
359 |
{*
|
|
360 |
(*Omitting used_Says makes the tactic much faster: it leaves expressions
|
|
361 |
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
|
|
362 |
fun gen_possibility_tac ss state = state |>
|
|
363 |
(REPEAT
|
|
364 |
(ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets,
|
|
365 |
used_Inputs, used_C_Gets, used_Outpts, used_A_Gets]
|
|
366 |
setSolver safe_solver))
|
|
367 |
THEN
|
|
368 |
REPEAT_FIRST (eq_assume_tac ORELSE'
|
|
369 |
resolve_tac [refl, conjI, Nonce_supply])))
|
|
370 |
|
|
371 |
(*Tactic for possibility theorems (ML script version)*)
|
|
372 |
fun possibility_tac state = gen_possibility_tac (simpset()) state
|
|
373 |
|
|
374 |
(*For harder protocols (such as Recur) where we have to set up some
|
|
375 |
nonces and keys initially*)
|
|
376 |
fun basic_possibility_tac st = st |>
|
|
377 |
REPEAT
|
|
378 |
(ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
|
|
379 |
THEN
|
|
380 |
REPEAT_FIRST (resolve_tac [refl, conjI]))
|
|
381 |
*}
|
|
382 |
|
|
383 |
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
|
|
384 |
|
|
385 |
lemma subset_Compl_range_shrK: "A \<subseteq> - (range shrK) \<Longrightarrow> shrK x \<notin> A"
|
|
386 |
by blast
|
|
387 |
|
|
388 |
lemma subset_Compl_range_crdK: "A \<subseteq> - (range crdK) \<Longrightarrow> crdK x \<notin> A"
|
|
389 |
apply blast
|
|
390 |
done
|
|
391 |
|
|
392 |
lemma subset_Compl_range_pin: "A \<subseteq> - (range pin) \<Longrightarrow> pin x \<notin> A"
|
|
393 |
apply blast
|
|
394 |
done
|
|
395 |
|
|
396 |
lemma subset_Compl_range_pairK: "A \<subseteq> - (range pairK) \<Longrightarrow> pairK x \<notin> A"
|
|
397 |
apply blast
|
|
398 |
done
|
|
399 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
|
|
400 |
by blast
|
|
401 |
|
|
402 |
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
|
|
403 |
by blast
|
|
404 |
|
|
405 |
(** Reverse the normal simplification of "image" to build up (not break down)
|
|
406 |
the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to
|
|
407 |
erase occurrences of forwarded message components (X). **)
|
|
408 |
|
|
409 |
lemmas analz_image_freshK_simps =
|
|
410 |
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
|
|
411 |
disj_comms
|
|
412 |
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
|
|
413 |
analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
|
|
414 |
insert_Key_singleton subset_Compl_range_shrK subset_Compl_range_crdK
|
|
415 |
subset_Compl_range_pin subset_Compl_range_pairK
|
|
416 |
Key_not_used insert_Key_image Un_assoc [THEN sym]
|
|
417 |
|
|
418 |
(*Lemma for the trivial direction of the if-and-only-if*)
|
|
419 |
lemma analz_image_freshK_lemma:
|
|
420 |
"(Key K \<in> analz (Key`nE \<union> H)) \<longrightarrow> (K \<in> nE | Key K \<in> analz H) \<Longrightarrow>
|
|
421 |
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
|
|
422 |
by (blast intro: analz_mono [THEN [2] rev_subsetD])
|
|
423 |
|
|
424 |
ML
|
|
425 |
{*
|
|
426 |
val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
|
|
427 |
|
|
428 |
val analz_image_freshK_ss =
|
|
429 |
simpset() delsimps [image_insert, image_Un]
|
|
430 |
delsimps [imp_disjL] (*reduces blow-up*)
|
|
431 |
addsimps thms "analz_image_freshK_simps"
|
|
432 |
*}
|
|
433 |
|
|
434 |
|
|
435 |
|
|
436 |
(*Lets blast_tac perform this step without needing the simplifier*)
|
|
437 |
lemma invKey_shrK_iff [iff]:
|
|
438 |
"(Key (invKey K) \<in> X) = (Key K \<in> X)"
|
|
439 |
by auto
|
|
440 |
|
|
441 |
(*Specialized methods*)
|
|
442 |
|
|
443 |
method_setup analz_freshK = {*
|
|
444 |
Method.no_args
|
|
445 |
(Method.METHOD
|
|
446 |
(fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
|
|
447 |
REPEAT_FIRST (rtac analz_image_freshK_lemma),
|
|
448 |
ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
|
|
449 |
"for proving the Session Key Compromise theorem"
|
|
450 |
|
|
451 |
method_setup possibility = {*
|
|
452 |
Method.ctxt_args (fn ctxt =>
|
|
453 |
Method.METHOD (fn facts =>
|
|
454 |
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
|
|
455 |
"for proving possibility theorems"
|
|
456 |
|
|
457 |
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
|
|
458 |
by (induct e, auto simp: knows_Cons)
|
|
459 |
|
|
460 |
(*Needed for actual protocols that will follow*)
|
|
461 |
declare shrK_disj_crdK[THEN not_sym, iff]
|
|
462 |
declare shrK_disj_pin[THEN not_sym, iff]
|
|
463 |
declare pairK_disj_shrK[THEN not_sym, iff]
|
|
464 |
declare pairK_disj_crdK[THEN not_sym, iff]
|
|
465 |
declare pairK_disj_pin[THEN not_sym, iff]
|
|
466 |
declare crdK_disj_pin[THEN not_sym, iff]
|
|
467 |
|
|
468 |
declare legalUse_def [iff] illegalUse_def [iff]
|
|
469 |
|
|
470 |
|
|
471 |
|
|
472 |
|
|
473 |
|
|
474 |
end
|