Theory Implem_symmetric
section ‹Symmetric Implementation of Channel Messages›
theory Implem_symmetric
imports Implem
begin
subsection ‹Implementation of channel messages›
fun implem_sym :: "chan ⇒ msg" where
"implem_sym (Insec A B M) = ⟨InsecTag, Agent A, Agent B, M⟩"
|"implem_sym (Confid A B M) = Enc ⟨ConfidTag, M⟩ (shrK A B)"
|"implem_sym (Auth A B M) = ⟨M, hmac ⟨AuthTag, M⟩ (shrK A B)⟩"
|"implem_sym (Secure A B M) = Enc ⟨SecureTag, M⟩ (shrK A B)"
text ‹
First step: @{locale "basic_implem"}.
Trivial as there are no assumption, this locale just defines some useful abbreviations and valid.
›
interpretation sym: basic_implem implem_sym
done
text ‹Second step: @{locale "semivalid_implem"}.
Here we prove some basic properties such as injectivity and some properties about the
interaction of sets of implementation messages with @{term analz}; these properties are
proved as separate lemmas as the proofs are more complex.
›
text ‹Auxiliary: simpler definitions of the ‹implSets› for the proofs, using the
‹msgSet› definitions.
›
abbreviation implInsecSet_aux :: "msg set ⇒ msg set" where
"implInsecSet_aux G ≡ PairSet Tags (PairSet (range Agent) (PairSet (range Agent) G))"
abbreviation implAuthSet_aux :: "msg set ⇒ msg set" where
"implAuthSet_aux G ≡ PairSet G (HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))))"
abbreviation implConfidSet_aux :: "(agent * agent) set ⇒ msg set ⇒ msg set" where
"implConfidSet_aux Ag G ≡ EncSet (PairSet Tags G) (case_prod shrK`Ag)"
abbreviation implSecureSet_aux :: "(agent * agent) set ⇒ msg set ⇒ msg set" where
"implSecureSet_aux Ag G ≡ EncSet (PairSet Tags G) (case_prod shrK`Ag)"
text ‹These auxiliary definitions are overapproximations.›
lemma implInsecSet_implInsecSet_aux: "sym.implInsecSet G ⊆ implInsecSet_aux G"
by auto
lemma implAuthSet_implAuthSet_aux: "sym.implAuthSet G ⊆ implAuthSet_aux G"
by (auto, auto)
lemma implConfidSet_implConfidSet_aux: "sym.implConfidSet Ag G ⊆ implConfidSet_aux Ag G"
by (auto)
lemma implSecureSet_implSecureSet_aux: "sym.implSecureSet Ag G ⊆ implSecureSet_aux Ag G"
by (auto)
lemmas implSet_implSet_aux =
implInsecSet_implInsecSet_aux implAuthSet_implAuthSet_aux
implConfidSet_implConfidSet_aux implSecureSet_implSecureSet_aux
declare Enc_keys_clean_msgSet_Un [intro]
subsection ‹Lemmas to pull implementation sets out of @{term analz}›
text ‹
All these proofs are similar:
\begin{enumerate}
\item prove the lemma for the @{term "implSet_aux"} and with the set added outside of
@{term analz} given explicitly,
\item prove the lemma for the @{term "implSet_aux"} but with payload, and
\item prove the lemma for the @{term "implSet"}.
\end{enumerate}
There are two cases for the confidential and secure messages:
the general case (the payloads stay in @{term analz}) and the case where the key is unknown
(the messages cannot be opened and are completely removed from the @{term analz}).
›
subsubsection ‹Pull @{term implInsecSet} out of @{term analz}›
lemma analz_Un_implInsecSet_aux_1:
"Enc_keys_clean (G ∪ H) ⟹
analz (implInsecSet_aux G ∪ H) ⊆
implInsecSet_aux G ∪ Tags ∪
PairSet (range Agent) (PairSet (range Agent) G) ∪
PairSet (range Agent) G ∪
analz (range Agent ∪ G ∪ (range Agent ∪ H))"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
have "analz (implInsecSet_aux G ∪ H) ⊆ implInsecSet_aux G ∪
analz (Tags ∪ PairSet (range Agent) (PairSet (range Agent) G) ∪ H)"
by (rule analz_Un_PairSet)
also have "... = implInsecSet_aux G ∪
analz (Tags ∪ (PairSet (range Agent) (PairSet (range Agent) G) ∪ H))"
by (simp only: Un_assoc)
also have "... ⊆ implInsecSet_aux G ∪
(Tags ∪ analz (PairSet (range Agent) (PairSet (range Agent) G) ∪ H))"
by (rule Un_mono, blast, rule analz_Un_Tag, blast intro: H)
also have "... = implInsecSet_aux G ∪ Tags ∪
analz (PairSet (range Agent) (PairSet (range Agent) G) ∪ H)"
by auto
also have "... ⊆ implInsecSet_aux G ∪ Tags ∪ (PairSet (range Agent) (PairSet (range Agent) G) ∪
analz (range Agent ∪ PairSet (range Agent) G ∪ H))"
by (rule Un_mono, blast, rule analz_Un_PairSet)
also have "... = implInsecSet_aux G ∪ Tags ∪ PairSet (range Agent) (PairSet (range Agent) G) ∪
analz (PairSet (range Agent) G ∪ (range Agent ∪ H))"
by (auto simp add: Un_assoc Un_commute)
also have "... ⊆ implInsecSet_aux G ∪ Tags ∪ PairSet (range Agent) (PairSet (range Agent) G) ∪
(PairSet (range Agent) G ∪ analz (range Agent ∪ G ∪ (range Agent ∪ H)))"
by (rule Un_mono, blast, rule analz_Un_PairSet)
also have "... = implInsecSet_aux G ∪ Tags ∪ (PairSet (range Agent) (PairSet (range Agent) G) ∪
PairSet (range Agent) G) ∪ analz (range Agent ∪ G ∪ (range Agent ∪ H))"
by (simp only: Un_assoc Un_commute)
finally show ?thesis by auto
qed
lemma analz_Un_implInsecSet_aux_2:
"Enc_keys_clean (G ∪ H) ⟹
analz (implInsecSet_aux G ∪ H) ⊆
implInsecSet_aux G ∪ Tags ∪
synth (analz (G ∪ H))"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
have HH:"PairSet (range Agent) (PairSet (range Agent) G) ∪
PairSet (range Agent) G ⊆ synth (analz (G ∪ H))"
by auto
have HHH:"analz (range Agent ∪ G ∪ (range Agent ∪ H)) ⊆ synth (analz (G ∪ H))"
proof -
have "analz (range Agent ∪ G ∪ (range Agent ∪ H)) ⊆
synth (analz (range Agent ∪ G ∪ (range Agent ∪ H)))"
by auto
also have "... = synth (analz (synth (range Agent ∪ G ∪ (range Agent ∪ H))))" by auto
also have "... ⊆ synth (analz (synth (G ∪ H)))"
proof (rule synth_analz_mono)
have "range Agent ∪ G ∪ (range Agent ∪ H) ⊆ synth (G ∪ H)" by auto
then have "synth (range Agent ∪ G ∪ (range Agent ∪ H)) ⊆ synth (synth (G ∪ H))"
by (rule synth_mono)
then show "synth (range Agent ∪ G ∪ (range Agent ∪ H)) ⊆ synth (G ∪ H)" by auto
qed
also have "... = synth (analz (G ∪ H))" by auto
finally show ?thesis .
qed
from H have
"analz (implInsecSet_aux G ∪ H) ⊆
implInsecSet_aux G ∪ Tags ∪ PairSet (range Agent) (PairSet (range Agent) G) ∪
PairSet (range Agent) G ∪ analz (range Agent ∪ G ∪ (range Agent ∪ H))"
by (rule analz_Un_implInsecSet_aux_1)
also have "... = implInsecSet_aux G ∪ Tags ∪
(PairSet (range Agent) (PairSet (range Agent) G) ∪
PairSet (range Agent) G) ∪ analz (range Agent ∪ G ∪ (range Agent ∪ H))"
by (simp only: Un_assoc Un_commute)
also have "... ⊆ implInsecSet_aux G ∪ Tags ∪ synth (analz (G ∪ H)) ∪
synth (analz (G ∪ H))"
by ((rule Un_mono)+, auto simp add: HH HHH)
finally show ?thesis by auto
qed
lemma analz_Un_implInsecSet_aux_3:
"Enc_keys_clean (G ∪ H) ⟹
analz (implInsecSet_aux G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implInsecSet_aux_2], auto)
lemma analz_Un_implInsecSet:
"Enc_keys_clean (G ∪ H) ⟹
analz (sym.implInsecSet G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implInsecSet_aux G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implInsecSet_aux_3 apply blast
done
subsection ‹Pull @{term implConfidSet} out of @{term analz}›
lemma analz_Un_implConfidSet_aux_1:
"Enc_keys_clean (G ∪ H) ⟹
analz (implConfidSet_aux Ag G ∪ H) ⊆
implConfidSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪
analz (G ∪ H)"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
have "analz (implConfidSet_aux Ag G ∪ H) ⊆
implConfidSet_aux Ag G ∪ analz (PairSet Tags G ∪ H)"
by (rule analz_Un_EncSet, fast, blast intro: H)
also have "... ⊆ implConfidSet_aux Ag G ∪ (PairSet Tags G ∪ analz (Tags ∪ G ∪ H))"
by (rule Un_mono, blast, rule analz_Un_PairSet)
also have "... = implConfidSet_aux Ag G ∪ PairSet Tags G ∪ analz (Tags ∪ (G ∪ H))"
by (simp only: Un_assoc)
also have "... ⊆ implConfidSet_aux Ag G ∪ PairSet Tags G ∪ (Tags ∪ analz (G ∪ H))"
by (rule Un_mono, blast, rule analz_Un_Tag, blast intro: H)
finally show ?thesis by auto
qed
lemma analz_Un_implConfidSet_aux_2:
"Enc_keys_clean (G ∪ H) ⟹
analz (implConfidSet_aux Ag G ∪ H) ⊆
implConfidSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪
synth (analz (G ∪ H))"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
from H have "analz (implConfidSet_aux Ag G ∪ H) ⊆
implConfidSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪ analz (G ∪ H)"
by (rule analz_Un_implConfidSet_aux_1)
also have "... ⊆ implConfidSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪ synth (analz (G ∪ H))"
by auto
finally show ?thesis by auto
qed
lemma analz_Un_implConfidSet_aux_3:
"Enc_keys_clean (G ∪ H) ⟹
analz (implConfidSet_aux Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implConfidSet_aux_2], auto)
lemma analz_Un_implConfidSet:
"Enc_keys_clean (G ∪ H) ⟹
analz (sym.implConfidSet Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implConfidSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implConfidSet_aux_3 apply blast
done
text ‹Pull @{term implConfidSet} out of @{term analz}, 2nd case where the agents are honest.›
lemma analz_Un_implConfidSet_2_aux_1:
"Enc_keys_clean H ⟹
Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
analz (implConfidSet_aux Ag G ∪ H) ⊆ implConfidSet_aux Ag G ∪ synth (analz H)"
apply (rule subset_trans [OF analz_Un_EncSet2], simp)
apply (auto dest:analz_into_parts)
done
lemma analz_Un_implConfidSet_2_aux_3:
"Enc_keys_clean H ⟹
Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
analz (implConfidSet_aux Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
by (rule subset_trans [OF analz_Un_implConfidSet_2_aux_1], auto)
lemma analz_Un_implConfidSet_2:
"Enc_keys_clean H ⟹
Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
analz (sym.implConfidSet Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
apply (rule subset_trans [of _ "analz (implConfidSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implConfidSet_2_aux_3 apply auto
done
subsection ‹Pull @{term implSecureSet} out of @{term analz}›
lemma analz_Un_implSecureSet_aux_1:
"Enc_keys_clean (G ∪ H) ⟹
analz (implSecureSet_aux Ag G ∪ H) ⊆
implSecureSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪
analz (G ∪ H)"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
have "analz (implSecureSet_aux Ag G ∪ H) ⊆
implSecureSet_aux Ag G ∪ analz (PairSet Tags G ∪ H)"
by (rule analz_Un_EncSet, fast, blast intro: H)
also have "... ⊆ implSecureSet_aux Ag G ∪ (PairSet Tags G ∪ analz (Tags ∪ G ∪ H))"
by (rule Un_mono, blast, rule analz_Un_PairSet)
also have "... = implSecureSet_aux Ag G ∪ PairSet Tags G ∪ analz (Tags ∪ (G ∪ H))"
by (simp only: Un_assoc)
also have "... ⊆ implSecureSet_aux Ag G ∪ PairSet Tags G ∪ (Tags ∪ analz (G ∪ H))"
by (rule Un_mono, blast, rule analz_Un_Tag, blast intro: H)
finally show ?thesis by auto
qed
lemma analz_Un_implSecureSet_aux_2:
"Enc_keys_clean (G ∪ H) ⟹
analz (implSecureSet_aux Ag G ∪ H) ⊆
implSecureSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪
synth (analz (G ∪ H))"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
from H have "analz (implSecureSet_aux Ag G ∪ H) ⊆
implSecureSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪ analz (G ∪ H)"
by (rule analz_Un_implSecureSet_aux_1)
also have "... ⊆ implSecureSet_aux Ag G ∪ PairSet Tags G ∪ Tags ∪ synth (analz (G ∪ H))"
by auto
finally show ?thesis by auto
qed
lemma analz_Un_implSecureSet_aux_3:
"Enc_keys_clean (G ∪ H) ⟹
analz (implSecureSet_aux Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implSecureSet_aux_2], auto)
lemma analz_Un_implSecureSet:
"Enc_keys_clean (G ∪ H) ⟹
analz (sym.implSecureSet Ag G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implSecureSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implSecureSet_aux_3 apply blast
done
text ‹
Pull @{term implSecureSet} out of @{term analz}, 2nd case, where the agents are honest.
›
lemma analz_Un_implSecureSet_2_aux_1:
"Enc_keys_clean H ⟹
Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
analz (implSecureSet_aux Ag G ∪ H) ⊆ implSecureSet_aux Ag G ∪ synth (analz H)"
apply (rule subset_trans [OF analz_Un_EncSet2], simp)
apply (auto dest:analz_into_parts)
done
lemma analz_Un_implSecureSet_2_aux_3:
"Enc_keys_clean H ⟹
Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
analz (implSecureSet_aux Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
by (rule subset_trans [OF analz_Un_implSecureSet_2_aux_1], auto)
lemma analz_Un_implSecureSet_2:
"Enc_keys_clean H ⟹
Ag ∩ broken (parts H ∩ range LtK) = {} ⟹
analz (sym.implSecureSet Ag G ∪ H) ⊆ synth (analz H) ∪ -payload"
apply (rule subset_trans [of _ "analz (implSecureSet_aux Ag G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implSecureSet_2_aux_3 apply auto
done
subsection ‹Pull @{term implAuthSet} out of @{term analz}›
lemma analz_Un_implAuthSet_aux_1:
"Enc_keys_clean (G ∪ H) ⟹
analz (implAuthSet_aux G ∪ H) ⊆
implAuthSet_aux G ∪ HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪
analz (G ∪ H)"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
have "analz (implAuthSet_aux G ∪ H) ⊆ implAuthSet_aux G ∪
analz (G ∪ HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪ H)"
by (rule analz_Un_PairSet)
also have "... = implAuthSet_aux G ∪
analz (HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪ G ∪ H)"
by (simp only: Un_assoc Un_commute)
also have "... = implAuthSet_aux G ∪
analz (HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪ (G ∪ H))"
by (simp only: Un_assoc)
also have
"... ⊆ implAuthSet_aux G ∪
(HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪
analz (G ∪ H))"
by (rule Un_mono, blast, rule analz_Un_HashSet, blast intro: H, auto)
also have "... = implAuthSet_aux G ∪
HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪
analz (G ∪ H)"
by auto
finally show ?thesis by auto
qed
lemma analz_Un_implAuthSet_aux_2:
"Enc_keys_clean (G ∪ H) ⟹
analz (implAuthSet_aux G ∪ H) ⊆
implAuthSet_aux G ∪ HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪
synth (analz (G ∪ H))"
proof -
assume H:"Enc_keys_clean (G ∪ H)"
from H have
"analz (implAuthSet_aux G ∪ H) ⊆
implAuthSet_aux G ∪
HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪
analz (G ∪ H)"
by (rule analz_Un_implAuthSet_aux_1)
also have
"... ⊆ implAuthSet_aux G ∪
HashSet (PairSet (PairSet Tags G) (range (case_prod shrK))) ∪
synth (analz (G ∪ H))"
by auto
finally show ?thesis by auto
qed
lemma analz_Un_implAuthSet_aux_3:
"Enc_keys_clean (G ∪ H) ⟹
analz (implAuthSet_aux G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
by (rule subset_trans [OF analz_Un_implAuthSet_aux_2], auto)
lemma analz_Un_implAuthSet:
"Enc_keys_clean (G ∪ H) ⟹
analz (sym.implAuthSet G ∪ H) ⊆ synth (analz (G ∪ H)) ∪ -payload"
apply (rule subset_trans [of _ "analz (implAuthSet_aux G ∪ H)" _])
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
using analz_Un_implAuthSet_aux_3 apply blast
done
declare Enc_keys_clean_msgSet_Un [rule del]
subsection ‹Locale interpretations›
interpretation sym: semivalid_implem implem_sym
proof (unfold_locales)
fix x A B M x' A' B' M'
show "implem_sym (Chan x A B M) = implem_sym (Chan x' A' B' M') ⟷
x = x' ∧ A = A' ∧ B = B' ∧ M = M'"
by (cases x, (cases x', auto)+)
next
fix M' M x x' A A' B B'
assume H: "M' ∈ payload"
then have A1: "⋀y. y ∈ parts {M'} ⟹ y ∈ payload"
and A2: "⋀y. M' = y ⟹ y ∈ payload" by auto
assume "implem_sym (Chan x A B M) ∈ parts {implem_sym (Chan x' A' B' M')}"
then show "x = x' ∧ A = A' ∧ B = B' ∧ M = M'"
by (cases "x", (cases x', auto dest!: A1 A2)+)
next
fix I
assume "I ⊆ sym.valid"
then show "Enc_keys_clean I"
proof (simp add: Enc_keys_clean_def, intro allI impI)
fix X Y
assume "Enc X Y ∈ parts I"
obtain x A B M where "M ∈ payload" and "Enc X Y ∈ parts {implem_sym (Chan x A B M)}"
using parts_singleton [OF ‹Enc X Y ∈ parts I›] ‹I ⊆ sym.valid›
by (auto elim!: sym.validE)
then show "Y ∈ range LtK ∨ Y ∈ payload" by (cases x, auto)
qed
next
fix Z
show "composed (implem_sym Z)"
proof (cases Z, simp)
fix x A B M
show "composed (implem_sym (Chan x A B M))" by (cases x, auto)
qed
next
fix x A B M
show "implem_sym (Chan x A B M) ∉ payload"
by (cases x, auto)
next
fix X K
assume "X ∈ sym.valid"
then obtain x A B M where "M ∈ payload" "X = implem_sym (Chan x A B M)"
by (auto elim: sym.validE)
then show "LtK K ∉ parts {X}"
by (cases x, auto)
next
fix G H
assume "G ⊆ payload" "Enc_keys_clean H"
hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
then show "analz ({implem_sym (Insec A B M) |A B M. M ∈ G} ∪ H) ⊆
synth (analz (G ∪ H)) ∪ - payload"
by (rule analz_Un_implInsecSet)
next
fix G H
assume "G ⊆ payload" "Enc_keys_clean H"
hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
then show "analz ({implem_sym (Auth A B M) |A B M. M ∈ G} ∪ H) ⊆
synth (analz (G ∪ H)) ∪ - payload"
by (rule analz_Un_implAuthSet)
next
fix G H Ag
assume "G ⊆ payload" "Enc_keys_clean H"
hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
then show "analz ({implem_sym (Confid A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆
synth (analz (G ∪ H)) ∪ - payload"
by (rule analz_Un_implConfidSet)
next
fix G H Ag
assume "G ⊆ payload" "Enc_keys_clean H"
hence "Enc_keys_clean (G ∪ H)" by (auto intro: Enc_keys_clean_Un)
then show "analz ({implem_sym (Secure A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆
synth (analz (G ∪ H)) ∪ - payload"
by (rule analz_Un_implSecureSet)
next
fix G H Ag
assume "Enc_keys_clean H"
hence "Enc_keys_clean H" by auto
moreover assume "Ag ∩ broken (parts H ∩ range LtK) = {}"
ultimately show "analz ({implem_sym (Confid A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆
synth (analz H) ∪ - payload"
by (rule analz_Un_implConfidSet_2)
next
fix G H Ag
assume "Enc_keys_clean H"
moreover assume "Ag ∩ broken (parts H ∩ range LtK) = {}"
ultimately show "analz ({implem_sym (Secure A B M) |A B M. (A, B) ∈ Ag ∧ M ∈ G} ∪ H) ⊆
synth (analz H) ∪ - payload"
by (rule analz_Un_implSecureSet_2)
qed
text ‹
Third step: @{locale "valid_implem"}.
The lemmas giving conditions on $M$, $A$ and $B$ for
@{prop "implXXX A B M ∈ synth (analz Z)"}.
›
lemma implInsec_synth_analz:
"H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags ⟹
sym.implInsec A B M ∈ synth (analz H) ⟹
sym.implInsec A B M ∈ H ∨ M ∈ synth (analz H)"
apply (erule synth.cases, auto)
done
lemma implConfid_synth_analz:
"H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags ⟹
sym.implConfid A B M ∈ synth (analz H) ⟹
sym.implConfid A B M ∈ H ∨ M ∈ synth (analz H)"
apply (erule synth.cases, auto)
apply (frule sym.analz_valid [where x=confid], auto)
done
lemma implAuth_synth_analz:
"H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags ⟹
sym.implAuth A B M ∈ synth (analz H) ⟹
sym.implAuth A B M ∈ H ∨ (M ∈ synth (analz H) ∧ (A, B) ∈ broken H)"
using [[simproc del: defined_all]] proof (erule synth.cases, simp_all)
fix X
assume H: "H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags"
assume H':"⟨M, hmac ⟨AuthTag, M⟩ (shrK A B)⟩ = X" " X ∈ analz H"
hence "sym.implAuth A B M ∈ analz H" by auto
with H have "sym.implAuth A B M ∈ H" by (rule sym.analz_valid)
with H' show "X ∈ H ∨ M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
by auto
next
fix X Y
assume H:"H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags"
assume H':"M = X ∧ hmac ⟨AuthTag, M⟩ (shrK A B) = Y" "Y ∈ synth (analz H)"
hence "hmac ⟨AuthTag, M⟩ (shrK A B) ∈ synth (analz H)" by auto
then have "hmac ⟨AuthTag, M⟩ (shrK A B) ∈ analz H ∨
shrK A B ∈ synth (analz H)"
by (rule synth.cases, auto)
then show "⟨X, hmac ⟨AuthTag, X⟩ (shrK A B)⟩ ∈ H ∨ (A, B) ∈ broken H"
proof
assume "shrK A B ∈ synth (analz H)"
with H have "(A, B) ∈ broken H" by (auto dest:sym.analz_LtKeys)
then show ?thesis by auto
next
assume "hmac ⟨AuthTag, M⟩ (shrK A B) ∈ analz H"
hence "hmac ⟨AuthTag, M⟩ (shrK A B) ∈ parts H" by (rule analz_into_parts)
with H have "hmac ⟨AuthTag, M⟩ (shrK A B) ∈ parts H"
by (auto dest!:payload_parts elim!:payload_Hash)
from H obtain Z where "Z ∈ H" and H'':"hmac ⟨AuthTag, M⟩ (shrK A B) ∈ parts {Z}"
using parts_singleton [OF ‹hmac ⟨AuthTag, M⟩ (shrK A B) ∈ parts H›] by blast
moreover with H have "Z ∈ sym.valid" by (auto dest!: subsetD)
moreover with H'' have "Z = sym.implAuth A B M"
by (auto) (erule sym.valid_cases, auto)
ultimately have "sym.implAuth A B M ∈ H" by auto
with H' show ?thesis by auto
qed
qed
lemma implSecure_synth_analz:
"H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags ⟹
sym.implSecure A B M ∈ synth (analz H) ⟹
sym.implSecure A B M ∈ H ∨ (M ∈ synth (analz H) ∧ (A, B) ∈ broken H)"
apply (erule synth.cases, auto)
apply (frule sym.analz_valid [where x=secure], auto)
apply (frule sym.analz_valid [where x=secure], auto)
apply (auto dest:sym.analz_LtKeys)
done
interpretation sym: valid_implem implem_sym
proof (unfold_locales)
fix H A B M
assume "H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags"
"implem_sym (Insec A B M) ∈ synth (analz H)"
then show "implem_sym (Insec A B M) ∈ H ∨ M ∈ synth (analz H)"
by (rule implInsec_synth_analz)
next
fix H A B M
assume "H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags"
"implem_sym (Confid A B M) ∈ synth (analz H)"
then show "implem_sym (Confid A B M) ∈ H ∨ M ∈ synth (analz H)"
by (rule implConfid_synth_analz)
next
fix H A B M
assume "H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags"
"implem_sym (Auth A B M) ∈ synth (analz H)"
then show "implem_sym (Auth A B M) ∈ H ∨
M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
by (rule implAuth_synth_analz)
next
fix H A B M
assume "H ⊆ payload ∪ sym.valid ∪ range LtK ∪ Tags"
"implem_sym (Secure A B M) ∈ synth (analz H)"
then show "implem_sym (Secure A B M) ∈ H ∨
M ∈ synth (analz H) ∧ (A, B) ∈ broken H"
by (rule implSecure_synth_analz)
qed
end