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