--- a/src/HOL/Auth/Guard/Proto.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Thu Feb 15 12:11:00 2018 +0100
@@ -18,8 +18,8 @@
type_synonym proto = "rule set"
definition wdef :: "proto => bool" where
-"wdef p == ALL R k. R:p --> Number k:parts {msg' R}
---> Number k:parts (msg`(fst R))"
+"wdef p \<equiv> \<forall>R k. R \<in> p \<longrightarrow> Number k \<in> parts {msg' R}
+\<longrightarrow> Number k \<in> parts (msg`(fst R))"
subsection\<open>substitutions\<close>
@@ -36,89 +36,89 @@
| "apm s (Key K) = Key (key s K)"
| "apm s (Hash X) = Hash (apm s X)"
| "apm s (Crypt K X) = (
-if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
-else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
+if (\<exists>A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
+else if (\<exists>A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
else Crypt (key s K) (apm s X))"
| "apm s \<lbrace>X,Y\<rbrace> = \<lbrace>apm s X, apm s Y\<rbrace>"
-lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}"
+lemma apm_parts: "X \<in> parts {Y} \<Longrightarrow> apm s X \<in> parts {apm s Y}"
apply (erule parts.induct, simp_all, blast)
apply (erule parts.Fst)
apply (erule parts.Snd)
by (erule parts.Body)+
-lemma Nonce_apm [rule_format]: "Nonce n:parts {apm s X} ==>
-(ALL k. Number k:parts {X} --> Nonce n ~:parts {nb s k}) -->
-(EX k. Nonce k:parts {X} & nonce s k = n)"
+lemma Nonce_apm [rule_format]: "Nonce n \<in> parts {apm s X} \<Longrightarrow>
+(\<forall>k. Number k \<in> parts {X} \<longrightarrow> Nonce n \<notin> parts {nb s k}) \<longrightarrow>
+(\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)"
by (induct X, simp_all, blast)
-lemma wdef_Nonce: "[| Nonce n:parts {apm s X}; R:p; msg' R = X; wdef p;
-Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
-(EX k. Nonce k:parts {X} & nonce s k = n)"
+lemma wdef_Nonce: "[| Nonce n \<in> parts {apm s X}; R \<in> p; msg' R = X; wdef p;
+Nonce n \<notin> parts (apm s `(msg `(fst R))) |] ==>
+(\<exists>k. Nonce k \<in> parts {X} \<and> nonce s k = n)"
apply (erule Nonce_apm, unfold wdef_def)
apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
apply (drule_tac x=x in bspec, simp)
apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
by (blast dest: parts_parts)
-primrec ap :: "subs => event => event" where
+primrec ap :: "subs \<Rightarrow> event \<Rightarrow> event" where
"ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)"
| "ap s (Gets A X) = Gets (agent s A) (apm s X)"
| "ap s (Notes A X) = Notes (agent s A) (apm s X)"
abbreviation
- ap' :: "subs => rule => event" where
- "ap' s R == ap s (snd R)"
+ ap' :: "subs \<Rightarrow> rule \<Rightarrow> event" where
+ "ap' s R \<equiv> ap s (snd R)"
abbreviation
- apm' :: "subs => rule => msg" where
- "apm' s R == apm s (msg' R)"
+ apm' :: "subs \<Rightarrow> rule \<Rightarrow> msg" where
+ "apm' s R \<equiv> apm s (msg' R)"
abbreviation
- priK' :: "subs => agent => key" where
- "priK' s A == priK (agent s A)"
+ priK' :: "subs \<Rightarrow> agent \<Rightarrow> key" where
+ "priK' s A \<equiv> priK (agent s A)"
abbreviation
- pubK' :: "subs => agent => key" where
- "pubK' s A == pubK (agent s A)"
+ pubK' :: "subs \<Rightarrow> agent \<Rightarrow> key" where
+ "pubK' s A \<equiv> pubK (agent s A)"
subsection\<open>nonces generated by a rule\<close>
-definition newn :: "rule => nat set" where
-"newn R == {n. Nonce n:parts {msg (snd R)} & Nonce n ~:parts (msg`(fst R))}"
+definition newn :: "rule \<Rightarrow> nat set" where
+"newn R \<equiv> {n. Nonce n \<in> parts {msg (snd R)} \<and> Nonce n \<notin> parts (msg`(fst R))}"
-lemma newn_parts: "n:newn R ==> Nonce (nonce s n):parts {apm' s R}"
+lemma newn_parts: "n \<in> newn R \<Longrightarrow> Nonce (nonce s n) \<in> parts {apm' s R}"
by (auto simp: newn_def dest: apm_parts)
subsection\<open>traces generated by a protocol\<close>
-definition ok :: "event list => rule => subs => bool" where
-"ok evs R s == ((ALL x. x:fst R --> ap s x:set evs)
-& (ALL n. n:newn R --> Nonce (nonce s n) ~:used evs))"
+definition ok :: "event list \<Rightarrow> rule \<Rightarrow> subs \<Rightarrow> bool" where
+"ok evs R s \<equiv> ((\<forall>x. x \<in> fst R \<longrightarrow> ap s x \<in> set evs)
+\<and> (\<forall>n. n \<in> newn R \<longrightarrow> Nonce (nonce s n) \<notin> used evs))"
inductive_set
tr :: "proto => event list set"
for p :: proto
where
- Nil [intro]: "[]:tr p"
+ Nil [intro]: "[] \<in> tr p"
-| Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |]
- ==> Says Spy B X # evsf:tr p"
+| Fake [intro]: "[| evsf \<in> tr p; X \<in> synth (analz (spies evsf)) |]
+ ==> Says Spy B X # evsf \<in> tr p"
-| Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p"
+| Proto [intro]: "[| evs \<in> tr p; R \<in> p; ok evs R s |] ==> ap' s R # evs \<in> tr p"
subsection\<open>general properties\<close>
lemma one_step_tr [iff]: "one_step (tr p)"
apply (unfold one_step_def, clarify)
-by (ind_cases "ev # evs:tr p" for ev evs, auto)
+by (ind_cases "ev # evs \<in> tr p" for ev evs, auto)
definition has_only_Says' :: "proto => bool" where
-"has_only_Says' p == ALL R. R:p --> is_Says (snd R)"
+"has_only_Says' p \<equiv> \<forall>R. R \<in> p \<longrightarrow> is_Says (snd R)"
-lemma has_only_Says'D: "[| R:p; has_only_Says' p |]
-==> (EX A B X. snd R = Says A B X)"
+lemma has_only_Says'D: "[| R \<in> p; has_only_Says' p |]
+==> (\<exists>A B X. snd R = Says A B X)"
by (unfold has_only_Says'_def is_Says_def, blast)
lemma has_only_Says_tr [simp]: "has_only_Says' p ==> has_only_Says (tr p)"
@@ -129,17 +129,17 @@
by (drule_tac x=a in spec, auto simp: is_Says_def)
lemma has_only_Says'_in_trD: "[| has_only_Says' p; list @ ev # evs1 \<in> tr p |]
-==> (EX A B X. ev = Says A B X)"
+==> (\<exists>A B X. ev = Says A B X)"
by (drule has_only_Says_tr, auto)
-lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
-ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
+lemma ok_not_used: "[| Nonce n \<notin> used evs; ok evs R s;
+\<forall>x. x \<in> fst R \<longrightarrow> is_Says x |] ==> Nonce n \<notin> parts (apm s `(msg `(fst R)))"
apply (unfold ok_def, clarsimp)
apply (drule_tac x=x in spec, drule_tac x=x in spec)
by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
-lemma ok_is_Says: "[| evs' @ ev # evs:tr p; ok evs R s; has_only_Says' p;
-R:p; x:fst R |] ==> is_Says x"
+lemma ok_is_Says: "[| evs' @ ev # evs \<in> tr p; ok evs R s; has_only_Says' p;
+R \<in> p; x \<in> fst R |] ==> is_Says x"
apply (unfold ok_def is_Says_def, clarify)
apply (drule_tac x=x in spec, simp)
apply (subgoal_tac "one_step (tr p)")
@@ -149,42 +149,42 @@
subsection\<open>types\<close>
-type_synonym keyfun = "rule => subs => nat => event list => key set"
+type_synonym keyfun = "rule \<Rightarrow> subs \<Rightarrow> nat \<Rightarrow> event list \<Rightarrow> key set"
-type_synonym secfun = "rule => nat => subs => key set => msg"
+type_synonym secfun = "rule \<Rightarrow> nat \<Rightarrow> subs \<Rightarrow> key set \<Rightarrow> msg"
subsection\<open>introduction of a fresh guarded nonce\<close>
-definition fresh :: "proto => rule => subs => nat => key set => event list
-=> bool" where
-"fresh p R s n Ks evs == (EX evs1 evs2. evs = evs2 @ ap' s R # evs1
-& Nonce n ~:used evs1 & R:p & ok evs1 R s & Nonce n:parts {apm' s R}
-& apm' s R:guard n Ks)"
+definition fresh :: "proto \<Rightarrow> rule \<Rightarrow> subs \<Rightarrow> nat \<Rightarrow> key set \<Rightarrow> event list
+\<Rightarrow> bool" where
+"fresh p R s n Ks evs \<equiv> (\<exists>evs1 evs2. evs = evs2 @ ap' s R # evs1
+\<and> Nonce n \<notin> used evs1 \<and> R \<in> p \<and> ok evs1 R s \<and> Nonce n \<in> parts {apm' s R}
+\<and> apm' s R \<in> guard n Ks)"
-lemma freshD: "fresh p R s n Ks evs ==> (EX evs1 evs2.
-evs = evs2 @ ap' s R # evs1 & Nonce n ~:used evs1 & R:p & ok evs1 R s
-& Nonce n:parts {apm' s R} & apm' s R:guard n Ks)"
+lemma freshD: "fresh p R s n Ks evs \<Longrightarrow> (\<exists>evs1 evs2.
+evs = evs2 @ ap' s R # evs1 \<and> Nonce n \<notin> used evs1 \<and> R \<in> p \<and> ok evs1 R s
+\<and> Nonce n \<in> parts {apm' s R} \<and> apm' s R \<in> guard n Ks)"
by (unfold fresh_def, blast)
-lemma freshI [intro]: "[| Nonce n ~:used evs1; R:p; Nonce n:parts {apm' s R};
-ok evs1 R s; apm' s R:guard n Ks |]
+lemma freshI [intro]: "[| Nonce n \<notin> used evs1; R \<in> p; Nonce n \<in> parts {apm' s R};
+ok evs1 R s; apm' s R \<in> guard n Ks |]
==> fresh p R s n Ks (list @ ap' s R # evs1)"
by (unfold fresh_def, blast)
-lemma freshI': "[| Nonce n ~:used evs1; (l,r):p;
-Nonce n:parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r):guard n Ks |]
+lemma freshI': "[| Nonce n \<notin> used evs1; (l,r) \<in> p;
+Nonce n \<in> parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r) \<in> guard n Ks |]
==> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)"
by (drule freshI, simp+)
lemma fresh_used: "[| fresh p R' s' n Ks evs; has_only_Says' p |]
-==> Nonce n:used evs"
+==> Nonce n \<in> used evs"
apply (unfold fresh_def, clarify)
apply (drule has_only_Says'D)
by (auto intro: parts_used_app)
-lemma fresh_newn: "[| evs' @ ap' s R # evs:tr p; wdef p; has_only_Says' p;
-Nonce n ~:used evs; R:p; ok evs R s; Nonce n:parts {apm' s R} |]
-==> EX k. k:newn R & nonce s k = n"
+lemma fresh_newn: "[| evs' @ ap' s R # evs \<in> tr p; wdef p; has_only_Says' p;
+Nonce n \<notin> used evs; R \<in> p; ok evs R s; Nonce n \<in> parts {apm' s R} |]
+==> \<exists>k. k \<in> newn R \<and> nonce s k = n"
apply (drule wdef_Nonce, simp+)
apply (frule ok_not_used, simp+)
apply (clarify, erule ok_is_Says, simp+)
@@ -193,22 +193,22 @@
apply (drule ok_not_used, simp+)
by (clarify, erule ok_is_Says, simp_all)
-lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
-Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
-apply (drule trunc, simp, ind_cases "ev # evs:tr p", simp)
+lemma fresh_rule: "[| evs' @ ev # evs \<in> tr p; wdef p; Nonce n \<notin> used evs;
+Nonce n \<in> parts {msg ev} |] ==> \<exists>R s. R \<in> p \<and> ap' s R = ev"
+apply (drule trunc, simp, ind_cases "ev # evs \<in> tr p", simp)
by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+)
-lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs <= Ks; wdef p;
-has_only_Says' p; evs:tr p; ALL R k s. nonce s k = n --> Nonce n:used evs -->
-R:p --> k:newn R --> Nonce n:parts {apm' s R} --> apm' s R:guard n Ks -->
-apm' s R:parts (spies evs) --> keys R s n evs <= Ks --> P |] ==> P"
+lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs \<subseteq> Ks; wdef p;
+has_only_Says' p; evs \<in> tr p; \<forall>R k s. nonce s k = n \<longrightarrow> Nonce n \<in> used evs \<longrightarrow>
+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>
+apm' s R \<in> parts (spies evs) \<longrightarrow> keys R s n evs \<subseteq> Ks \<longrightarrow> P |] ==> P"
apply (frule fresh_used, simp)
apply (unfold fresh_def, clarify)
apply (drule_tac x=R' in spec)
apply (drule fresh_newn, simp+, clarify)
apply (drule_tac x=k in spec)
apply (drule_tac x=s' in spec)
-apply (subgoal_tac "apm' s' R':parts (spies (evs2 @ ap' s' R' # evs1))")
+apply (subgoal_tac "apm' s' R' \<in> parts (spies (evs2 @ ap' s' R' # evs1))")
apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
apply (case_tac R', drule has_only_Says'D, simp, clarsimp)
apply (rule_tac Y="apm s' X" in parts_parts, blast)
@@ -216,50 +216,50 @@
subsection\<open>safe keys\<close>
-definition safe :: "key set => msg set => bool" where
-"safe Ks G == ALL K. K:Ks --> Key K ~:analz G"
+definition safe :: "key set \<Rightarrow> msg set \<Rightarrow> bool" where
+"safe Ks G \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G"
-lemma safeD [dest]: "[| safe Ks G; K:Ks |] ==> Key K ~:analz G"
+lemma safeD [dest]: "[| safe Ks G; K \<in> Ks |] ==> Key K \<notin> analz G"
by (unfold safe_def, blast)
lemma safe_insert: "safe Ks (insert X G) ==> safe Ks G"
by (unfold safe_def, blast)
-lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n ~:analz G"
+lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n \<notin> analz G"
by (blast dest: Guard_invKey)
subsection\<open>guardedness preservation\<close>
-definition preserv :: "proto => keyfun => nat => key set => bool" where
-"preserv p keys n Ks == (ALL evs R' s' R s. evs:tr p -->
-Guard n Ks (spies evs) --> safe Ks (spies evs) --> fresh p R' s' n Ks evs -->
-keys R' s' n evs <= Ks --> R:p --> ok evs R s --> apm' s R:guard n Ks)"
+definition preserv :: "proto \<Rightarrow> keyfun \<Rightarrow> nat \<Rightarrow> key set \<Rightarrow> bool" where
+"preserv p keys n Ks \<equiv> (\<forall>evs R' s' R s. evs \<in> tr p \<longrightarrow>
+Guard n Ks (spies evs) \<longrightarrow> safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow>
+keys R' s' n evs \<subseteq> Ks \<longrightarrow> R \<in> p \<longrightarrow> ok evs R s \<longrightarrow> apm' s R \<in> guard n Ks)"
-lemma preservD: "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs);
-safe Ks (spies evs); fresh p R' s' n Ks evs; R:p; ok evs R s;
-keys R' s' n evs <= Ks |] ==> apm' s R:guard n Ks"
+lemma preservD: "[| preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs);
+safe Ks (spies evs); fresh p R' s' n Ks evs; R \<in> p; ok evs R s;
+keys R' s' n evs \<subseteq> Ks |] ==> apm' s R \<in> guard n Ks"
by (unfold preserv_def, blast)
-lemma preservD': "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs);
-safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X):p;
-ok evs (l,Says A B X) s; keys R' s' n evs <= Ks |] ==> apm s X:guard n Ks"
+lemma preservD': "[| preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs);
+safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X) \<in> p;
+ok evs (l,Says A B X) s; keys R' s' n evs \<subseteq> Ks |] ==> apm s X \<in> guard n Ks"
by (drule preservD, simp+)
subsection\<open>monotonic keyfun\<close>
definition monoton :: "proto => keyfun => bool" where
-"monoton p keys == ALL R' s' n ev evs. ev # evs:tr p -->
-keys R' s' n evs <= keys R' s' n (ev # evs)"
+"monoton p keys \<equiv> \<forall>R' s' n ev evs. ev # evs \<in> tr p \<longrightarrow>
+keys R' s' n evs \<subseteq> keys R' s' n (ev # evs)"
-lemma monotonD [dest]: "[| keys R' s' n (ev # evs) <= Ks; monoton p keys;
-ev # evs:tr p |] ==> keys R' s' n evs <= Ks"
+lemma monotonD [dest]: "[| keys R' s' n (ev # evs) \<subseteq> Ks; monoton p keys;
+ev # evs \<in> tr p |] ==> keys R' s' n evs \<subseteq> Ks"
by (unfold monoton_def, blast)
subsection\<open>guardedness theorem\<close>
-lemma Guard_tr [rule_format]: "[| evs:tr p; has_only_Says' p;
+lemma Guard_tr [rule_format]: "[| evs \<in> tr p; has_only_Says' p;
preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy) |] ==>
-safe Ks (spies evs) --> fresh p R' s' n Ks evs --> keys R' s' n evs <= Ks -->
+safe Ks (spies evs) \<longrightarrow> fresh p R' s' n Ks evs \<longrightarrow> keys R' s' n evs \<subseteq> Ks \<longrightarrow>
Guard n Ks (spies evs)"
apply (erule tr.induct)
(* Nil *)
@@ -297,59 +297,59 @@
subsection\<open>useful properties for guardedness\<close>
-lemma newn_neq_used: "[| Nonce n:used evs; ok evs R s; k:newn R |]
-==> n ~= nonce s k"
+lemma newn_neq_used: "[| Nonce n \<in> used evs; ok evs R s; k \<in> newn R |]
+==> n \<noteq> nonce s k"
by (auto simp: ok_def)
-lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x:fst R; is_Says x |]
-==> apm s (msg x):parts (spies evs) & apm s (msg x):guard n Ks"
+lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x \<in> fst R; is_Says x |]
+==> apm s (msg x) \<in> parts (spies evs) \<and> apm s (msg x) \<in> guard n Ks"
apply (unfold ok_def is_Says_def, clarify)
apply (drule_tac x="Says A B X" in spec, simp)
by (drule Says_imp_spies, auto intro: parts_parts)
-lemma ok_parts_not_new: "[| Y:parts (spies evs); Nonce (nonce s n):parts {Y};
-ok evs R s |] ==> n ~:newn R"
+lemma ok_parts_not_new: "[| Y \<in> parts (spies evs); Nonce (nonce s n) \<in> parts {Y};
+ok evs R s |] ==> n \<notin> newn R"
by (auto simp: ok_def dest: not_used_not_spied parts_parts)
subsection\<open>unicity\<close>
-definition uniq :: "proto => secfun => bool" where
-"uniq p secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
-n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
-Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
-apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
-evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
-secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
+definition uniq :: "proto \<Rightarrow> secfun \<Rightarrow> bool" where
+"uniq p secret \<equiv> \<forall>evs R R' n n' Ks s s'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow>
+n \<in> newn R \<longrightarrow> n' \<in> newn R' \<longrightarrow> nonce s n = nonce s' n' \<longrightarrow>
+Nonce (nonce s n) \<in> parts {apm' s R} \<longrightarrow> Nonce (nonce s n) \<in> parts {apm' s' R'} \<longrightarrow>
+apm' s R \<in> guard (nonce s n) Ks \<longrightarrow> apm' s' R' \<in> guard (nonce s n) Ks \<longrightarrow>
+evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow>
+secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow>
secret R n s Ks = secret R' n' s' Ks"
-lemma uniqD: "[| uniq p secret; evs: tr p; R:p; R':p; n:newn R; n':newn R';
-nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
-Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
-secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
-apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==>
+lemma uniqD: "[| uniq p secret; evs \<in> tr p; R \<in> p; R' \<in> p; n \<in> newn R; n' \<in> newn R';
+nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs);
+Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'};
+secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs);
+apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks |] ==>
secret R n s Ks = secret R' n' s' Ks"
by (unfold uniq_def, blast)
-definition ord :: "proto => (rule => rule => bool) => bool" where
-"ord p inff == ALL R R'. R:p --> R':p --> ~ inff R R' --> inff R' R"
+definition ord :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> bool" where
+"ord p inff \<equiv> \<forall>R R'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow> \<not> inff R R' \<longrightarrow> inff R' R"
-lemma ordD: "[| ord p inff; ~ inff R R'; R:p; R':p |] ==> inff R' R"
+lemma ordD: "[| ord p inff; \<not> inff R R'; R \<in> p; R' \<in> p |] ==> inff R' R"
by (unfold ord_def, blast)
-definition uniq' :: "proto => (rule => rule => bool) => secfun => bool" where
-"uniq' p inff secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
-inff R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
-Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
-apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
-evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
-secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
+definition uniq' :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> secfun \<Rightarrow> bool" where
+"uniq' p inff secret \<equiv> \<forall>evs R R' n n' Ks s s'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow>
+inff R R' \<longrightarrow> n \<in> newn R \<longrightarrow> n' \<in> newn R' \<longrightarrow> nonce s n = nonce s' n' \<longrightarrow>
+Nonce (nonce s n) \<in> parts {apm' s R} \<longrightarrow> Nonce (nonce s n) \<in> parts {apm' s' R'} \<longrightarrow>
+apm' s R \<in> guard (nonce s n) Ks \<longrightarrow> apm' s' R' \<in> guard (nonce s n) Ks \<longrightarrow>
+evs \<in> tr p \<longrightarrow> Nonce (nonce s n) \<notin> analz (spies evs) \<longrightarrow>
+secret R n s Ks \<in> parts (spies evs) \<longrightarrow> secret R' n' s' Ks \<in> parts (spies evs) \<longrightarrow>
secret R n s Ks = secret R' n' s' Ks"
-lemma uniq'D: "[| uniq' p inff secret; evs: tr p; inff R R'; R:p; R':p; n:newn R;
-n':newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
-Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
-secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
-apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==>
+lemma uniq'D: "[| uniq' p inff secret; evs \<in> tr p; inff R R'; R \<in> p; R' \<in> p; n \<in> newn R;
+n' \<in> newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) \<notin> analz (spies evs);
+Nonce (nonce s n) \<in> parts {apm' s R}; Nonce (nonce s n) \<in> parts {apm' s' R'};
+secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs);
+apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks |] ==>
secret R n s Ks = secret R' n' s' Ks"
by (unfold uniq'_def, blast)
@@ -385,9 +385,9 @@
Says a b (Crypt (pubK b) (Nonce Nb)))"
inductive_set ns :: proto where
- [iff]: "ns1:ns"
-| [iff]: "ns2:ns"
-| [iff]: "ns3:ns"
+ [iff]: "ns1 \<in> ns"
+| [iff]: "ns2 \<in> ns"
+| [iff]: "ns3 \<in> ns"
abbreviation (input)
ns3a :: event where