src/HOL/Auth/Guard/Proto.thy
changeset 76287 cdc14f94c754
parent 67613 ce654b0e6d69
child 76288 b82ac7ef65ec
equal deleted inserted replaced
76280:e381884c09d4 76287:cdc14f94c754
    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)
   439 lemma ns_wdef [iff]: "wdef ns"
   439 lemma ns_wdef [iff]: "wdef ns"
   440 by (auto simp: wdef_def elim: ns.cases)
   440 by (auto simp: wdef_def elim: ns.cases)
   441 
   441 
   442 subsection\<open>guardedness for NSL\<close>
   442 subsection\<open>guardedness for NSL\<close>
   443 
   443 
   444 lemma "uniq ns secret ==> preserv ns keys n Ks"
   444 lemma "uniq ns secret \<Longrightarrow> preserv ns keys n Ks"
   445 apply (unfold preserv_def)
   445 apply (unfold preserv_def)
   446 apply (rule allI)+
   446 apply (rule allI)+
   447 apply (rule impI, rule impI, rule impI, rule impI, rule impI)
   447 apply (rule impI, rule impI, rule impI, rule impI, rule impI)
   448 apply (erule fresh_ruleD, simp, simp, simp, simp)
   448 apply (erule fresh_ruleD, simp, simp, simp, simp)
   449 apply (rule allI)+
   449 apply (rule allI)+