author | chaieb |
Mon, 11 Jun 2007 11:06:00 +0200 | |
changeset 23314 | 6894137e854a |
parent 21588 | cd0dc678a205 |
child 24122 | fc7f857d33c8 |
permissions | -rw-r--r-- |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Auth/Event |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
4 |
Copyright 1996 University of Cambridge |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
5 |
|
3683 | 6 |
Datatype of events; function "spies"; freshness |
3678 | 7 |
|
3683 | 8 |
"bad" agents have been broken by the Spy; their private keys and internal |
3678 | 9 |
stores are visible to him |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
10 |
*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
11 |
|
13956 | 12 |
header{*Theory of Events for Security Protocols*} |
13 |
||
16417 | 14 |
theory Event imports Message begin |
11104 | 15 |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
16 |
consts (*Initial states of agents -- parameter of the construction*) |
11104 | 17 |
initState :: "agent => msg set" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
18 |
|
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
19 |
datatype |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
20 |
event = Says agent agent msg |
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
21 |
| Gets agent msg |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
22 |
| Notes agent msg |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
23 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
24 |
consts |
11104 | 25 |
bad :: "agent set" (*compromised agents*) |
26 |
knows :: "agent => event list => msg set" |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
27 |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
28 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
29 |
text{*The constant "spies" is retained for compatibility's sake*} |
20768 | 30 |
|
31 |
abbreviation (input) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
32 |
spies :: "event list => msg set" where |
20768 | 33 |
"spies == knows Spy" |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
34 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
35 |
text{*Spy has access to his own key for spoof messages, but Server is secure*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
36 |
specification (bad) |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
37 |
Spy_in_bad [iff]: "Spy \<in> bad" |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
38 |
Server_not_bad [iff]: "Server \<notin> bad" |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
39 |
by (rule exI [of _ "{Spy}"], simp) |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
40 |
|
5183 | 41 |
primrec |
11104 | 42 |
knows_Nil: "knows A [] = initState A" |
43 |
knows_Cons: |
|
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
44 |
"knows A (ev # evs) = |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
45 |
(if A = Spy then |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
46 |
(case ev of |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
47 |
Says A' B X => insert X (knows Spy evs) |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
48 |
| Gets A' X => knows Spy evs |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
49 |
| Notes A' X => |
13922 | 50 |
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) |
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
51 |
else |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
52 |
(case ev of |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
53 |
Says A' B X => |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
54 |
if A'=A then insert X (knows A evs) else knows A evs |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
55 |
| Gets A' X => |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
56 |
if A'=A then insert X (knows A evs) else knows A evs |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
57 |
| Notes A' X => |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
58 |
if A'=A then insert X (knows A evs) else knows A evs))" |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
59 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
60 |
(* |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
61 |
Case A=Spy on the Gets event |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
62 |
enforces the fact that if a message is received then it must have been sent, |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
63 |
therefore the oops case must use Notes |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
64 |
*) |
3678 | 65 |
|
3683 | 66 |
consts |
67 |
(*Set of items that might be visible to somebody: |
|
68 |
complement of the set of fresh items*) |
|
11104 | 69 |
used :: "event list => msg set" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
70 |
|
5183 | 71 |
primrec |
11104 | 72 |
used_Nil: "used [] = (UN B. parts (initState B))" |
73 |
used_Cons: "used (ev # evs) = |
|
74 |
(case ev of |
|
13935 | 75 |
Says A B X => parts {X} \<union> used evs |
11104 | 76 |
| Gets A X => used evs |
13935 | 77 |
| Notes A X => parts {X} \<union> used evs)" |
78 |
--{*The case for @{term Gets} seems anomalous, but @{term Gets} always |
|
79 |
follows @{term Says} in real protocols. Seems difficult to change. |
|
80 |
See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *} |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
81 |
|
13926 | 82 |
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs" |
83 |
apply (induct_tac evs) |
|
11463 | 84 |
apply (auto split: event.split) |
85 |
done |
|
86 |
||
13926 | 87 |
lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs" |
88 |
apply (induct_tac evs) |
|
11463 | 89 |
apply (auto split: event.split) |
90 |
done |
|
91 |
||
13926 | 92 |
|
93 |
subsection{*Function @{term knows}*} |
|
94 |
||
13956 | 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.*) |
|
13935 | 98 |
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard] |
13926 | 99 |
|
100 |
lemma knows_Spy_Says [simp]: |
|
101 |
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)" |
|
102 |
by simp |
|
103 |
||
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
104 |
text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
105 |
on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*} |
13926 | 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: |
|
13935 | 115 |
"knows Spy evs \<subseteq> knows Spy (Says A B X # evs)" |
13926 | 116 |
by (simp add: subset_insertI) |
117 |
||
118 |
lemma knows_Spy_subset_knows_Spy_Notes: |
|
13935 | 119 |
"knows Spy evs \<subseteq> knows Spy (Notes A X # evs)" |
13926 | 120 |
by force |
121 |
||
122 |
lemma knows_Spy_subset_knows_Spy_Gets: |
|
13935 | 123 |
"knows Spy evs \<subseteq> knows Spy (Gets A X # evs)" |
13926 | 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 |
||
18570 | 146 |
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj] |
147 |
||
13926 | 148 |
text{*Compatibility for the old "spies" function*} |
149 |
lemmas spies_partsEs = knows_Spy_partsEs |
|
150 |
lemmas Says_imp_spies = Says_imp_knows_Spy |
|
13935 | 151 |
lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy] |
13926 | 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 |
||
13935 | 167 |
lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)" |
168 |
by (simp add: subset_insertI) |
|
13926 | 169 |
|
13935 | 170 |
lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)" |
171 |
by (simp add: subset_insertI) |
|
13926 | 172 |
|
13935 | 173 |
lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)" |
174 |
by (simp add: subset_insertI) |
|
13926 | 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 |
||
13935 | 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) |
|
13926 | 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") |
|
13935 | 229 |
apply (simp_all add: parts_insert_knows_A split add: event.split, blast) |
13926 | 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 |
||
13935 | 241 |
lemma used_nil_subset: "used [] \<subseteq> used evs" |
242 |
apply simp |
|
13926 | 243 |
apply (blast intro: initState_into_used) |
244 |
done |
|
245 |
||
246 |
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} |
|
13935 | 247 |
declare knows_Cons [simp del] |
248 |
used_Nil [simp del] used_Cons [simp del] |
|
13926 | 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 |
||
11104 | 273 |
|
13922 | 274 |
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)" |
275 |
by (induct e, auto simp: knows_Cons) |
|
276 |
||
13935 | 277 |
lemma initState_subset_knows: "initState A \<subseteq> knows A evs" |
13926 | 278 |
apply (induct_tac evs, simp) |
13922 | 279 |
apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) |
280 |
done |
|
281 |
||
282 |
||
13926 | 283 |
text{*For proving @{text new_keys_not_used}*} |
13922 | 284 |
lemma keysFor_parts_insert: |
13926 | 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"; |
|
13922 | 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]) |
|
291 |
||
11104 | 292 |
method_setup analz_mono_contra = {* |
21588 | 293 |
Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} |
13922 | 294 |
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P" |
295 |
||
296 |
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} |
|
297 |
||
298 |
ML |
|
299 |
{* |
|
13926 | 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 |
||
13922 | 329 |
val synth_analz_mono = thm "synth_analz_mono"; |
330 |
||
13935 | 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 |
||
13922 | 336 |
val synth_analz_mono_contra_tac = |
13926 | 337 |
let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI |
13922 | 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 = {* |
|
21588 | 351 |
Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} |
13922 | 352 |
"for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
353 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
354 |
end |