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