24 |
24 |
25 |
25 |
26 text\<open>The constant "spies" is retained for compatibility's sake\<close> |
26 text\<open>The constant "spies" is retained for compatibility's sake\<close> |
27 |
27 |
28 primrec |
28 primrec |
29 knows :: "agent => event list => msg set" |
29 knows :: "agent \<Rightarrow> event list \<Rightarrow> msg set" |
30 where |
30 where |
31 knows_Nil: "knows A [] = initState A" |
31 knows_Nil: "knows A [] = initState A" |
32 | knows_Cons: |
32 | knows_Cons: |
33 "knows A (ev # evs) = |
33 "knows A (ev # evs) = |
34 (if A = Spy then |
34 (if A = Spy then |
35 (case ev of |
35 (case ev of |
36 Says A' B X => insert X (knows Spy evs) |
36 Says A' B X \<Rightarrow> insert X (knows Spy evs) |
37 | Gets A' X => knows Spy evs |
37 | Gets A' X \<Rightarrow> knows Spy evs |
38 | Notes A' X => |
38 | Notes A' X \<Rightarrow> |
39 if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) |
39 if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) |
40 else |
40 else |
41 (case ev of |
41 (case ev of |
42 Says A' B X => |
42 Says A' B X \<Rightarrow> |
43 if A'=A then insert X (knows A evs) else knows A evs |
43 if A'=A then insert X (knows A evs) else knows A evs |
44 | Gets A' X => |
44 | Gets A' X \<Rightarrow> |
45 if A'=A then insert X (knows A evs) else knows A evs |
45 if A'=A then insert X (knows A evs) else knows A evs |
46 | Notes A' X => |
46 | Notes A' X \<Rightarrow> |
47 if A'=A then insert X (knows A evs) else knows A evs))" |
47 if A'=A then insert X (knows A evs) else knows A evs))" |
48 |
48 |
49 abbreviation (input) |
49 abbreviation (input) |
50 spies :: "event list => msg set" where |
50 spies :: "event list \<Rightarrow> msg set" where |
51 "spies == knows Spy" |
51 "spies == knows Spy" |
52 |
52 |
53 text\<open>Spy has access to his own key for spoof messages, but Server is secure\<close> |
53 text\<open>Spy has access to his own key for spoof messages, but Server is secure\<close> |
54 specification (bad) |
54 specification (bad) |
55 Spy_in_bad [iff]: "Spy \<in> bad" |
55 Spy_in_bad [iff]: "Spy \<in> bad" |
63 *) |
63 *) |
64 |
64 |
65 primrec |
65 primrec |
66 (*Set of items that might be visible to somebody: |
66 (*Set of items that might be visible to somebody: |
67 complement of the set of fresh items*) |
67 complement of the set of fresh items*) |
68 used :: "event list => msg set" |
68 used :: "event list \<Rightarrow> msg set" |
69 where |
69 where |
70 used_Nil: "used [] = (UN B. parts (initState B))" |
70 used_Nil: "used [] = (UN B. parts (initState B))" |
71 | used_Cons: "used (ev # evs) = |
71 | used_Cons: "used (ev # evs) = |
72 (case ev of |
72 (case ev of |
73 Says A B X => parts {X} \<union> used evs |
73 Says A B X \<Rightarrow> parts {X} \<union> used evs |
74 | Gets A X => used evs |
74 | Gets A X \<Rightarrow> used evs |
75 | Notes A X => parts {X} \<union> used evs)" |
75 | Notes A X \<Rightarrow> parts {X} \<union> used evs)" |
76 \<comment> \<open>The case for @{term Gets} seems anomalous, but @{term Gets} always |
76 \<comment> \<open>The case for @{term Gets} seems anomalous, but @{term Gets} always |
77 follows @{term Says} in real protocols. Seems difficult to change. |
77 follows @{term Says} in real protocols. Seems difficult to change. |
78 See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}.\<close> |
78 See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}.\<close> |
79 |
79 |
80 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs" |
80 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs" |
81 apply (induct_tac evs) |
81 apply (induct_tac evs) |
82 apply (auto split: event.split) |
82 apply (auto split: event.split) |
83 done |
83 done |
84 |
84 |
85 lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs" |
85 lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> used evs" |
86 apply (induct_tac evs) |
86 apply (induct_tac evs) |
87 apply (auto split: event.split) |
87 apply (auto split: event.split) |
88 done |
88 done |
89 |
89 |
90 |
90 |
121 "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)" |
121 "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)" |
122 by (simp add: subset_insertI) |
122 by (simp add: subset_insertI) |
123 |
123 |
124 text\<open>Spy sees what is sent on the traffic\<close> |
124 text\<open>Spy sees what is sent on the traffic\<close> |
125 lemma Says_imp_knows_Spy [rule_format]: |
125 lemma Says_imp_knows_Spy [rule_format]: |
126 "Says A B X \<in> set evs --> X \<in> knows Spy evs" |
126 "Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs" |
127 apply (induct_tac "evs") |
127 apply (induct_tac "evs") |
128 apply (simp_all (no_asm_simp) split: event.split) |
128 apply (simp_all (no_asm_simp) split: event.split) |
129 done |
129 done |
130 |
130 |
131 lemma Notes_imp_knows_Spy [rule_format]: |
131 lemma Notes_imp_knows_Spy [rule_format]: |
132 "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs" |
132 "Notes A X \<in> set evs \<longrightarrow> A \<in> bad \<longrightarrow> X \<in> knows Spy evs" |
133 apply (induct_tac "evs") |
133 apply (induct_tac "evs") |
134 apply (simp_all (no_asm_simp) split: event.split) |
134 apply (simp_all (no_asm_simp) split: event.split) |
135 done |
135 done |
136 |
136 |
137 |
137 |
170 |
170 |
171 lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)" |
171 lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)" |
172 by (simp add: subset_insertI) |
172 by (simp add: subset_insertI) |
173 |
173 |
174 text\<open>Agents know what they say\<close> |
174 text\<open>Agents know what they say\<close> |
175 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs" |
175 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
176 apply (induct_tac "evs") |
176 apply (induct_tac "evs") |
177 apply (simp_all (no_asm_simp) split: event.split) |
177 apply (simp_all (no_asm_simp) split: event.split) |
178 apply blast |
178 apply blast |
179 done |
179 done |
180 |
180 |
181 text\<open>Agents know what they note\<close> |
181 text\<open>Agents know what they note\<close> |
182 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs" |
182 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
183 apply (induct_tac "evs") |
183 apply (induct_tac "evs") |
184 apply (simp_all (no_asm_simp) split: event.split) |
184 apply (simp_all (no_asm_simp) split: event.split) |
185 apply blast |
185 apply blast |
186 done |
186 done |
187 |
187 |
188 text\<open>Agents know what they receive\<close> |
188 text\<open>Agents know what they receive\<close> |
189 lemma Gets_imp_knows_agents [rule_format]: |
189 lemma Gets_imp_knows_agents [rule_format]: |
190 "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs" |
190 "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs" |
191 apply (induct_tac "evs") |
191 apply (induct_tac "evs") |
192 apply (simp_all (no_asm_simp) split: event.split) |
192 apply (simp_all (no_asm_simp) split: event.split) |
193 done |
193 done |
194 |
194 |
195 |
195 |
196 text\<open>What agents DIFFERENT FROM Spy know |
196 text\<open>What agents DIFFERENT FROM Spy know |
197 was either said, or noted, or got, or known initially\<close> |
197 was either said, or noted, or got, or known initially\<close> |
198 lemma knows_imp_Says_Gets_Notes_initState [rule_format]: |
198 lemma knows_imp_Says_Gets_Notes_initState [rule_format]: |
199 "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B. |
199 "[| X \<in> knows A evs; A \<noteq> Spy |] ==> \<exists>B. |
200 Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A" |
200 Says A B X \<in> set evs \<or> Gets A X \<in> set evs \<or> Notes A X \<in> set evs \<or> X \<in> initState A" |
201 apply (erule rev_mp) |
201 apply (erule rev_mp) |
202 apply (induct_tac "evs") |
202 apply (induct_tac "evs") |
203 apply (simp_all (no_asm_simp) split: event.split) |
203 apply (simp_all (no_asm_simp) split: event.split) |
204 apply blast |
204 apply blast |
205 done |
205 done |
206 |
206 |
207 text\<open>What the Spy knows -- for the time being -- |
207 text\<open>What the Spy knows -- for the time being -- |
208 was either said or noted, or known initially\<close> |
208 was either said or noted, or known initially\<close> |
209 lemma knows_Spy_imp_Says_Notes_initState [rule_format]: |
209 lemma knows_Spy_imp_Says_Notes_initState [rule_format]: |
210 "[| X \<in> knows Spy evs |] ==> EX A B. |
210 "[| X \<in> knows Spy evs |] ==> \<exists>A B. |
211 Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy" |
211 Says A B X \<in> set evs \<or> Notes A X \<in> set evs \<or> X \<in> initState Spy" |
212 apply (erule rev_mp) |
212 apply (erule rev_mp) |
213 apply (induct_tac "evs") |
213 apply (induct_tac "evs") |
214 apply (simp_all (no_asm_simp) split: event.split) |
214 apply (simp_all (no_asm_simp) split: event.split) |
215 apply blast |
215 apply blast |
216 done |
216 done |
220 apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) |
220 apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) |
221 done |
221 done |
222 |
222 |
223 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] |
223 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] |
224 |
224 |
225 lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs" |
225 lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs" |
226 apply (induct_tac "evs") |
226 apply (induct_tac "evs") |
227 apply (simp_all add: parts_insert_knows_A split: event.split, blast) |
227 apply (simp_all add: parts_insert_knows_A split: event.split, blast) |
228 done |
228 done |
229 |
229 |
230 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs" |
230 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs" |
244 text\<open>NOTE REMOVAL--laws above are cleaner, as they don't involve "case"\<close> |
244 text\<open>NOTE REMOVAL--laws above are cleaner, as they don't involve "case"\<close> |
245 declare knows_Cons [simp del] |
245 declare knows_Cons [simp del] |
246 used_Nil [simp del] used_Cons [simp del] |
246 used_Nil [simp del] used_Cons [simp del] |
247 |
247 |
248 |
248 |
249 text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"} |
249 text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) \<longrightarrow> P"} |
250 New events added by induction to "evs" are discarded. Provided |
250 New events added by induction to "evs" are discarded. Provided |
251 this information isn't needed, the proof will be much shorter, since |
251 this information isn't needed, the proof will be much shorter, since |
252 it will omit complicated reasoning about @{term analz}.\<close> |
252 it will omit complicated reasoning about @{term analz}.\<close> |
253 |
253 |
254 lemmas analz_mono_contra = |
254 lemmas analz_mono_contra = |
284 analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
284 analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
285 intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) |
285 intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) |
286 |
286 |
287 method_setup analz_mono_contra = \<open> |
287 method_setup analz_mono_contra = \<open> |
288 Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\<close> |
288 Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\<close> |
289 "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P" |
289 "for proving theorems of the form X \<notin> analz (knows Spy evs) \<longrightarrow> P" |
290 |
290 |
291 subsubsection\<open>Useful for case analysis on whether a hash is a spoof or not\<close> |
291 subsubsection\<open>Useful for case analysis on whether a hash is a spoof or not\<close> |
292 |
292 |
293 lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs |
293 lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs |
294 |
294 |