author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 46471 | 2289a3869c88 |
child 53428 | 3083c611ec40 |
permissions | -rw-r--r-- |
18886 | 1 |
header{*Theory of Events for Security Protocols that use smartcards*} |
2 |
||
3 |
theory EventSC imports "../Message" begin |
|
4 |
||
5 |
consts (*Initial states of agents -- parameter of the construction*) |
|
6 |
initState :: "agent => msg set" |
|
7 |
||
8 |
datatype card = Card agent |
|
9 |
||
10 |
text{*Four new events express the traffic between an agent and his card*} |
|
11 |
datatype |
|
12 |
event = Says agent agent msg |
|
13 |
| Notes agent msg |
|
14 |
| Gets agent msg |
|
15 |
| Inputs agent card msg (*Agent sends to card and\<dots>*) |
|
16 |
| C_Gets card msg (*\<dots> card receives it*) |
|
17 |
| Outpts card agent msg (*Card sends to agent and\<dots>*) |
|
18 |
| A_Gets agent msg (*agent receives it*) |
|
19 |
||
20 |
consts |
|
21 |
bad :: "agent set" (*compromised agents*) |
|
22 |
stolen :: "card set" (* stolen smart cards *) |
|
23 |
cloned :: "card set" (* cloned smart cards*) |
|
24 |
secureM :: "bool"(*assumption of secure means between agents and their cards*) |
|
25 |
||
20768 | 26 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
27 |
insecureM :: bool where (*certain protocols make no assumption of secure means*) |
20768 | 28 |
"insecureM == \<not>secureM" |
18886 | 29 |
|
30 |
||
31 |
text{*Spy has access to his own key for spoof messages, but Server is secure*} |
|
32 |
specification (bad) |
|
33 |
Spy_in_bad [iff]: "Spy \<in> bad" |
|
34 |
Server_not_bad [iff]: "Server \<notin> bad" |
|
35 |
apply (rule exI [of _ "{Spy}"], simp) done |
|
36 |
||
37 |
specification (stolen) |
|
38 |
(*The server's card is secure by assumption\<dots>*) |
|
39 |
Card_Server_not_stolen [iff]: "Card Server \<notin> stolen" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
40 |
Card_Spy_not_stolen [iff]: "Card Spy \<notin> stolen" |
18886 | 41 |
apply blast done |
42 |
||
43 |
specification (cloned) |
|
44 |
(*\<dots> the spy's card is secure because she already can use it freely*) |
|
45 |
Card_Server_not_cloned [iff]: "Card Server \<notin> cloned" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
46 |
Card_Spy_not_cloned [iff]: "Card Spy \<notin> cloned" |
18886 | 47 |
apply blast done |
48 |
||
49 |
||
50 |
primrec (*This definition is extended over the new events, subject to the |
|
51 |
assumption of secure means*) |
|
39246 | 52 |
knows :: "agent => event list => msg set" (*agents' knowledge*) where |
53 |
knows_Nil: "knows A [] = initState A" | |
|
18886 | 54 |
knows_Cons: "knows A (ev # evs) = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
55 |
(case ev of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
56 |
Says A' B X => |
18886 | 57 |
if (A=A' | A=Spy) then insert X (knows A evs) else knows A evs |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
58 |
| Notes A' X => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
59 |
if (A=A' | (A=Spy & A'\<in>bad)) then insert X (knows A evs) |
18886 | 60 |
else knows A evs |
61 |
| Gets A' X => |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
62 |
if (A=A' & A \<noteq> Spy) then insert X (knows A evs) |
18886 | 63 |
else knows A evs |
64 |
| Inputs A' C X => |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
65 |
if secureM then |
18886 | 66 |
if A=A' then insert X (knows A evs) else knows A evs |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
67 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
68 |
if (A=A' | A=Spy) then insert X (knows A evs) else knows A evs |
18886 | 69 |
| C_Gets C X => knows A evs |
70 |
| Outpts C A' X => |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
71 |
if secureM then |
18886 | 72 |
if A=A' then insert X (knows A evs) else knows A evs |
73 |
else |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
74 |
if A=Spy then insert X (knows A evs) else knows A evs |
18886 | 75 |
| A_Gets A' X => |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
76 |
if (A=A' & A \<noteq> Spy) then insert X (knows A evs) |
18886 | 77 |
else knows A evs)" |
78 |
||
79 |
||
80 |
||
39246 | 81 |
primrec |
18886 | 82 |
(*The set of items that might be visible to someone is easily extended |
83 |
over the new events*) |
|
39246 | 84 |
used :: "event list => msg set" where |
85 |
used_Nil: "used [] = (UN B. parts (initState B))" | |
|
18886 | 86 |
used_Cons: "used (ev # evs) = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
87 |
(case ev of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
88 |
Says A B X => parts {X} \<union> (used evs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
89 |
| Notes A X => parts {X} \<union> (used evs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
90 |
| Gets A X => used evs |
18886 | 91 |
| Inputs A C X => parts{X} \<union> (used evs) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
92 |
| C_Gets C X => used evs |
18886 | 93 |
| Outpts C A X => parts{X} \<union> (used evs) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26302
diff
changeset
|
94 |
| A_Gets A X => used evs)" |
18886 | 95 |
--{*@{term Gets} always follows @{term Says} in real protocols. |
96 |
Likewise, @{term C_Gets} will always have to follow @{term Inputs} |
|
97 |
and @{term A_Gets} will always have to follow @{term Outpts}*} |
|
98 |
||
99 |
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs" |
|
100 |
apply (induct_tac evs) |
|
101 |
apply (auto split: event.split) |
|
102 |
done |
|
103 |
||
104 |
lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> used evs" |
|
105 |
apply (induct_tac evs) |
|
106 |
apply (auto split: event.split) |
|
107 |
done |
|
108 |
||
109 |
lemma MPair_used [rule_format]: |
|
110 |
"MPair X Y \<in> used evs \<longrightarrow> X \<in> used evs & Y \<in> used evs" |
|
111 |
apply (induct_tac evs) |
|
112 |
apply (auto split: event.split) |
|
113 |
done |
|
114 |
||
115 |
||
116 |
subsection{*Function @{term knows}*} |
|
117 |
||
118 |
(*Simplifying |
|
119 |
parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs). |
|
120 |
This version won't loop with the simplifier.*) |
|
45605 | 121 |
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs |
18886 | 122 |
|
123 |
lemma knows_Spy_Says [simp]: |
|
124 |
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)" |
|
125 |
by simp |
|
126 |
||
127 |
text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits |
|
128 |
on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*} |
|
129 |
lemma knows_Spy_Notes [simp]: |
|
130 |
"knows Spy (Notes A X # evs) = |
|
131 |
(if A\<in>bad then insert X (knows Spy evs) else knows Spy evs)" |
|
132 |
by simp |
|
133 |
||
134 |
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs" |
|
135 |
by simp |
|
136 |
||
137 |
lemma knows_Spy_Inputs_secureM [simp]: |
|
138 |
"secureM \<Longrightarrow> knows Spy (Inputs A C X # evs) = |
|
139 |
(if A=Spy then insert X (knows Spy evs) else knows Spy evs)" |
|
140 |
by simp |
|
141 |
||
142 |
lemma knows_Spy_Inputs_insecureM [simp]: |
|
143 |
"insecureM \<Longrightarrow> knows Spy (Inputs A C X # evs) = insert X (knows Spy evs)" |
|
144 |
by simp |
|
145 |
||
146 |
lemma knows_Spy_C_Gets [simp]: "knows Spy (C_Gets C X # evs) = knows Spy evs" |
|
147 |
by simp |
|
148 |
||
149 |
lemma knows_Spy_Outpts_secureM [simp]: |
|
150 |
"secureM \<Longrightarrow> knows Spy (Outpts C A X # evs) = |
|
151 |
(if A=Spy then insert X (knows Spy evs) else knows Spy evs)" |
|
152 |
by simp |
|
153 |
||
154 |
lemma knows_Spy_Outpts_insecureM [simp]: |
|
155 |
"insecureM \<Longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)" |
|
156 |
by simp |
|
157 |
||
158 |
lemma knows_Spy_A_Gets [simp]: "knows Spy (A_Gets A X # evs) = knows Spy evs" |
|
159 |
by simp |
|
160 |
||
161 |
||
162 |
||
163 |
||
164 |
lemma knows_Spy_subset_knows_Spy_Says: |
|
165 |
"knows Spy evs \<subseteq> knows Spy (Says A B X # evs)" |
|
166 |
by (simp add: subset_insertI) |
|
167 |
||
168 |
lemma knows_Spy_subset_knows_Spy_Notes: |
|
169 |
"knows Spy evs \<subseteq> knows Spy (Notes A X # evs)" |
|
170 |
by force |
|
171 |
||
172 |
lemma knows_Spy_subset_knows_Spy_Gets: |
|
173 |
"knows Spy evs \<subseteq> knows Spy (Gets A X # evs)" |
|
174 |
by (simp add: subset_insertI) |
|
175 |
||
176 |
lemma knows_Spy_subset_knows_Spy_Inputs: |
|
177 |
"knows Spy evs \<subseteq> knows Spy (Inputs A C X # evs)" |
|
178 |
by auto |
|
179 |
||
180 |
lemma knows_Spy_equals_knows_Spy_Gets: |
|
181 |
"knows Spy evs = knows Spy (C_Gets C X # evs)" |
|
182 |
by (simp add: subset_insertI) |
|
183 |
||
184 |
lemma knows_Spy_subset_knows_Spy_Outpts: "knows Spy evs \<subseteq> knows Spy (Outpts C A X # evs)" |
|
185 |
by auto |
|
186 |
||
187 |
lemma knows_Spy_subset_knows_Spy_A_Gets: "knows Spy evs \<subseteq> knows Spy (A_Gets A X # evs)" |
|
188 |
by (simp add: subset_insertI) |
|
189 |
||
190 |
||
191 |
||
192 |
text{*Spy sees what is sent on the traffic*} |
|
193 |
lemma Says_imp_knows_Spy [rule_format]: |
|
194 |
"Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs" |
|
195 |
apply (induct_tac "evs") |
|
196 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
197 |
done |
|
198 |
||
199 |
lemma Notes_imp_knows_Spy [rule_format]: |
|
200 |
"Notes A X \<in> set evs \<longrightarrow> A\<in> bad \<longrightarrow> X \<in> knows Spy evs" |
|
201 |
apply (induct_tac "evs") |
|
202 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
203 |
done |
|
204 |
||
205 |
(*Nothing can be stated on a Gets event*) |
|
206 |
||
207 |
lemma Inputs_imp_knows_Spy_secureM [rule_format (no_asm)]: |
|
208 |
"Inputs Spy C X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs" |
|
209 |
apply (induct_tac "evs") |
|
210 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
211 |
done |
|
212 |
||
213 |
lemma Inputs_imp_knows_Spy_insecureM [rule_format (no_asm)]: |
|
214 |
"Inputs A C X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs" |
|
215 |
apply (induct_tac "evs") |
|
216 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
217 |
done |
|
218 |
||
219 |
(*Nothing can be stated on a C_Gets event*) |
|
220 |
||
221 |
lemma Outpts_imp_knows_Spy_secureM [rule_format (no_asm)]: |
|
222 |
"Outpts C Spy X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs" |
|
223 |
apply (induct_tac "evs") |
|
224 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
225 |
done |
|
226 |
||
227 |
lemma Outpts_imp_knows_Spy_insecureM [rule_format (no_asm)]: |
|
228 |
"Outpts C A X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs" |
|
229 |
apply (induct_tac "evs") |
|
230 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
231 |
done |
|
232 |
||
233 |
(*Nothing can be stated on an A_Gets event*) |
|
234 |
||
235 |
||
236 |
||
237 |
text{*Elimination rules: derive contradictions from old Says events containing |
|
238 |
items known to be fresh*} |
|
239 |
lemmas knows_Spy_partsEs = |
|
46471 | 240 |
Says_imp_knows_Spy [THEN parts.Inj, elim_format] |
241 |
parts.Body [elim_format] |
|
18886 | 242 |
|
243 |
||
244 |
||
245 |
subsection{*Knowledge of Agents*} |
|
246 |
||
247 |
lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)" |
|
248 |
by simp |
|
249 |
||
250 |
lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)" |
|
251 |
by simp |
|
252 |
||
253 |
lemma knows_Gets: |
|
254 |
"A \<noteq> Spy \<longrightarrow> knows A (Gets A X # evs) = insert X (knows A evs)" |
|
255 |
by simp |
|
256 |
||
257 |
lemma knows_Inputs: "knows A (Inputs A C X # evs) = insert X (knows A evs)" |
|
258 |
by simp |
|
259 |
||
260 |
lemma knows_C_Gets: "knows A (C_Gets C X # evs) = knows A evs" |
|
261 |
by simp |
|
262 |
||
263 |
lemma knows_Outpts_secureM: |
|
264 |
"secureM \<longrightarrow> knows A (Outpts C A X # evs) = insert X (knows A evs)" |
|
265 |
by simp |
|
266 |
||
26302
68b073052e8c
proper naming of knows_Outpts_insecureM, knows_subset_knows_A_Gets;
wenzelm
parents:
21404
diff
changeset
|
267 |
lemma knows_Outpts_insecureM: |
18886 | 268 |
"insecureM \<longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)" |
269 |
by simp |
|
270 |
(*somewhat equivalent to knows_Spy_Outpts_insecureM*) |
|
271 |
||
272 |
||
273 |
||
274 |
||
275 |
lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)" |
|
276 |
by (simp add: subset_insertI) |
|
277 |
||
278 |
lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)" |
|
279 |
by (simp add: subset_insertI) |
|
280 |
||
281 |
lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)" |
|
282 |
by (simp add: subset_insertI) |
|
283 |
||
284 |
lemma knows_subset_knows_Inputs: "knows A evs \<subseteq> knows A (Inputs A' C X # evs)" |
|
285 |
by (simp add: subset_insertI) |
|
286 |
||
287 |
lemma knows_subset_knows_C_Gets: "knows A evs \<subseteq> knows A (C_Gets C X # evs)" |
|
288 |
by (simp add: subset_insertI) |
|
289 |
||
290 |
lemma knows_subset_knows_Outpts: "knows A evs \<subseteq> knows A (Outpts C A' X # evs)" |
|
291 |
by (simp add: subset_insertI) |
|
292 |
||
26302
68b073052e8c
proper naming of knows_Outpts_insecureM, knows_subset_knows_A_Gets;
wenzelm
parents:
21404
diff
changeset
|
293 |
lemma knows_subset_knows_A_Gets: "knows A evs \<subseteq> knows A (A_Gets A' X # evs)" |
18886 | 294 |
by (simp add: subset_insertI) |
295 |
||
296 |
||
297 |
text{*Agents know what they say*} |
|
298 |
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
|
299 |
apply (induct_tac "evs") |
|
300 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
301 |
apply blast |
|
302 |
done |
|
303 |
||
304 |
text{*Agents know what they note*} |
|
305 |
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
|
306 |
apply (induct_tac "evs") |
|
307 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
308 |
apply blast |
|
309 |
done |
|
310 |
||
311 |
text{*Agents know what they receive*} |
|
312 |
lemma Gets_imp_knows_agents [rule_format]: |
|
313 |
"A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
|
314 |
apply (induct_tac "evs") |
|
315 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
316 |
done |
|
317 |
||
318 |
(*Agents know what they input to their smart card*) |
|
319 |
lemma Inputs_imp_knows_agents [rule_format (no_asm)]: |
|
320 |
"Inputs A (Card A) X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
|
321 |
apply (induct_tac "evs") |
|
322 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
323 |
apply blast |
|
324 |
done |
|
325 |
||
326 |
(*Nothing to prove about C_Gets*) |
|
327 |
||
328 |
(*Agents know what they obtain as output of their smart card, |
|
329 |
if the means is secure...*) |
|
330 |
lemma Outpts_imp_knows_agents_secureM [rule_format (no_asm)]: |
|
331 |
"secureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
|
332 |
apply (induct_tac "evs") |
|
333 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
334 |
done |
|
335 |
||
336 |
(*otherwise only the spy knows the outputs*) |
|
337 |
lemma Outpts_imp_knows_agents_insecureM [rule_format (no_asm)]: |
|
338 |
"insecureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows Spy evs" |
|
339 |
apply (induct_tac "evs") |
|
340 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
341 |
done |
|
342 |
||
343 |
(*end lemmas about agents' knowledge*) |
|
344 |
||
345 |
||
346 |
||
347 |
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs" |
|
348 |
apply (induct_tac "evs", force) |
|
349 |
apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) |
|
350 |
done |
|
351 |
||
352 |
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] |
|
353 |
||
354 |
lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs" |
|
355 |
apply (induct_tac "evs") |
|
356 |
apply (simp_all add: parts_insert_knows_A split add: event.split, blast) |
|
357 |
done |
|
358 |
||
359 |
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs" |
|
360 |
by simp |
|
361 |
||
362 |
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs" |
|
363 |
by simp |
|
364 |
||
365 |
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" |
|
366 |
by simp |
|
367 |
||
368 |
lemma used_Inputs [simp]: "used (Inputs A C X # evs) = parts{X} \<union> used evs" |
|
369 |
by simp |
|
370 |
||
371 |
lemma used_C_Gets [simp]: "used (C_Gets C X # evs) = used evs" |
|
372 |
by simp |
|
373 |
||
374 |
lemma used_Outpts [simp]: "used (Outpts C A X # evs) = parts{X} \<union> used evs" |
|
375 |
by simp |
|
376 |
||
377 |
lemma used_A_Gets [simp]: "used (A_Gets A X # evs) = used evs" |
|
378 |
by simp |
|
379 |
||
380 |
lemma used_nil_subset: "used [] \<subseteq> used evs" |
|
381 |
apply simp |
|
382 |
apply (blast intro: initState_into_used) |
|
383 |
done |
|
384 |
||
385 |
||
386 |
||
387 |
(*Novel lemmas*) |
|
388 |
lemma Says_parts_used [rule_format (no_asm)]: |
|
389 |
"Says A B X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs" |
|
390 |
apply (induct_tac "evs") |
|
391 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
392 |
apply blast |
|
393 |
done |
|
394 |
||
395 |
lemma Notes_parts_used [rule_format (no_asm)]: |
|
396 |
"Notes A X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs" |
|
397 |
apply (induct_tac "evs") |
|
398 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
399 |
apply blast |
|
400 |
done |
|
401 |
||
402 |
lemma Outpts_parts_used [rule_format (no_asm)]: |
|
403 |
"Outpts C A X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs" |
|
404 |
apply (induct_tac "evs") |
|
405 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
406 |
apply blast |
|
407 |
done |
|
408 |
||
409 |
lemma Inputs_parts_used [rule_format (no_asm)]: |
|
410 |
"Inputs A C X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs" |
|
411 |
apply (induct_tac "evs") |
|
412 |
apply (simp_all (no_asm_simp) split add: event.split) |
|
413 |
apply blast |
|
414 |
done |
|
415 |
||
416 |
||
417 |
||
418 |
||
419 |
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} |
|
420 |
declare knows_Cons [simp del] |
|
421 |
used_Nil [simp del] used_Cons [simp del] |
|
422 |
||
423 |
||
424 |
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)" |
|
425 |
by (induct e, auto simp: knows_Cons) |
|
426 |
||
427 |
lemma initState_subset_knows: "initState A \<subseteq> knows A evs" |
|
428 |
apply (induct_tac evs, simp) |
|
429 |
apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) |
|
430 |
done |
|
431 |
||
432 |
||
433 |
text{*For proving @{text new_keys_not_used}*} |
|
434 |
lemma keysFor_parts_insert: |
|
435 |
"\<lbrakk> K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) \<rbrakk> |
|
436 |
\<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H"; |
|
437 |
by (force |
|
438 |
dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] |
|
439 |
analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
|
440 |
intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) |
|
441 |
||
442 |
end |