50 lemma Nonce_apm [rule_format]: "Nonce n \<in> parts {apm s X} \<Longrightarrow> |
50 lemma Nonce_apm [rule_format]: "Nonce n \<in> parts {apm s X} \<Longrightarrow> |
51 (\<forall>k. Number k \<in> parts {X} \<longrightarrow> Nonce n \<notin> parts {nb s k}) \<longrightarrow> |
51 (\<forall>k. Number k \<in> parts {X} \<longrightarrow> Nonce n \<notin> parts {nb s k}) \<longrightarrow> |
52 (\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)" |
52 (\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)" |
53 by (induct X, simp_all, blast) |
53 by (induct X, simp_all, blast) |
54 |
54 |
55 lemma wdef_Nonce: "[| Nonce n \<in> parts {apm s X}; R \<in> p; msg' R = X; wdef p; |
55 lemma wdef_Nonce: "\<lbrakk>Nonce n \<in> parts {apm s X}; R \<in> p; msg' R = X; wdef p; |
56 Nonce n \<notin> parts (apm s `(msg `(fst R))) |] ==> |
56 Nonce n \<notin> parts (apm s `(msg `(fst R)))\<rbrakk> \<Longrightarrow> |
57 (\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)" |
57 (\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)" |
58 apply (erule Nonce_apm, unfold wdef_def) |
58 apply (erule Nonce_apm, unfold wdef_def) |
59 apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp) |
59 apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp) |
60 apply (drule_tac x=x in bspec, simp) |
60 apply (drule_tac x=x in bspec, simp) |
61 apply (drule_tac Y="msg x" and s=s in apm_parts, simp) |
61 apply (drule_tac Y="msg x" and s=s in apm_parts, simp) |
101 for p :: proto |
101 for p :: proto |
102 where |
102 where |
103 |
103 |
104 Nil [intro]: "[] \<in> tr p" |
104 Nil [intro]: "[] \<in> tr p" |
105 |
105 |
106 | Fake [intro]: "[| evsf \<in> tr p; X \<in> synth (analz (spies evsf)) |] |
106 | Fake [intro]: "\<lbrakk>evsf \<in> tr p; X \<in> synth (analz (spies evsf))\<rbrakk> |
107 ==> Says Spy B X # evsf \<in> tr p" |
107 \<Longrightarrow> Says Spy B X # evsf \<in> tr p" |
108 |
108 |
109 | Proto [intro]: "[| evs \<in> tr p; R \<in> p; ok evs R s |] ==> ap' s R # evs \<in> tr p" |
109 | Proto [intro]: "\<lbrakk>evs \<in> tr p; R \<in> p; ok evs R s\<rbrakk> \<Longrightarrow> ap' s R # evs \<in> tr p" |
110 |
110 |
111 subsection\<open>general properties\<close> |
111 subsection\<open>general properties\<close> |
112 |
112 |
113 lemma one_step_tr [iff]: "one_step (tr p)" |
113 lemma one_step_tr [iff]: "one_step (tr p)" |
114 apply (unfold one_step_def, clarify) |
114 apply (unfold one_step_def, clarify) |
115 by (ind_cases "ev # evs \<in> tr p" for ev evs, auto) |
115 by (ind_cases "ev # evs \<in> tr p" for ev evs, auto) |
116 |
116 |
117 definition has_only_Says' :: "proto => bool" where |
117 definition has_only_Says' :: "proto => bool" where |
118 "has_only_Says' p \<equiv> \<forall>R. R \<in> p \<longrightarrow> is_Says (snd R)" |
118 "has_only_Says' p \<equiv> \<forall>R. R \<in> p \<longrightarrow> is_Says (snd R)" |
119 |
119 |
120 lemma has_only_Says'D: "[| R \<in> p; has_only_Says' p |] |
120 lemma has_only_Says'D: "\<lbrakk>R \<in> p; has_only_Says' p\<rbrakk> |
121 ==> (\<exists>A B X. snd R = Says A B X)" |
121 \<Longrightarrow> (\<exists>A B X. snd R = Says A B X)" |
122 by (unfold has_only_Says'_def is_Says_def, blast) |
122 by (unfold has_only_Says'_def is_Says_def, blast) |
123 |
123 |
124 lemma has_only_Says_tr [simp]: "has_only_Says' p ==> has_only_Says (tr p)" |
124 lemma has_only_Says_tr [simp]: "has_only_Says' p \<Longrightarrow> has_only_Says (tr p)" |
125 apply (unfold has_only_Says_def) |
125 apply (unfold has_only_Says_def) |
126 apply (rule allI, rule allI, rule impI) |
126 apply (rule allI, rule allI, rule impI) |
127 apply (erule tr.induct) |
127 apply (erule tr.induct) |
128 apply (auto simp: has_only_Says'_def ok_def) |
128 apply (auto simp: has_only_Says'_def ok_def) |
129 by (drule_tac x=a in spec, auto simp: is_Says_def) |
129 by (drule_tac x=a in spec, auto simp: is_Says_def) |
130 |
130 |
131 lemma has_only_Says'_in_trD: "[| has_only_Says' p; list @ ev # evs1 \<in> tr p |] |
131 lemma has_only_Says'_in_trD: "\<lbrakk>has_only_Says' p; list @ ev # evs1 \<in> tr p\<rbrakk> |
132 ==> (\<exists>A B X. ev = Says A B X)" |
132 \<Longrightarrow> (\<exists>A B X. ev = Says A B X)" |
133 by (drule has_only_Says_tr, auto) |
133 by (drule has_only_Says_tr, auto) |
134 |
134 |
135 lemma ok_not_used: "[| Nonce n \<notin> used evs; ok evs R s; |
135 lemma ok_not_used: "\<lbrakk>Nonce n \<notin> used evs; ok evs R s; |
136 \<forall>x. x \<in> fst R \<longrightarrow> is_Says x |] ==> Nonce n \<notin> parts (apm s `(msg `(fst R)))" |
136 \<forall>x. x \<in> fst R \<longrightarrow> is_Says x\<rbrakk> \<Longrightarrow> Nonce n \<notin> parts (apm s `(msg `(fst R)))" |
137 apply (unfold ok_def, clarsimp) |
137 apply (unfold ok_def, clarsimp) |
138 apply (drule_tac x=x in spec, drule_tac x=x in spec) |
138 apply (drule_tac x=x in spec, drule_tac x=x in spec) |
139 by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts) |
139 by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts) |
140 |
140 |
141 lemma ok_is_Says: "[| evs' @ ev # evs \<in> tr p; ok evs R s; has_only_Says' p; |
141 lemma ok_is_Says: "\<lbrakk>evs' @ ev # evs \<in> tr p; ok evs R s; has_only_Says' p; |
142 R \<in> p; x \<in> fst R |] ==> is_Says x" |
142 R \<in> p; x \<in> fst R\<rbrakk> \<Longrightarrow> is_Says x" |
143 apply (unfold ok_def is_Says_def, clarify) |
143 apply (unfold ok_def is_Says_def, clarify) |
144 apply (drule_tac x=x in spec, simp) |
144 apply (drule_tac x=x in spec, simp) |
145 apply (subgoal_tac "one_step (tr p)") |
145 apply (subgoal_tac "one_step (tr p)") |
146 apply (drule trunc, simp, drule one_step_Cons, simp) |
146 apply (drule trunc, simp, drule one_step_Cons, simp) |
147 apply (drule has_only_SaysD, simp+) |
147 apply (drule has_only_SaysD, simp+) |
164 lemma freshD: "fresh p R s n Ks evs \<Longrightarrow> (\<exists>evs1 evs2. |
164 lemma freshD: "fresh p R s n Ks evs \<Longrightarrow> (\<exists>evs1 evs2. |
165 evs = evs2 @ ap' s R # evs1 \<and> Nonce n \<notin> used evs1 \<and> R \<in> p \<and> ok evs1 R s |
165 evs = evs2 @ ap' s R # evs1 \<and> Nonce n \<notin> used evs1 \<and> R \<in> p \<and> ok evs1 R s |
166 \<and> Nonce n \<in> parts {apm' s R} \<and> apm' s R \<in> guard n Ks)" |
166 \<and> Nonce n \<in> parts {apm' s R} \<and> apm' s R \<in> guard n Ks)" |
167 by (unfold fresh_def, blast) |
167 by (unfold fresh_def, blast) |
168 |
168 |
169 lemma freshI [intro]: "[| Nonce n \<notin> used evs1; R \<in> p; Nonce n \<in> parts {apm' s R}; |
169 lemma freshI [intro]: "\<lbrakk>Nonce n \<notin> used evs1; R \<in> p; Nonce n \<in> parts {apm' s R}; |
170 ok evs1 R s; apm' s R \<in> guard n Ks |] |
170 ok evs1 R s; apm' s R \<in> guard n Ks\<rbrakk> |
171 ==> fresh p R s n Ks (list @ ap' s R # evs1)" |
171 \<Longrightarrow> fresh p R s n Ks (list @ ap' s R # evs1)" |
172 by (unfold fresh_def, blast) |
172 by (unfold fresh_def, blast) |
173 |
173 |
174 lemma freshI': "[| Nonce n \<notin> used evs1; (l,r) \<in> p; |
174 lemma freshI': "\<lbrakk>Nonce n \<notin> used evs1; (l,r) \<in> p; |
175 Nonce n \<in> parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r) \<in> guard n Ks |] |
175 Nonce n \<in> parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r) \<in> guard n Ks\<rbrakk> |
176 ==> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)" |
176 \<Longrightarrow> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)" |
177 by (drule freshI, simp+) |
177 by (drule freshI, simp+) |
178 |
178 |
179 lemma fresh_used: "[| fresh p R' s' n Ks evs; has_only_Says' p |] |
179 lemma fresh_used: "\<lbrakk>fresh p R' s' n Ks evs; has_only_Says' p\<rbrakk> |
180 ==> Nonce n \<in> used evs" |
180 \<Longrightarrow> Nonce n \<in> used evs" |
181 apply (unfold fresh_def, clarify) |
181 apply (unfold fresh_def, clarify) |
182 apply (drule has_only_Says'D) |
182 apply (drule has_only_Says'D) |
183 by (auto intro: parts_used_app) |
183 by (auto intro: parts_used_app) |
184 |
184 |
185 lemma fresh_newn: "[| evs' @ ap' s R # evs \<in> tr p; wdef p; has_only_Says' p; |
185 lemma fresh_newn: "\<lbrakk>evs' @ ap' s R # evs \<in> tr p; wdef p; has_only_Says' p; |
186 Nonce n \<notin> used evs; R \<in> p; ok evs R s; Nonce n \<in> parts {apm' s R} |] |
186 Nonce n \<notin> used evs; R \<in> p; ok evs R s; Nonce n \<in> parts {apm' s R}\<rbrakk> |
187 ==> \<exists>k. k \<in> newn R \<and> nonce s k = n" |
187 \<Longrightarrow> \<exists>k. k \<in> newn R \<and> nonce s k = n" |
188 apply (drule wdef_Nonce, simp+) |
188 apply (drule wdef_Nonce, simp+) |
189 apply (frule ok_not_used, simp+) |
189 apply (frule ok_not_used, simp+) |
190 apply (clarify, erule ok_is_Says, simp+) |
190 apply (clarify, erule ok_is_Says, simp+) |
191 apply (clarify, rule_tac x=k in exI, simp add: newn_def) |
191 apply (clarify, rule_tac x=k in exI, simp add: newn_def) |
192 apply (clarify, drule_tac Y="msg x" and s=s in apm_parts) |
192 apply (clarify, drule_tac Y="msg x" and s=s in apm_parts) |
193 apply (drule ok_not_used, simp+) |
193 apply (drule ok_not_used, simp+) |
194 by (clarify, erule ok_is_Says, simp_all) |
194 by (clarify, erule ok_is_Says, simp_all) |
195 |
195 |
196 lemma fresh_rule: "[| evs' @ ev # evs \<in> tr p; wdef p; Nonce n \<notin> used evs; |
196 lemma fresh_rule: "\<lbrakk>evs' @ ev # evs \<in> tr p; wdef p; Nonce n \<notin> used evs; |
197 Nonce n \<in> parts {msg ev} |] ==> \<exists>R s. R \<in> p \<and> ap' s R = ev" |
197 Nonce n \<in> parts {msg ev}\<rbrakk> \<Longrightarrow> \<exists>R s. R \<in> p \<and> ap' s R = ev" |
198 apply (drule trunc, simp, ind_cases "ev # evs \<in> tr p", simp) |
198 apply (drule trunc, simp, ind_cases "ev # evs \<in> tr p", simp) |
199 by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+) |
199 by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+) |
200 |
200 |
201 lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs \<subseteq> Ks; wdef p; |
201 lemma fresh_ruleD: "\<lbrakk>fresh p R' s' n Ks evs; keys R' s' n evs \<subseteq> Ks; wdef p; |
202 has_only_Says' p; evs \<in> tr p; \<forall>R k s. nonce s k = n \<longrightarrow> Nonce n \<in> used evs \<longrightarrow> |
202 has_only_Says' p; evs \<in> tr p; \<forall>R k s. nonce s k = n \<longrightarrow> Nonce n \<in> used evs \<longrightarrow> |
203 R \<in> p \<longrightarrow> k \<in> newn R \<longrightarrow> Nonce n \<in> parts {apm' s R} \<longrightarrow> apm' s R \<in> guard n Ks \<longrightarrow> |
203 R \<in> p \<longrightarrow> k \<in> newn R \<longrightarrow> Nonce n \<in> parts {apm' s R} \<longrightarrow> apm' s R \<in> guard n Ks \<longrightarrow> |
204 apm' s R \<in> parts (spies evs) \<longrightarrow> keys R s n evs \<subseteq> Ks \<longrightarrow> P |] ==> P" |
204 apm' s R \<in> parts (spies evs) \<longrightarrow> keys R s n evs \<subseteq> Ks \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
205 apply (frule fresh_used, simp) |
205 apply (frule fresh_used, simp) |
206 apply (unfold fresh_def, clarify) |
206 apply (unfold fresh_def, clarify) |
207 apply (drule_tac x=R' in spec) |
207 apply (drule_tac x=R' in spec) |
208 apply (drule fresh_newn, simp+, clarify) |
208 apply (drule fresh_newn, simp+, clarify) |
209 apply (drule_tac x=k in spec) |
209 apply (drule_tac x=k in spec) |
217 subsection\<open>safe keys\<close> |
217 subsection\<open>safe keys\<close> |
218 |
218 |
219 definition safe :: "key set \<Rightarrow> msg set \<Rightarrow> bool" where |
219 definition safe :: "key set \<Rightarrow> msg set \<Rightarrow> bool" where |
220 "safe Ks G \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G" |
220 "safe Ks G \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G" |
221 |
221 |
222 lemma safeD [dest]: "[| safe Ks G; K \<in> Ks |] ==> Key K \<notin> analz G" |
222 lemma safeD [dest]: "\<lbrakk>safe Ks G; K \<in> Ks\<rbrakk> \<Longrightarrow> Key K \<notin> analz G" |
223 by (unfold safe_def, blast) |
223 by (unfold safe_def, blast) |
224 |
224 |
225 lemma safe_insert: "safe Ks (insert X G) ==> safe Ks G" |
225 lemma safe_insert: "safe Ks (insert X G) \<Longrightarrow> safe Ks G" |
226 by (unfold safe_def, blast) |
226 by (unfold safe_def, blast) |
227 |
227 |
228 lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n \<notin> analz G" |
228 lemma Guard_safe: "\<lbrakk>Guard n Ks G; safe Ks G\<rbrakk> \<Longrightarrow> Nonce n \<notin> analz G" |
229 by (blast dest: Guard_invKey) |
229 by (blast dest: Guard_invKey) |
230 |
230 |
231 subsection\<open>guardedness preservation\<close> |
231 subsection\<open>guardedness preservation\<close> |
232 |
232 |
233 definition preserv :: "proto \<Rightarrow> keyfun \<Rightarrow> nat \<Rightarrow> key set \<Rightarrow> bool" where |
233 definition preserv :: "proto \<Rightarrow> keyfun \<Rightarrow> nat \<Rightarrow> key set \<Rightarrow> bool" where |
234 "preserv p keys n Ks \<equiv> (\<forall>evs R' s' R s. evs \<in> tr p \<longrightarrow> |
234 "preserv p keys n Ks \<equiv> (\<forall>evs R' s' R s. evs \<in> tr p \<longrightarrow> |
235 Guard n Ks (spies evs) \<longrightarrow> safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow> |
235 Guard n Ks (spies evs) \<longrightarrow> safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow> |
236 keys R' s' n evs \<subseteq> Ks \<longrightarrow> R \<in> p \<longrightarrow> ok evs R s \<longrightarrow> apm' s R \<in> guard n Ks)" |
236 keys R' s' n evs \<subseteq> Ks \<longrightarrow> R \<in> p \<longrightarrow> ok evs R s \<longrightarrow> apm' s R \<in> guard n Ks)" |
237 |
237 |
238 lemma preservD: "[| preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs); |
238 lemma preservD: "\<lbrakk>preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs); |
239 safe Ks (spies evs); fresh p R' s' n Ks evs; R \<in> p; ok evs R s; |
239 safe Ks (spies evs); fresh p R' s' n Ks evs; R \<in> p; ok evs R s; |
240 keys R' s' n evs \<subseteq> Ks |] ==> apm' s R \<in> guard n Ks" |
240 keys R' s' n evs \<subseteq> Ks\<rbrakk> \<Longrightarrow> apm' s R \<in> guard n Ks" |
241 by (unfold preserv_def, blast) |
241 by (unfold preserv_def, blast) |
242 |
242 |
243 lemma preservD': "[| preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs); |
243 lemma preservD': "\<lbrakk>preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs); |
244 safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X) \<in> p; |
244 safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X) \<in> p; |
245 ok evs (l,Says A B X) s; keys R' s' n evs \<subseteq> Ks |] ==> apm s X \<in> guard n Ks" |
245 ok evs (l,Says A B X) s; keys R' s' n evs \<subseteq> Ks\<rbrakk> \<Longrightarrow> apm s X \<in> guard n Ks" |
246 by (drule preservD, simp+) |
246 by (drule preservD, simp+) |
247 |
247 |
248 subsection\<open>monotonic keyfun\<close> |
248 subsection\<open>monotonic keyfun\<close> |
249 |
249 |
250 definition monoton :: "proto => keyfun => bool" where |
250 definition monoton :: "proto => keyfun => bool" where |
251 "monoton p keys \<equiv> \<forall>R' s' n ev evs. ev # evs \<in> tr p \<longrightarrow> |
251 "monoton p keys \<equiv> \<forall>R' s' n ev evs. ev # evs \<in> tr p \<longrightarrow> |
252 keys R' s' n evs \<subseteq> keys R' s' n (ev # evs)" |
252 keys R' s' n evs \<subseteq> keys R' s' n (ev # evs)" |
253 |
253 |
254 lemma monotonD [dest]: "[| keys R' s' n (ev # evs) \<subseteq> Ks; monoton p keys; |
254 lemma monotonD [dest]: "\<lbrakk>keys R' s' n (ev # evs) \<subseteq> Ks; monoton p keys; |
255 ev # evs \<in> tr p |] ==> keys R' s' n evs \<subseteq> Ks" |
255 ev # evs \<in> tr p\<rbrakk> \<Longrightarrow> keys R' s' n evs \<subseteq> Ks" |
256 by (unfold monoton_def, blast) |
256 by (unfold monoton_def, blast) |
257 |
257 |
258 subsection\<open>guardedness theorem\<close> |
258 subsection\<open>guardedness theorem\<close> |
259 |
259 |
260 lemma Guard_tr [rule_format]: "[| evs \<in> tr p; has_only_Says' p; |
260 lemma Guard_tr [rule_format]: "\<lbrakk>evs \<in> tr p; has_only_Says' p; |
261 preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy) |] ==> |
261 preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy)\<rbrakk> \<Longrightarrow> |
262 safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow> keys R' s' n evs \<subseteq> Ks \<longrightarrow> |
262 safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow> keys R' s' n evs \<subseteq> Ks \<longrightarrow> |
263 Guard n Ks (spies evs)" |
263 Guard n Ks (spies evs)" |
264 apply (erule tr.induct) |
264 apply (erule tr.induct) |
265 (* Nil *) |
265 (* Nil *) |
266 apply simp |
266 apply simp |
295 apply (blast dest: safe_insert) |
295 apply (blast dest: safe_insert) |
296 by (blast, simp, simp, blast) |
296 by (blast, simp, simp, blast) |
297 |
297 |
298 subsection\<open>useful properties for guardedness\<close> |
298 subsection\<open>useful properties for guardedness\<close> |
299 |
299 |
300 lemma newn_neq_used: "[| Nonce n \<in> used evs; ok evs R s; k \<in> newn R |] |
300 lemma newn_neq_used: "\<lbrakk>Nonce n \<in> used evs; ok evs R s; k \<in> newn R\<rbrakk> |
301 ==> n \<noteq> nonce s k" |
301 \<Longrightarrow> n \<noteq> nonce s k" |
302 by (auto simp: ok_def) |
302 by (auto simp: ok_def) |
303 |
303 |
304 lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x \<in> fst R; is_Says x |] |
304 lemma ok_Guard: "\<lbrakk>ok evs R s; Guard n Ks (spies evs); x \<in> fst R; is_Says x\<rbrakk> |
305 ==> apm s (msg x) \<in> parts (spies evs) \<and> apm s (msg x) \<in> guard n Ks" |
305 \<Longrightarrow> apm s (msg x) \<in> parts (spies evs) \<and> apm s (msg x) \<in> guard n Ks" |
306 apply (unfold ok_def is_Says_def, clarify) |
306 apply (unfold ok_def is_Says_def, clarify) |
307 apply (drule_tac x="Says A B X" in spec, simp) |
307 apply (drule_tac x="Says A B X" in spec, simp) |
308 by (drule Says_imp_spies, auto intro: parts_parts) |
308 by (drule Says_imp_spies, auto intro: parts_parts) |
309 |
309 |
310 lemma ok_parts_not_new: "[| Y \<in> parts (spies evs); Nonce (nonce s n) \<in> parts {Y}; |
310 lemma ok_parts_not_new: "\<lbrakk>Y \<in> parts (spies evs); Nonce (nonce s n) \<in> parts {Y}; |
311 ok evs R s |] ==> n \<notin> newn R" |
311 ok evs R s\<rbrakk> \<Longrightarrow> n \<notin> newn R" |
312 by (auto simp: ok_def dest: not_used_not_spied parts_parts) |
312 by (auto simp: ok_def dest: not_used_not_spied parts_parts) |
313 |
313 |
314 subsection\<open>unicity\<close> |
314 subsection\<open>unicity\<close> |
315 |
315 |
316 definition uniq :: "proto \<Rightarrow> secfun \<Rightarrow> bool" where |
316 definition uniq :: "proto \<Rightarrow> secfun \<Rightarrow> bool" where |
320 apm' s R \<in> guard (nonce s n) Ks \<longrightarrow> apm' s' R' \<in> guard (nonce s n) Ks \<longrightarrow> |
320 apm' s R \<in> guard (nonce s n) Ks \<longrightarrow> apm' s' R' \<in> guard (nonce s n) Ks \<longrightarrow> |
321 evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow> |
321 evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow> |
322 secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow> |
322 secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow> |
323 secret R n s Ks = secret R' n' s' Ks" |
323 secret R n s Ks = secret R' n' s' Ks" |
324 |
324 |
325 lemma uniqD: "[| uniq p secret; evs \<in> tr p; R \<in> p; R' \<in> p; n \<in> newn R; n' \<in> newn R'; |
325 lemma uniqD: "\<lbrakk>uniq p secret; evs \<in> tr p; R \<in> p; R' \<in> p; n \<in> newn R; n' \<in> newn R'; |
326 nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs); |
326 nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs); |
327 Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'}; |
327 Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'}; |
328 secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs); |
328 secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs); |
329 apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks |] ==> |
329 apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks\<rbrakk> \<Longrightarrow> |
330 secret R n s Ks = secret R' n' s' Ks" |
330 secret R n s Ks = secret R' n' s' Ks" |
331 by (unfold uniq_def, blast) |
331 by (unfold uniq_def, blast) |
332 |
332 |
333 definition ord :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> bool" where |
333 definition ord :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> bool" where |
334 "ord p inff \<equiv> \<forall>R R'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow> \<not> inff R R' \<longrightarrow> inff R' R" |
334 "ord p inff \<equiv> \<forall>R R'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow> \<not> inff R R' \<longrightarrow> inff R' R" |
335 |
335 |
336 lemma ordD: "[| ord p inff; \<not> inff R R'; R \<in> p; R' \<in> p |] ==> inff R' R" |
336 lemma ordD: "\<lbrakk>ord p inff; \<not> inff R R'; R \<in> p; R' \<in> p\<rbrakk> \<Longrightarrow> inff R' R" |
337 by (unfold ord_def, blast) |
337 by (unfold ord_def, blast) |
338 |
338 |
339 definition uniq' :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> secfun \<Rightarrow> bool" where |
339 definition uniq' :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> secfun \<Rightarrow> bool" where |
340 "uniq' p inff secret \<equiv> \<forall>evs R R' n n' Ks s s'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow> |
340 "uniq' p inff secret \<equiv> \<forall>evs R R' n n' Ks s s'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow> |
341 inff R R' \<longrightarrow> n \<in> newn R \<longrightarrow> n' \<in> newn R' \<longrightarrow> nonce s n = nonce s' n' \<longrightarrow> |
341 inff R R' \<longrightarrow> n \<in> newn R \<longrightarrow> n' \<in> newn R' \<longrightarrow> nonce s n = nonce s' n' \<longrightarrow> |
343 apm' s R \<in> guard (nonce s n) Ks \<longrightarrow> apm' s' R' \<in> guard (nonce s n) Ks \<longrightarrow> |
343 apm' s R \<in> guard (nonce s n) Ks \<longrightarrow> apm' s' R' \<in> guard (nonce s n) Ks \<longrightarrow> |
344 evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow> |
344 evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow> |
345 secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow> |
345 secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow> |
346 secret R n s Ks = secret R' n' s' Ks" |
346 secret R n s Ks = secret R' n' s' Ks" |
347 |
347 |
348 lemma uniq'D: "[| uniq' p inff secret; evs \<in> tr p; inff R R'; R \<in> p; R' \<in> p; n \<in> newn R; |
348 lemma uniq'D: "\<lbrakk>uniq' p inff secret; evs \<in> tr p; inff R R'; R \<in> p; R' \<in> p; n \<in> newn R; |
349 n' \<in> newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs); |
349 n' \<in> newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs); |
350 Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'}; |
350 Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'}; |
351 secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs); |
351 secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs); |
352 apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks |] ==> |
352 apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks\<rbrakk> \<Longrightarrow> |
353 secret R n s Ks = secret R' n' s' Ks" |
353 secret R n s Ks = secret R' n' s' Ks" |
354 by (unfold uniq'_def, blast) |
354 by (unfold uniq'_def, blast) |
355 |
355 |
356 lemma uniq'_imp_uniq: "[| uniq' p inff secret; ord p inff |] ==> uniq p secret" |
356 lemma uniq'_imp_uniq: "\<lbrakk>uniq' p inff secret; ord p inff\<rbrakk> \<Longrightarrow> uniq p secret" |
357 apply (unfold uniq_def) |
357 apply (unfold uniq_def) |
358 apply (rule allI)+ |
358 apply (rule allI)+ |
359 apply (case_tac "inff R R'") |
359 apply (case_tac "inff R R'") |
360 apply (blast dest: uniq'D) |
360 apply (blast dest: uniq'D) |
361 by (auto dest: ordD uniq'D intro: sym) |
361 by (auto dest: ordD uniq'D intro: sym) |