72 |
70 |
73 primrec |
71 primrec |
74 used_Nil: "used [] = (UN B. parts (initState B))" |
72 used_Nil: "used [] = (UN B. parts (initState B))" |
75 used_Cons: "used (ev # evs) = |
73 used_Cons: "used (ev # evs) = |
76 (case ev of |
74 (case ev of |
77 Says A B X => parts {X} Un (used evs) |
75 Says A B X => parts {X} \<union> used evs |
78 | Gets A X => used evs |
76 | Gets A X => used evs |
79 | Notes A X => parts {X} Un (used evs))" |
77 | Notes A X => parts {X} \<union> used evs)" |
80 |
78 --{*The case for @{term Gets} seems anomalous, but @{term Gets} always |
81 |
79 follows @{term Says} in real protocols. Seems difficult to change. |
82 use "Event_lemmas.ML" |
80 See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *} |
|
81 |
|
82 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs" |
|
83 apply (induct_tac evs) |
|
84 apply (auto split: event.split) |
|
85 done |
|
86 |
|
87 lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs" |
|
88 apply (induct_tac evs) |
|
89 apply (auto split: event.split) |
|
90 done |
|
91 |
|
92 |
|
93 subsection{*Function @{term knows}*} |
|
94 |
|
95 (*Simplifying |
|
96 parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs). |
|
97 This version won't loop with the simplifier.*) |
|
98 lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard] |
|
99 |
|
100 lemma knows_Spy_Says [simp]: |
|
101 "knows Spy (Says A B X # evs) = insert X (knows Spy evs)" |
|
102 by simp |
|
103 |
|
104 text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits |
|
105 on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*} |
|
106 lemma knows_Spy_Notes [simp]: |
|
107 "knows Spy (Notes A X # evs) = |
|
108 (if A:bad then insert X (knows Spy evs) else knows Spy evs)" |
|
109 by simp |
|
110 |
|
111 lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs" |
|
112 by simp |
|
113 |
|
114 lemma knows_Spy_subset_knows_Spy_Says: |
|
115 "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)" |
|
116 by (simp add: subset_insertI) |
|
117 |
|
118 lemma knows_Spy_subset_knows_Spy_Notes: |
|
119 "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)" |
|
120 by force |
|
121 |
|
122 lemma knows_Spy_subset_knows_Spy_Gets: |
|
123 "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)" |
|
124 by (simp add: subset_insertI) |
|
125 |
|
126 text{*Spy sees what is sent on the traffic*} |
|
127 lemma Says_imp_knows_Spy [rule_format]: |
|
128 "Says A B X \<in> set evs --> X \<in> knows Spy evs" |
|
129 apply (induct_tac "evs") |
|
130 apply (simp_all (no_asm_simp) split add: event.split) |
|
131 done |
|
132 |
|
133 lemma Notes_imp_knows_Spy [rule_format]: |
|
134 "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs" |
|
135 apply (induct_tac "evs") |
|
136 apply (simp_all (no_asm_simp) split add: event.split) |
|
137 done |
|
138 |
|
139 |
|
140 text{*Elimination rules: derive contradictions from old Says events containing |
|
141 items known to be fresh*} |
|
142 lemmas knows_Spy_partsEs = |
|
143 Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] |
|
144 parts.Body [THEN revcut_rl, standard] |
|
145 |
|
146 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj] |
|
147 |
|
148 text{*Compatibility for the old "spies" function*} |
|
149 lemmas spies_partsEs = knows_Spy_partsEs |
|
150 lemmas Says_imp_spies = Says_imp_knows_Spy |
|
151 lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy] |
|
152 |
|
153 |
|
154 subsection{*Knowledge of Agents*} |
|
155 |
|
156 lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)" |
|
157 by simp |
|
158 |
|
159 lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)" |
|
160 by simp |
|
161 |
|
162 lemma knows_Gets: |
|
163 "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)" |
|
164 by simp |
|
165 |
|
166 |
|
167 lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)" |
|
168 by (simp add: subset_insertI) |
|
169 |
|
170 lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)" |
|
171 by (simp add: subset_insertI) |
|
172 |
|
173 lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)" |
|
174 by (simp add: subset_insertI) |
|
175 |
|
176 text{*Agents know what they say*} |
|
177 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs" |
|
178 apply (induct_tac "evs") |
|
179 apply (simp_all (no_asm_simp) split add: event.split) |
|
180 apply blast |
|
181 done |
|
182 |
|
183 text{*Agents know what they note*} |
|
184 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs" |
|
185 apply (induct_tac "evs") |
|
186 apply (simp_all (no_asm_simp) split add: event.split) |
|
187 apply blast |
|
188 done |
|
189 |
|
190 text{*Agents know what they receive*} |
|
191 lemma Gets_imp_knows_agents [rule_format]: |
|
192 "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs" |
|
193 apply (induct_tac "evs") |
|
194 apply (simp_all (no_asm_simp) split add: event.split) |
|
195 done |
|
196 |
|
197 |
|
198 text{*What agents DIFFERENT FROM Spy know |
|
199 was either said, or noted, or got, or known initially*} |
|
200 lemma knows_imp_Says_Gets_Notes_initState [rule_format]: |
|
201 "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B. |
|
202 Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A" |
|
203 apply (erule rev_mp) |
|
204 apply (induct_tac "evs") |
|
205 apply (simp_all (no_asm_simp) split add: event.split) |
|
206 apply blast |
|
207 done |
|
208 |
|
209 text{*What the Spy knows -- for the time being -- |
|
210 was either said or noted, or known initially*} |
|
211 lemma knows_Spy_imp_Says_Notes_initState [rule_format]: |
|
212 "[| X \<in> knows Spy evs |] ==> EX A B. |
|
213 Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy" |
|
214 apply (erule rev_mp) |
|
215 apply (induct_tac "evs") |
|
216 apply (simp_all (no_asm_simp) split add: event.split) |
|
217 apply blast |
|
218 done |
|
219 |
|
220 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs" |
|
221 apply (induct_tac "evs", force) |
|
222 apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) |
|
223 done |
|
224 |
|
225 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] |
|
226 |
|
227 lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs" |
|
228 apply (induct_tac "evs") |
|
229 apply (simp_all add: parts_insert_knows_A split add: event.split, blast) |
|
230 done |
|
231 |
|
232 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs" |
|
233 by simp |
|
234 |
|
235 lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs" |
|
236 by simp |
|
237 |
|
238 lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" |
|
239 by simp |
|
240 |
|
241 lemma used_nil_subset: "used [] \<subseteq> used evs" |
|
242 apply simp |
|
243 apply (blast intro: initState_into_used) |
|
244 done |
|
245 |
|
246 text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} |
|
247 declare knows_Cons [simp del] |
|
248 used_Nil [simp del] used_Cons [simp del] |
|
249 |
|
250 |
|
251 text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"} |
|
252 New events added by induction to "evs" are discarded. Provided |
|
253 this information isn't needed, the proof will be much shorter, since |
|
254 it will omit complicated reasoning about @{term analz}.*} |
|
255 |
|
256 lemmas analz_mono_contra = |
|
257 knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] |
|
258 knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] |
|
259 knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] |
|
260 |
|
261 ML |
|
262 {* |
|
263 val analz_mono_contra_tac = |
|
264 let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI |
|
265 in |
|
266 rtac analz_impI THEN' |
|
267 REPEAT1 o |
|
268 (dresolve_tac (thms"analz_mono_contra")) |
|
269 THEN' mp_tac |
|
270 end |
|
271 *} |
|
272 |
|
273 |
|
274 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)" |
|
275 by (induct e, auto simp: knows_Cons) |
|
276 |
|
277 lemma initState_subset_knows: "initState A \<subseteq> knows A evs" |
|
278 apply (induct_tac evs, simp) |
|
279 apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) |
|
280 done |
|
281 |
|
282 |
|
283 text{*For proving @{text new_keys_not_used}*} |
|
284 lemma keysFor_parts_insert: |
|
285 "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] |
|
286 ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; |
|
287 by (force |
|
288 dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] |
|
289 analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
|
290 intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) |
83 |
291 |
84 method_setup analz_mono_contra = {* |
292 method_setup analz_mono_contra = {* |
85 Method.no_args |
293 Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} |
86 (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *} |
|
87 "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P" |
294 "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P" |
88 |
295 |
|
296 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} |
|
297 |
|
298 ML |
|
299 {* |
|
300 val knows_Cons = thm "knows_Cons" |
|
301 val used_Nil = thm "used_Nil" |
|
302 val used_Cons = thm "used_Cons" |
|
303 |
|
304 val Notes_imp_used = thm "Notes_imp_used"; |
|
305 val Says_imp_used = thm "Says_imp_used"; |
|
306 val Says_imp_knows_Spy = thm "Says_imp_knows_Spy"; |
|
307 val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy"; |
|
308 val knows_Spy_partsEs = thms "knows_Spy_partsEs"; |
|
309 val spies_partsEs = thms "spies_partsEs"; |
|
310 val Says_imp_spies = thm "Says_imp_spies"; |
|
311 val parts_insert_spies = thm "parts_insert_spies"; |
|
312 val Says_imp_knows = thm "Says_imp_knows"; |
|
313 val Notes_imp_knows = thm "Notes_imp_knows"; |
|
314 val Gets_imp_knows_agents = thm "Gets_imp_knows_agents"; |
|
315 val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState"; |
|
316 val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState"; |
|
317 val usedI = thm "usedI"; |
|
318 val initState_into_used = thm "initState_into_used"; |
|
319 val used_Says = thm "used_Says"; |
|
320 val used_Notes = thm "used_Notes"; |
|
321 val used_Gets = thm "used_Gets"; |
|
322 val used_nil_subset = thm "used_nil_subset"; |
|
323 val analz_mono_contra = thms "analz_mono_contra"; |
|
324 val knows_subset_knows_Cons = thm "knows_subset_knows_Cons"; |
|
325 val initState_subset_knows = thm "initState_subset_knows"; |
|
326 val keysFor_parts_insert = thm "keysFor_parts_insert"; |
|
327 |
|
328 |
|
329 val synth_analz_mono = thm "synth_analz_mono"; |
|
330 |
|
331 val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says"; |
|
332 val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes"; |
|
333 val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets"; |
|
334 |
|
335 |
|
336 val synth_analz_mono_contra_tac = |
|
337 let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI |
|
338 in |
|
339 rtac syan_impI THEN' |
|
340 REPEAT1 o |
|
341 (dresolve_tac |
|
342 [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD, |
|
343 knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD, |
|
344 knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD]) |
|
345 THEN' |
|
346 mp_tac |
|
347 end; |
|
348 *} |
|
349 |
|
350 method_setup synth_analz_mono_contra = {* |
|
351 Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} |
|
352 "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P" |
|
353 (*>*) |
|
354 |
|
355 section{* Event Traces \label{sec:events} *} |
|
356 |
|
357 text {* |
|
358 The system's behaviour is formalized as a set of traces of |
|
359 \emph{events}. The most important event, @{text "Says A B X"}, expresses |
|
360 $A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$. |
|
361 A trace is simply a list, constructed in reverse |
|
362 using~@{text "#"}. Other event types include reception of messages (when |
|
363 we want to make it explicit) and an agent's storing a fact. |
|
364 |
|
365 Sometimes the protocol requires an agent to generate a new nonce. The |
|
366 probability that a 20-byte random number has appeared before is effectively |
|
367 zero. To formalize this important property, the set @{term "used evs"} |
|
368 denotes the set of all items mentioned in the trace~@{text evs}. |
|
369 The function @{text used} has a straightforward |
|
370 recursive definition. Here is the case for @{text Says} event: |
|
371 @{thm [display,indent=5] used_Says [no_vars]} |
|
372 |
|
373 The function @{text knows} formalizes an agent's knowledge. Mostly we only |
|
374 care about the spy's knowledge, and @{term "knows Spy evs"} is the set of items |
|
375 available to the spy in the trace~@{text evs}. Already in the empty trace, |
|
376 the spy starts with some secrets at his disposal, such as the private keys |
|
377 of compromised users. After each @{text Says} event, the spy learns the |
|
378 message that was sent: |
|
379 @{thm [display,indent=5] knows_Spy_Says [no_vars]} |
|
380 Combinations of functions express other important |
|
381 sets of messages derived from~@{text evs}: |
|
382 \begin{itemize} |
|
383 \item @{term "analz (knows Spy evs)"} is everything that the spy could |
|
384 learn by decryption |
|
385 \item @{term "synth (analz (knows Spy evs))"} is everything that the spy |
|
386 could generate |
|
387 \end{itemize} |
|
388 *} |
|
389 |
|
390 (*<*) |
89 end |
391 end |
|
392 (*>*) |