Theory Implem
section ‹Assumptions for Channel Message Implementation›
text ‹We define a series of locales capturing our assumptions on channel message
implementations.›
theory Implem
imports Channels Payloads
begin
subsection ‹First step: basic implementation locale›
text ‹This locale has no assumptions, it only fixes an implementation function and
defines some useful abbreviations (impl*, impl*Set) and ‹valid›.
›
locale basic_implem =
fixes implem :: "chan ⇒ msg"
begin
abbreviation "implInsec A B M ≡ implem (Insec A B M)"
abbreviation "implConfid A B M ≡ implem (Confid A B M)"
abbreviation "implAuth A B M ≡ implem (Auth A B M)"
abbreviation "implSecure A B M ≡ implem (Secure A B M)"
abbreviation implInsecSet :: "msg set ⇒ msg set"
where "implInsecSet G ≡ {implInsec A B M | A B M. M ∈ G}"
abbreviation implConfidSet :: "(agent * agent) set ⇒ msg set ⇒ msg set"
where "implConfidSet Ag G ≡ {implConfid A B M | A B M. (A, B) ∈ Ag ∧ M ∈ G}"
abbreviation implAuthSet :: "msg set ⇒ msg set"
where "implAuthSet G ≡ {implAuth A B M | A B M. M ∈ G}"
abbreviation implSecureSet :: "(agent * agent) set ⇒ msg set ⇒ msg set"
where "implSecureSet Ag G ≡ {implSecure A B M | A B M. (A, B) ∈ Ag ∧ M ∈ G}"
definition
valid :: "msg set"
where
"valid ≡ {implem (Chan x A B M) | x A B M. M ∈ payload}"
lemma validI:
"M ∈ payload ⟹ implem (Chan x A B M) ∈ valid"
by (auto simp add: valid_def)
lemma validE:
"X ∈ valid ⟹ (⋀ x A B M. X = implem (Chan x A B M) ⟹ M ∈ payload ⟹ P) ⟹ P"
by (auto simp add: valid_def)
lemma valid_cases:
fixes X P
assumes "X ∈ valid"
"(⋀A B M. X = implInsec A B M ⟹ M ∈ payload ⟹ P)"
"(⋀A B M. X = implConfid A B M ⟹ M ∈ payload ⟹ P)"
"(⋀A B M. X = implAuth A B M ⟹ M ∈ payload ⟹ P)"
"(⋀A B M. X = implSecure A B M ⟹ M ∈ payload ⟹ P)"
shows "P"
proof -
from assms have "(⋀ x A B M. X = implem (Chan x A B M) ⟹ M ∈ payload ⟹ P) ⟹ P"
by (auto elim: validE)
moreover from assms have "⋀ x A B M. X = implem (Chan x A B M) ⟹ M ∈ payload ⟹ P"
proof -
fix x A B M
assume "X = implem (Chan x A B M)" "M ∈ payload"
with assms show "P" by (cases x, auto)
qed
ultimately show ?thesis .
qed
end
subsection ‹Second step: basic and analyze assumptions›
text ‹This locale contains most of the assumptions on implem, i.e.:
\begin{itemize}
\item ‹impl_inj›: injectivity
\item ‹parts_impl_inj›: injectivity through parts
\item ‹Enc_parts_valid_impl›: if Enc X Y appears in parts of an implem, then it is
in parts of the payload, or the key is either long term or payload
\item ‹impl_composed›: the implementations are composed (not nonces, agents, tags etc.)
\item ‹analz_Un_implXXXSet›: move the impl*Set out of the analz (only keep the payloads)
\item ‹impl_Impl›: implementations contain implementation material
\item ‹LtK_parts_impl›: no exposed long term keys in the implementations
(i.e., they are only used as keys, or under hashes)
\end{itemize}
›
locale semivalid_implem = basic_implem +
assumes impl_inj:
"implem (Chan x A B M) = implem (Chan x' A' B' M')
⟷ x = x' ∧ A = A' ∧ B = B' ∧ M = M'"
and parts_impl_inj:
"M' ∈ payload ⟹
implem (Chan x A B M) ∈ parts {implem (Chan x' A' B' M')} ⟹
x = x' ∧ A = A' ∧ B = B' ∧ M = M'"
and Enc_keys_clean_valid: "I ⊆ valid ⟹ Enc_keys_clean I"
and impl_composed: "composed (implem Z)"
and impl_Impl: "implem (Chan x A B M) ∉ payload"
and LtK_parts_impl: "X ∈ valid ⟹ LtK K ∉ parts {X}"
and analz_Un_implInsecSet:
"⟦ G ⊆ payload; Enc_keys_clean H ⟧
⟹ analz (implInsecSet G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
and analz_Un_implConfidSet:
"⟦ G ⊆ payload; Enc_keys_clean H ⟧
⟹ analz (implConfidSet Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
and analz_Un_implConfidSet_2:
"⟦ G ⊆ payload; Enc_keys_clean H; Ag ∩ broken (parts H ∩ range LtK) = {} ⟧
⟹ analz (implConfidSet Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
and analz_Un_implAuthSet:
"⟦ G ⊆ payload; Enc_keys_clean H ⟧
⟹ analz (implAuthSet G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
and analz_Un_implSecureSet:
"⟦ G ⊆ payload; Enc_keys_clean H ⟧
⟹ analz (implSecureSet Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
and analz_Un_implSecureSet_2:
"⟦ G ⊆ payload; Enc_keys_clean H; Ag ∩ broken (parts H ∩ range LtK) = {} ⟧
⟹ analz (implSecureSet Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
begin
declare impl_inj [simp]
lemmas parts_implE [elim] = parts_impl_inj [rotated 1]
declare impl_composed [simp, intro]
lemma composed_arg_cong: "X = Y ⟹ composed X ⟷ composed Y"
by (rule arg_cong)
lemma implem_Tags_aux: "implem (Chan x A B M) ∉ Tags" by (cases x, auto dest: composed_arg_cong)
lemma implem_Tags [simp]: "implem x ∉ Tags" by (cases x, auto simp add: implem_Tags_aux)
lemma implem_LtK_aux: "implem (Chan x A B M) ≠ LtK K" by (cases x, auto dest: composed_arg_cong)
lemma implem_LtK [simp]: "implem x ≠ LtK K" by (cases x, auto simp add: implem_LtK_aux)
lemma implem_LtK2 [simp]: "implem x ∉ range LtK" by (cases x, auto simp add: implem_LtK_aux)
declare impl_Impl [simp]
lemma LtK_parts_impl_insert:
"LtK K ∈ parts (insert (implem (Chan x A B M)) S) ⟹ M ∈ payload ⟹ LtK K ∈ parts S"
apply (simp add: parts_insert [of _ S], clarify)
apply (auto dest: validI LtK_parts_impl)
done
declare LtK_parts_impl_insert [dest]
declare Enc_keys_clean_valid [simp, intro]
lemma valid_composed [simp,dest]: "M ∈ valid ⟹ composed M"
by (auto elim: validE)
lemma valid_payload [dest]: "⟦ X ∈ valid; X ∈ payload ⟧ ⟹ P"
by (auto elim!: validE)
lemma valid_isLtKey [dest]: "⟦ X ∈ valid; X ∈ range LtK ⟧ ⟹ P"
by (auto)
lemma analz_valid:
"H ⊆ payload ∪ valid ∪ range LtK ∪ Tags ⟹
implem (Chan x A B M) ∈ analz H ⟹
implem (Chan x A B M) ∈ H"
apply (drule analz_into_parts,
drule parts_monotone [of _ H "payload ∪ H ∩ valid ∪ range LtK ∪ Tags"], auto)
apply (drule parts_singleton, auto elim!:validE dest: parts_impl_inj)
done
lemma parts_valid_LtKeys_disjoint:
"I ⊆ valid ⟹ parts I ∩ range LtK = {}"
apply (safe, drule parts_singleton, clarsimp)
apply (auto dest: subsetD LtK_parts_impl)
done
lemma analz_LtKeys:
"H ⊆ payload ∪ valid ∪ range LtK ∪ Tags ⟹
analz H ∩ range LtK ⊆ H"
apply auto
apply (drule analz_into_parts, drule parts_monotone [of _ H "payload ∪ valid ∪ H ∩ range LtK ∪ Tags"], auto)
apply (drule parts_singleton, auto elim!:validE dest: parts_impl_inj)
done
end
subsection ‹Third step: ‹valid_implem››
text ‹This extends @{locale "semivalid_implem"} with four new assumptions, which under certain
conditions give information on $A$, $B$, $M$ when @{term "implXXX A B M ∈ synth (analz Z)"}.
These assumptions are separated because interpretations are more easily proved, if the
conclusions that follow from the @{locale "semivalid_implem"} assumptions are already
available.
›
locale valid_implem = semivalid_implem +
assumes implInsec_synth_analz:
"H ⊆ payload ∪ valid ∪ range LtK ∪ Tags ⟹
implInsec A B M ∈ synth (analz H) ⟹
implInsec A B M ∈ H ∨ M ∈ synth (analz H)"
and implConfid_synth_analz:
"H ⊆ payload ∪ valid ∪ range LtK ∪ Tags ⟹
implConfid A B M ∈ synth (analz H) ⟹
implConfid A B M ∈ H ∨ M ∈ synth (analz H)"
and implAuth_synth_analz:
"H ⊆ payload ∪ valid ∪ range LtK ∪ Tags ⟹
implAuth A B M ∈ synth (analz H) ⟹
implAuth A B M ∈ H ∨ (M ∈ synth (analz H) ∧ (A, B) ∈ broken H)"
and implSecure_synth_analz:
"H ⊆ payload ∪ valid ∪ range LtK ∪ Tags ⟹
implSecure A B M ∈ synth (analz H) ⟹
implSecure A B M ∈ H ∨ (M ∈ synth (analz H) ∧ (A, B) ∈ broken H)"
end