Theory Message_Authentication_Code
section ‹Security of message authentication›
theory Message_Authentication_Code imports
System_Construction
begin
definition rnd :: "security ⇒ bool list set" where
"rnd η ≡ nlists UNIV η"
definition mac :: "security ⇒ bool list ⇒ bool list ⇒ bool list spmf" where
"mac η r m ≡ return_spmf r"
definition vld :: "security ⇒ bool list set" where
"vld η ≡ nlists UNIV η"
fun valid_mac_query :: "security ⇒ (bool list × bool list) insec_query ⇒ bool" where
"valid_mac_query η (ForwardOrEdit (Some (a, m))) ⟷ a ∈ vld η ∧ m ∈ vld η"
| "valid_mac_query η _ = True"
fun sim :: "('b list × 'b list) option + unit ⇒ ('b list × 'b list) insec_query
⇒ (('b list × 'b list) option × (('b list × 'b list) option + unit), auth_query , 'b list option) gpv" where
"sim (Inr ()) _ = Done (None, Inr())"
| "sim (Inl None) (Edit (a', m')) = do { _ ← Pause Drop Done; Done (None, Inr ())}"
| "sim (Inl (Some (a, m))) (Edit (a', m')) = (if a = a' ∧ m = m'
then do { _ ← Pause Forward Done; Done (None, Inl (Some (a, m)))}
else do { _ ← Pause Drop Done; Done (None, Inr ())})"
| "sim (Inl None) Forward = do {
Pause Forward Done;
Done (None, Inl None) }"
| "sim (Inl (Some _)) Forward = do {
Pause Forward Done;
Done (None, Inr ()) }"
| "sim (Inl None) Drop = do {
Pause Drop Done;
Done (None, Inl None) }"
| "sim (Inl (Some _)) Drop = do {
Pause Drop Done;
Done (None, Inr ()) }"
| "sim (Inl (Some (a, m))) Look = do {
lo ← Pause Look Done;
(case lo of
Some m ⇒ Done (Some (a, m), Inl (Some (a, m)))
| None ⇒ Done (None, Inl (Some (a, m))))}"
| "sim (Inl None) Look = do {
lo ← Pause Look Done;
(case lo of
Some m ⇒ do {
a ← lift_spmf (spmf_of_set (nlists UNIV (length m)));
Done (Some (a, m), Inl (Some (a, m)))}
| None ⇒ Done (None, Inl None))}"
context
fixes η :: "security"
begin
private definition rorc_channel_send :: "((bool × unit) × (bool list ⇒ bool list option) × (bool list × bool list) cstate, bool list, unit) oracle'" where
"rorc_channel_send s m ≡ (if fst (fst s)
then return_spmf ((), (True, ()), snd s)
else do {
(r, s) ← (rorc.rnd_oracle (rnd η))† (snd s) m;
a ← mac η r m;
(_, s) ← †channel.send_oracle s (a, m);
return_spmf ((), (True, ()), s)
})"
private definition rorc_channel_recv :: "((bool × unit) × (bool list ⇒ bool list option) × (bool list × bool list) cstate, unit, bool list option) oracle'" where
"rorc_channel_recv s q ≡ do {
(m, s) ← ††channel.recv_oracle s ();
(case m of
None ⇒ return_spmf (None, s)
| Some (a, m) ⇒ do {
(r, s) ← †(rorc.rnd_oracle (rnd η))† s m;
a' ← mac η r m;
return_spmf (if a' = a then Some m else None, s)})
}"
private definition rorc_channel_recv_f :: "((bool list ⇒ bool list option) × (bool list × bool list) cstate, unit, bool list option) oracle'" where
"rorc_channel_recv_f s q ≡ do {
(am, (as, ams)) ← †channel.recv_oracle s ();
(case am of
None ⇒ return_spmf (None, (as, ams))
| Some (a, m) ⇒ (case as m of
None ⇒ do {
a'' :: bool list ← spmf_of_set (nlists UNIV η - {a});
a' ← spmf_of_set (nlists UNIV η);
(if a' = a
then return_spmf (None, as(m := Some a''), ams)
else return_spmf (None, as(m := Some a'), ams)) }
| Some a' ⇒ return_spmf (if a' = a then Some m else None, as, ams)))}"
private fun lazy_channel_send :: "(bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option), bool list, unit) oracle'" where
"lazy_channel_send (Void, es) m = return_spmf ((), (Store m, es))"
| "lazy_channel_send s m = return_spmf ((), s)"
private fun lazy_channel_recv :: "(bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option), unit, bool list option) oracle'" where
"lazy_channel_recv (Collect m, None, as) () = return_spmf (Some m, (Fail, None, as))"
| "lazy_channel_recv (ms, Some (a', m'), as) () = (case as m' of
None ⇒ do {
a ← spmf_of_set (rnd η);
return_spmf (if a = a' then Some m' else None, cstate.Fail, None, as (m' := Some a))}
| Some a ⇒ return_spmf (if a = a' then Some m' else None, Fail, None, as))"
| "lazy_channel_recv s () = return_spmf (None, s)"
private fun lazy_channel_insec :: "(bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option),
(bool list × bool list) insec_query, (bool list × bool list) option) oracle'" where
"lazy_channel_insec (Void, _, as) (Edit (a', m')) = return_spmf (None, (Collect m', Some (a', m'), as))"
| "lazy_channel_insec (Store m, _, as) (Edit (a', m')) = return_spmf (None, (Collect m', Some (a', m'), as))"
| "lazy_channel_insec (Store m, es) Forward = return_spmf (None, (Collect m, es))"
| "lazy_channel_insec (Store m, es) Drop = return_spmf (None, (Fail, es))"
| "lazy_channel_insec (Store m, None, as) Look = (case as m of
None ⇒ do {
a ← spmf_of_set (rnd η);
return_spmf (Some (a, m), Store m, None, as (m := Some a))}
| Some a ⇒ return_spmf (Some (a, m), Store m, None, as))"
| "lazy_channel_insec s _ = return_spmf (None, s)"
private fun lazy_channel_recv_f :: "(bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option), unit, bool list option) oracle'" where
"lazy_channel_recv_f (Collect m, None, as) () = return_spmf (Some m, (Fail, None, as))"
| "lazy_channel_recv_f (ms, Some (a', m'), as) () = (case as m' of
None ⇒ do {
a ← spmf_of_set (rnd η);
return_spmf (None, Fail, None, as (m' := Some a))}
| Some a ⇒ return_spmf (if a = a' then Some m' else None, Fail, None, as))"
| "lazy_channel_recv_f s () = return_spmf (None, s)"
private abbreviation callee_auth_channel where
"callee_auth_channel callee ≡ lift_state_oracle extend_state_oracle (attach_callee callee auth_channel.auth_oracle)"
private abbreviation
"valid_insecQ ≡ {(x :: (bool list × bool list) insec_query). case x of
ForwardOrEdit (Some (a, m)) ⇒ length a = id' η ∧ length m = id' η
| _ ⇒ True}"
private inductive S :: "(bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option)) spmf
⇒ ((bool × unit) × (bool list ⇒ bool list option) × (bool list × bool list) cstate) spmf ⇒ bool" where
"S (return_spmf (Void, None, Map.empty))
(return_spmf ((False, ()), Map.empty, Void))"
| "S (return_spmf (Store m, None, Map.empty))
(map_spmf (λa. ((True, ()), [m ↦ a], Store (a, m))) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η"
| "S (return_spmf (Collect m, None, Map.empty))
(map_spmf (λa. ((True, ()), [m ↦ a], Collect (a, m))) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η"
| "S (return_spmf (Store m, None, [m ↦ a]))
(return_spmf ((True, ()), [m ↦ a], Store (a, m)))"
if "length m = id' η" and "length a = id' η"
| "S (return_spmf (Collect m, None, [m ↦ a]))
(return_spmf ((True, ()), [m ↦ a], Collect (a, m)))"
if "length m = id' η" and "length a = id' η"
| "S (return_spmf (Fail, None, Map.empty))
(map_spmf (λa. ((True, ()), [m ↦ a], Fail)) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η"
| "S (return_spmf (Fail, None, [m ↦ a]))
(return_spmf ((True, ()), [m ↦ a], Fail))"
if "length m = id' η" and "length a = id' η"
| "S (return_spmf (Collect m', Some (a', m'), Map.empty))
(return_spmf ((False, ()), Map.empty, Collect (a', m')))"
if "length m' = id' η" and "length a' = id' η"
| "S (return_spmf (Collect m', Some (a', m'), [m ↦ a]))
(return_spmf ((True, ()), [m ↦ a], Collect (a', m')))"
if "length m = id' η" and "length a = id' η" and "length m' = id' η" and "length a' = id' η"
| "S (return_spmf (Collect m', Some (a', m'), Map.empty))
(map_spmf (λx. ((True, ()), [m ↦ x], Collect (a', m'))) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η" and "length m' = id' η" and "length a' = id' η"
| "S (map_spmf (λx. (Fail, None, as(m' ↦ x))) spmf_s)
(map_spmf (λx. ((False, ()), as(m' ↦ x), Fail)) spmf_s)"
if "length m' = id' η" and "lossless_spmf spmf_s"
| "S (map_spmf (λx. (Fail, None, as(m' ↦ x))) spmf_s)
(map_spmf (λx. ((True, ()), as(m' ↦ x), Fail)) spmf_s)"
if "length m' = id' η" and "lossless_spmf spmf_s"
| "S (return_spmf (Fail, None, [m' ↦ a']))
(map_spmf (λx. ((True, ()), [m ↦ x, m' ↦ a'], Fail)) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η" and "length m'= id' η" and "length a' = id' η"
| "S (map_spmf (λx. (Fail, None, [m' ↦ x])) (spmf_of_set (nlists UNIV η ∩ {x. x ≠ a'})))
(map_spmf (λx. ((True, ()), [m ↦ fst x, m' ↦ snd x], Fail)) (spmf_of_set (nlists UNIV η × nlists UNIV η ∩ {x. snd x ≠ a'})))"
if "length m = id' η" and "length m'= id' η"
| "S (map_spmf (λx. (Fail, None, as(m' ↦ x))) spmf_s)
(map_spmf (λp. ((True, ()), as(m' ↦ fst p, m ↦ snd p), Fail)) (mk_lossless (pair_spmf spmf_s (spmf_of_set (nlists UNIV η)))))"
if "length m = id' η" and "length m'= id' η" and "lossless_spmf spmf_s"
private lemma trace_eq_lazy:
assumes "η > 0"
shows "(valid_insecQ <+> nlists UNIV (id' η) <+> UNIV) ⊢⇩R
RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv) (Void, None, Map.empty)
≈
RES (††insec_channel.insec_oracle ⊕⇩O rorc_channel_send ⊕⇩O rorc_channel_recv) ((False, ()), Map.empty, Void)"
(is "?A ⊢⇩R RES (?L1 ⊕⇩O ?L2 ⊕⇩O ?L3) ?SL ≈ RES (?R1 ⊕⇩O ?R2 ⊕⇩O ?R3) ?SR")
proof -
note [simp] =
spmf.map_comp o_def map_bind_spmf bind_map_spmf bind_spmf_const exec_gpv_bind
insec_channel.insec_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps
rorc_channel_send_def rorc_channel_recv_def rorc.rnd_oracle.simps mac_def rnd_def
have aux1: "nlists (UNIV::bool set) η × nlists (UNIV::bool set) η ∩ {x. snd x ≠ a'} ≠ {}" (is ?aux1)
and aux2: "nlists (UNIV::bool set) η ∩ {x. x ≠ a'} ≠ {}" (is ?aux2) for a'
proof -
have "∃a. a ∈ nlists (UNIV::bool set) η ∧ a ≠ a'" for a'
proof (cases "a' ∈ nlists (UNIV::bool set) η")
case True
show ?thesis
proof (rule ccontr)
have "2 ^ η = card (nlists (UNIV :: bool set) η)" by (simp add: card_nlists)
also assume "∄a. a ∈ nlists UNIV η ∧ a ≠ a'"
then have "nlists UNIV η = {a'}" using True by blast
then have fct:"card (nlists (UNIV :: bool set) η) = card {a'}" by simp
also have " card {a'} = 1" by simp
finally have "η = 0" by simp
then show "False" using assms by blast
qed
next
case False
obtain a where obt:"a ∈ nlists (UNIV::bool set) η" using assms by auto
then have "a ≠ a'" using False by blast
then show ?thesis using obt by auto
qed
then obtain a where o1: "a ∈ nlists (UNIV::bool set) η" and o2: "a ≠ a'" by blast
obtain m where "m ∈ nlists (UNIV::bool set) η" by blast
with o1 o2 have "(m, a) ∈ {x. snd x ≠ a'}" and "(m, a) ∈ nlists UNIV η × nlists UNIV η" by auto
then show ?aux1 by blast
from o1 o2 have "a ∈ {x. x ≠ a'}" and "a ∈ nlists UNIV η" by auto
then show ?aux2 by blast
qed
have *: "?A ⊢⇩C ?L1 ⊕⇩O ?L2 ⊕⇩O ?L3(?SL) ≈ ?R1 ⊕⇩O ?R2 ⊕⇩O ?R3(?SR)"
proof(rule trace'_eqI_sim[where S=S], goal_cases Init_OK Output_OK State_OK)
case Init_OK
then show ?case by (simp add: S.simps)
next
case (Output_OK p q query)
show ?case
proof (cases query)
case (Inl adv_query)
with Output_OK show ?thesis
proof cases
case (14 m m' a')
then show ?thesis using Output_OK(2) Inl
by(cases adv_query)(simp; subst (1 2) weight_spmf_of_set_finite; auto simp add: assms aux1 aux2)+
qed (auto simp add: weight_mk_lossless lossless_spmf_def split: aquery.splits option.splits)
next
case Snd_Rcv: (Inr query')
show ?thesis
proof (cases query')
case (Inl snd_query)
with Output_OK Snd_Rcv show ?thesis
proof cases
case (11 m' _ as)
with Output_OK(2) Snd_Rcv Inl show ?thesis
by(cases "snd_query = m'"; cases "as snd_query")(simp_all)
next
case (14 m m' a')
with Output_OK(2) Snd_Rcv Inl show ?thesis
by(simp; subst (1 2) weight_spmf_of_set_finite; auto simp add: assms aux1 aux2)
qed (auto simp add: weight_mk_lossless lossless_spmf_def)
next
case (Inr rcv_query)
with Output_OK Snd_Rcv show ?thesis
proof cases
case (10 m m' a')
with Output_OK(2) Snd_Rcv Inr show ?thesis by(cases "m = m'")(simp_all)
next
case (14 m m' a')
with Output_OK(2) Snd_Rcv Inr show ?thesis
by(simp; subst (1 2) weight_spmf_of_set_finite; auto simp add: assms aux1 aux2)
qed (auto simp add: weight_mk_lossless lossless_spmf_def split:option.splits)
qed
qed
next
case (State_OK p q query state answer state')
show ?case
proof (cases query)
case (Inl adv_query)
show ?thesis
proof (cases adv_query)
case Look
with State_OK Inl show ?thesis
proof cases
case Store_State_Channel: (2 m)
have[simp]: " a ∈ nlists UNIV η ⟹
S (cond_spmf_fst (map_spmf (λx. (Inl (Some (x, m)), Store m, None, [m ↦ x]))
(spmf_of_set (nlists UNIV η))) (Inl (Some (a, m))))
(cond_spmf_fst (map_spmf (λx. (Inl (Some (x, m)), (True, ()), [m ↦ x], Store (x, m)))
(spmf_of_set (nlists UNIV η))) (Inl (Some (a, m))))" for a
proof(subst (1 2) cond_spmf_fst_map_Pair1, goal_cases)
case 4
then show ?case
by(subst (1 2 3) inv_into_f_f, simp_all add: inj_on_def)
(rule S.intros, simp_all add: Store_State_Channel in_nlists_UNIV id'_def)
qed (simp_all add: id'_def inj_on_def)
from Store_State_Channel show ?thesis using State_OK Inl Look
by(clarsimp simp add: map_spmf_conv_bind_spmf[symmetric])
qed (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro: S.intros)
next
case (ForwardOrEdit foe)
with State_OK Inl show ?thesis
proof (cases foe)
case (Some am')
obtain a' m' where "am' = (a', m')" by (cases am') simp
with State_OK Inl ForwardOrEdit Some show ?thesis
by cases (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro: S.intros elim:S.cases)
qed (erule S.cases, auto simp add: map_spmf_conv_bind_spmf[symmetric] intro: S.intros)
next
case Drop
with State_OK Inl show ?thesis
by cases (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro: S.intros)
qed
next
case Snd_Rcv: (Inr query')
show ?thesis
proof (cases query')
case (Inl snd_query)
with State_OK Snd_Rcv show ?thesis
proof cases
case 1
with State_OK Snd_Rcv Inl show ?thesis
by(clarsimp simp add: map_spmf_conv_bind_spmf[symmetric])
(rule S.intros, simp add: in_nlists_UNIV)
next
case (8 m' a')
with State_OK Snd_Rcv Inl show ?thesis
by(clarsimp simp add: map_spmf_conv_bind_spmf[symmetric])
(rule S.intros, simp add: in_nlists_UNIV)
next
case (11 m' spmf_s as)
with State_OK Snd_Rcv Inl show ?thesis
by(auto simp add: bind_bind_conv_pair_spmf split_def split: if_splits option.splits intro!: S.intros)
((auto simp add: map_spmf_conv_bind_spmf[symmetric] intro!: S.intros), simp only: id'_def in_nlists_UNIV)
qed (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro: S.intros)
next
case (Inr rcv_query)
with State_OK Snd_Rcv show ?thesis
proof(cases)
case (8 m' a')
then show ?thesis using State_OK(2-) Snd_Rcv Inr
by (auto simp add: map_spmf_conv_bind_spmf[symmetric] image_def
cond_spmf_fst_def vimage_def aux1 aux2 assms intro:S.intros)
next
case (9 m a m' a')
then show ?thesis using State_OK(2-) Snd_Rcv Inr
by (cases "m = m'") (auto simp add: map_spmf_conv_bind_spmf[symmetric] cond_spmf_fst_def
vimage_def aux1 aux2 assms intro:S.intros split!: if_splits)
next
case (10 m m' a')
show ?thesis
proof (cases "m = m'")
case True
with 10 show ?thesis using State_OK(2-) Snd_Rcv Inr
by (auto simp add: map_spmf_conv_bind_spmf[symmetric] cond_spmf_fst_def
vimage_def aux1 aux2 assms split!: if_split intro:S.intros)
next
case False
have[simp]: "a' ∈ nlists UNIV η ⟹ nlists (UNIV :: bool set) η × nlists UNIV η ∩ {x. snd x = a'} = nlists UNIV η × {a'}"
by auto
from 10 False show ?thesis using State_OK(2-) Snd_Rcv Inr
by(simp add: bind_bind_conv_pair_spmf)
((auto simp add: bind_bind_conv_pair_spmf split_def image_def map_spmf_conv_bind_spmf[symmetric]
cond_spmf_fst_def vimage_def cond_spmf_spmf_of_set pair_spmf_of_set )
, (auto simp add: pair_spmf_of_set[symmetric] spmf_of_set_singleton pair_spmf_return_spmf2
map_spmf_of_set_inj_on[symmetric] simp del: map_spmf_of_set_inj_on intro: S.intros))
qed
qed (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro: S.intros)
qed
qed
qed
from * show ?thesis by simp
qed
private lemma game_difference:
defines "ℐ ≡ ℐ_uniform (Set.Collect (valid_mac_query η)) (insert None (Some ` (nlists UNIV η × nlists UNIV η))) ⊕⇩ℐ
(ℐ_uniform (vld η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` vld η)))"
assumes bound: "interaction_bounded_by' (λ_. True) 𝒜 q"
and lossless: "plossless_gpv ℐ 𝒜"
and WT: "ℐ ⊢g 𝒜 √"
shows
"¦spmf (connect 𝒜 (RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f) (Void, None, Map.empty))) True -
spmf (connect 𝒜 (RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv) (Void, None, Map.empty))) True¦
≤ q / real (2 ^ η)" (is "?LHS ≤ _")
proof -
define lazy_channel_insec' where
"lazy_channel_insec' = (†lazy_channel_insec :: (bool × bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option),
(bool list × bool list) insec_query, (bool list × bool list) option) oracle')"
define lazy_channel_send' where
"lazy_channel_send' = (†lazy_channel_send :: (bool × bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option),
bool list, unit) oracle')"
define lazy_channel_recv' where
"lazy_channel_recv' = (λ (s :: bool × bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option)) (q :: unit).
(case s of
(flg, Collect m, None, as) ⇒ return_spmf (Some m, (flg, Fail, None, as))
| (flg, ms, Some (a', m'), as) ⇒ (case as m' of
None ⇒ do {
a ← spmf_of_set (rnd η);
return_spmf (if a = a' then Some m' else None, flg ∨ a = a', Fail, None, as (m' := Some a))}
| Some a ⇒ return_spmf (if a = a' then Some m' else None, flg, Fail, None, as))
| _ ⇒ return_spmf (None, s)))"
define lazy_channel_recv_f' where
"lazy_channel_recv_f' = (λ (s :: bool × bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option)) (q :: unit).
(case s of
(flg, Collect m, None, as) ⇒ return_spmf (Some m, (flg, Fail, None, as))
| (flg, ms, Some (a', m'), as) ⇒ (case as m' of
None ⇒ do {
a ← spmf_of_set (rnd η);
return_spmf (None, flg ∨ a = a', Fail, None, as (m' := Some a))}
| Some a ⇒ return_spmf (if a = a' then Some m' else None, flg, Fail, None, as))
| _ ⇒ return_spmf (None, s)))"
define game where
"game = (λ(𝒜 :: ((bool list × bool list) insec_query + bool list + unit, (bool list × bool list) option + unit + bool list option) distinguisher) recv_oracle. do {
(b :: bool, (flg, ams, es, as))← (exec_gpv (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O recv_oracle) 𝒜 (False, Void, None, Map.empty));
return_spmf (b, flg) })"
have fact1: "spmf (connect 𝒜 (RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f) (Void, None, Map.empty))) True
= spmf (connect 𝒜 (RES (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f') (False, Void, None, Map.empty))) True"
proof -
let ?orc_lft = "lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f"
let ?orc_rgt = "lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f'"
have[simp]: "rel_spmf (rel_prod (=) (λx y. x = snd y))
(lazy_channel_insec s q) (lazy_channel_insec' (flg, s) q) " for s flg q
by (cases s) (simp add: lazy_channel_insec'_def spmf_rel_map rel_prod_sel split_def option.rel_refl pmf.rel_refl split:option.split)
have[simp]: "rel_spmf (rel_prod (=) (λx y. x = snd y))
(lazy_channel_send s q) (lazy_channel_send' (flg, s) q)" for s flg q
proof -
obtain ams es as where "s = (ams, es, as)" by (cases s)
then show ?thesis by (cases ams) (auto simp add: spmf_rel_map map_spmf_conv_bind_spmf split_def lazy_channel_send'_def)
qed
have[simp]: "rel_spmf (rel_prod (=) (λx y. x = snd y))
(lazy_channel_recv_f s q) (lazy_channel_recv_f' (flg, s) q)" for s flg q
proof -
obtain ams es as where *: "s = (ams, es, as)" by (cases s)
show ?thesis
proof (cases es)
case None
with * show ?thesis by (cases ams) (simp_all add:lazy_channel_recv_f'_def)
next
case (Some am)
obtain a m where "am = (a, m)" by (cases am)
with * show ?thesis by (cases ams) (simp_all add: lazy_channel_recv_f'_def rel_spmf_bind_reflI split:option.split)
qed
qed
have[simp]: "rel_spmf (rel_prod (=) (λx y. x = snd y))
((lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f) (ams, es, as) query)
((lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f') (flg, ams, es, as) query)" for flg ams es as query
proof (cases query)
case (Inl adv_query)
then show ?thesis
by(clarsimp simp add: spmf_rel_map map_spmf_conv_bind_spmf[symmetric] apfst_def map_prod_def split_beta)
((rule rel_spmf_mono[where A="rel_prod (=) (λx y. x = snd y)"]), auto)
next
case (Inr query')
note Snd_Rcv = this
then show ?thesis
by (cases query', auto simp add: spmf_rel_map map_spmf_conv_bind_spmf[symmetric] split_beta)
((rule rel_spmf_mono[where A="rel_prod (=) (λx y. x = snd y)"]); auto)+
qed
have[simp]: "rel_spmf (λx y. fst x = fst y)
(exec_gpv ?orc_lft 𝒜 (Void, None, Map.empty)) (exec_gpv ?orc_rgt 𝒜 (False, Void, None, Map.empty))"
by(rule rel_spmf_mono[where A="rel_prod (=) (λx y. x = snd y)"])
(auto simp add: gpv.rel_eq split_def intro!: rel_funI
exec_gpv_parametric[where CALL="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD])
show ?thesis
unfolding map_spmf_conv_bind_spmf exec_gpv_resource_of_oracle connect_def spmf_conv_measure_spmf
by(rule measure_spmf_parametric[where A="(=)", THEN rel_funD, THEN rel_funD])
(auto simp add: rel_pred_def spmf_rel_map map_spmf_conv_bind_spmf[symmetric] gpv.rel_eq split_def intro!: rel_funI)
qed
have fact2: "¦spmf (connect 𝒜 (RES (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f') (False, Void, None, Map.empty))) True -
spmf (connect 𝒜 (RES (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv') (False, Void, None, Map.empty))) True¦
≤ Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. snd x}" (is "¦spmf ?L _ - spmf ?R _ ¦ ≤ _ ")
proof -
let ?orc_lft = "lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f'"
let ?orc_rgt = "lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv'"
have[simp]: "callee_invariant_on lazy_channel_insec' fst (ℐ_uniform (Set.Collect (valid_mac_query η)) UNIV)"
proof (unfold_locales, goal_cases)
case (1 state query answer state')
then show ?case
by(cases state; cases "fst (snd state)")(auto simp add: spmf_rel_map map_spmf_conv_bind_spmf split_def lazy_channel_insec'_def)
qed (auto intro: WT_calleeI)
have[simp]: "callee_invariant_on lazy_channel_send' fst (ℐ_uniform (vld η) UNIV)"
proof (unfold_locales, goal_cases)
case (1 state query answer state')
then show ?case
by(cases state; cases "fst (snd state)")(auto simp add: spmf_rel_map map_spmf_conv_bind_spmf split_def lazy_channel_send'_def)
qed (auto intro: WT_calleeI)
have[simp]: "callee_invariant lazy_channel_recv' fst"
proof (unfold_locales, goal_cases)
case (1 state query answer state')
then show ?case
by(cases state; cases "fst (snd state)")(auto simp add: lazy_channel_recv'_def split:option.splits)
qed (auto split:option.splits)
have[simp]: "callee_invariant lazy_channel_recv_f' fst"
proof (unfold_locales, goal_cases)
case (1 state query answer state')
then show ?case
by(cases state; cases "fst (snd state)")(auto simp add: lazy_channel_recv_f'_def split:option.splits)
qed (auto split:option.splits)
have[simp]: "lossless_spmf (lazy_channel_insec s q)" for s q
by(cases "(s, q)" rule: lazy_channel_insec.cases)(auto simp add: rnd_def split!: option.split)
have[simp]: "lossless_spmf (lazy_channel_send' s q)" for s q
by(cases s; cases "fst (snd s)")(simp_all add: lazy_channel_send'_def)
have[simp]: "lossless_spmf (lazy_channel_recv' s ())" for s
by(auto simp add: lazy_channel_recv'_def rnd_def split: prod.split cstate.split option.split)
have[simp]: "lossless_spmf (lazy_channel_recv_f' s ())" for s
by(auto simp add: lazy_channel_recv_f'_def rnd_def split: prod.split cstate.split option.split)
have[simp]: "rel_spmf (λ(a, s1') (b, s2'). (fst s2' ⟶ fst s1') ∧ (¬ fst s2' ⟶ ¬ fst s1' ∧ a = b ∧ s1' = s2'))
(?orc_lft (flg, ams, es, as) query) (?orc_rgt (flg, ams, es, as) query)" for flg ams es as query
proof (cases query)
case (Inl adv_query)
then show ?thesis by (auto simp add: spmf_rel_map map_spmf_conv_bind_spmf intro: rel_spmf_bind_reflI)
next
case (Inr query')
note Snd_Rcv = this
show ?thesis
proof (cases query')
case (Inl snd_query)
with Snd_Rcv show ?thesis
by (auto simp add: spmf_rel_map map_spmf_conv_bind_spmf intro: rel_spmf_bind_reflI)
next
case (Inr rcv_query)
with Snd_Rcv show ?thesis
proof (cases es)
case (Some am')
obtain a' m' where "am' = (a', m')" by (cases am')
with Snd_Rcv Some Inr show ?thesis
by (cases ams) (auto simp add: spmf_rel_map map_spmf_conv_bind_spmf
lazy_channel_recv'_def lazy_channel_recv_f'_def rel_spmf_bind_reflI split:option.splits)
qed (cases ams; auto simp add: lazy_channel_recv'_def lazy_channel_recv_f'_def split:option.splits)
qed
qed
let ?ℐ = "ℐ_uniform (Set.Collect (valid_mac_query η)) UNIV ⊕⇩ℐ (ℐ_uniform (vld η) UNIV ⊕⇩ℐ ℐ_full)"
let ?𝒜 = "mk_lossless_gpv (responses_ℐ ℐ) True 𝒜"
have "plossless_gpv ?ℐ ?𝒜" using lossless WT
by(rule plossless_gpv_mk_lossless_gpv)(simp add: ℐ_def)
moreover have "?ℐ ⊢g ?𝒜 √" using WT by(rule WT_gpv_mk_lossless_gpv)(simp add: ℐ_def)
ultimately have "rel_spmf (λx y. fst (snd x) = fst (snd y) ∧ (¬ fst (snd y) ⟶ (fst x ⟷ fst y)))
(exec_gpv ?orc_lft ?𝒜 (False, Void, None, Map.empty)) (exec_gpv ?orc_rgt ?𝒜 (False, Void, None, Map.empty))"
by(auto simp add: ℐ_def intro!: exec_gpv_oracle_bisim_bad_plossless[where X="(=)" and
X_bad="λ _ _. True" and ?bad1.0="fst" and ?bad2.0="fst" and ℐ = "?ℐ", THEN rel_spmf_mono])
(auto simp add: lazy_channel_insec'_def intro: WT_calleeI)
also let ?I = "(λ(_, s1, s2, s3). pred_cstate (λx. length x = η) s1 ∧ pred_option (λ(x, y). length x = η ∧ length y = η) s2 ∧ ran s3 ⊆ nlists UNIV η)"
have "callee_invariant_on (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f') ?I ℐ"
apply(unfold_locales)
subgoal for s x y s'
supply [[simproc del: defined_all]]
apply(clarsimp simp add: ℐ_def; elim PlusE; clarsimp simp add: lazy_channel_insec'_def lazy_channel_send'_def lazy_channel_recv_f'_def)
subgoal for _ _ _ _ x'
by(cases "(snd s, x')" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def split: option.split_asm)
subgoal by(cases "(snd s, projl (projr x))" rule: lazy_channel_send.cases)(auto simp add: vld_def in_nlists_UNIV)
subgoal by(cases "(snd s, ())" rule: lazy_channel_recv_f.cases)(auto 4 3 split: option.split_asm if_split_asm cstate.split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def option.pred_set )
done
subgoal for s
apply(clarsimp simp add: ℐ_def; intro conjI WT_calleeI; clarsimp simp add: lazy_channel_insec'_def lazy_channel_send'_def lazy_channel_recv_f'_def)
subgoal for _ _ _ _ x
by(cases "(snd s, x)" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def ran_def split: option.split_asm)
subgoal by(cases "(snd s, ())" rule: lazy_channel_recv_f.cases)(auto 4 3 split: option.split_asm if_split_asm cstate.split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def)
done
done
then have "exec_gpv ?orc_lft ?𝒜 (False, Void, None, Map.empty) = exec_gpv ?orc_lft 𝒜 (False, Void, None, Map.empty)"
using WT by(rule callee_invariant_on.exec_gpv_mk_lossless_gpv) simp
also have "callee_invariant_on (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv') ?I ℐ"
apply(unfold_locales)
subgoal for s x y s'
supply [[simproc del: defined_all]]
apply(clarsimp simp add: ℐ_def; elim PlusE; clarsimp simp add: lazy_channel_insec'_def lazy_channel_send'_def lazy_channel_recv'_def)
subgoal for _ _ _ _ x'
by(cases "(snd s, x')" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def split: option.split_asm)
subgoal by(cases "(snd s, projl (projr x))" rule: lazy_channel_send.cases)(auto simp add: vld_def in_nlists_UNIV)
subgoal by(cases "(snd s, ())" rule: lazy_channel_recv.cases)(auto 4 3 split: option.split_asm if_split_asm cstate.split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def option.pred_set )
done
subgoal for s
apply(clarsimp simp add: ℐ_def; intro conjI WT_calleeI; clarsimp simp add: lazy_channel_insec'_def lazy_channel_send'_def lazy_channel_recv'_def)
subgoal for _ _ _ _ x
by(cases "(snd s, x)" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def ran_def split: option.split_asm)
subgoal by(cases "(snd s, ())" rule: lazy_channel_recv.cases)(auto 4 3 split: option.split_asm if_split_asm cstate.split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def)
done
done
then have "exec_gpv ?orc_rgt ?𝒜 (False, Void, None, Map.empty) = exec_gpv ?orc_rgt 𝒜 (False, Void, None, Map.empty)"
using WT by(rule callee_invariant_on.exec_gpv_mk_lossless_gpv) simp
finally have "¦Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. fst x}
- Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv')) {x. fst x}¦
≤ Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. snd x}"
unfolding game_def
by - (rule fundamental_lemma[where ?bad2.0="snd"]; auto simp add: spmf_rel_map map_spmf_conv_bind_spmf[symmetric] split_def)
moreover have "Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. fst x} = spmf ?L True"
unfolding game_def
by(auto simp add: map_spmf_conv_bind_spmf exec_gpv_resource_of_oracle connect_def spmf_conv_measure_spmf)
(auto simp add: rel_pred_def intro!: rel_spmf_bind_reflI measure_spmf_parametric[where A="λl r. fst l ⟷ r", THEN rel_funD, THEN rel_funD])
moreover have "spmf ?R True = Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv')) {x. fst x}"
unfolding game_def
by(auto simp add: map_spmf_conv_bind_spmf exec_gpv_resource_of_oracle connect_def spmf_conv_measure_spmf)
(auto simp add: rel_pred_def intro!: rel_spmf_bind_reflI measure_spmf_parametric[where A="λl r. l ⟷ fst r", THEN rel_funD, THEN rel_funD])
ultimately show ?thesis by simp
qed
have fact3: "spmf (connect 𝒜 (RES (lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv') (False, Void, None, Map.empty))) True
= spmf (connect 𝒜 (RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv) (Void, None, Map.empty))) True"
proof -
let ?orc_lft = "lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv'"
let ?orc_rgt = "lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv"
have[simp]: "rel_spmf (rel_prod (=) (λx y. y = snd x))
(lazy_channel_insec' (flg, s) q) (lazy_channel_insec s q)" for s flg q
by (cases s) (simp add: lazy_channel_insec'_def spmf_rel_map rel_prod_sel split_def option.rel_refl pmf.rel_refl split:option.split)
have[simp]: "rel_spmf (rel_prod (=) (λx y. y = snd x))
(lazy_channel_send' (flg, s) q) (lazy_channel_send s q)" for s flg q
by(cases "(s, q)" rule: lazy_channel_send.cases)(auto simp add: spmf_rel_map map_spmf_conv_bind_spmf split_def lazy_channel_send'_def)
have[simp]: "rel_spmf (rel_prod (=) (λx y. y = snd x))
(lazy_channel_recv' (flg, s) q) (lazy_channel_recv s q)" for s flg q
by(cases "(s, q)" rule: lazy_channel_recv.cases)(auto simp add: lazy_channel_recv'_def rel_spmf_bind_reflI split:option.split cstate.split)
have[simp]: "rel_spmf (rel_prod (=) (λx y. y = snd x))
((lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv') (flg, ams, es, as) query)
((lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv) (ams, es, as) query)" for flg ams es as query
proof (cases query)
case (Inl adv_query)
then show ?thesis
by(auto simp add: spmf_rel_map map_spmf_conv_bind_spmf[symmetric] apfst_def map_prod_def split_beta intro: rel_spmf_mono[where A="rel_prod (=) (λx y. y = snd x)"])
next
case (Inr query')
note Snd_Rcv = this
then show ?thesis
by (cases query', auto simp add: spmf_rel_map map_spmf_conv_bind_spmf[symmetric] split_beta)
((rule rel_spmf_mono[where A="rel_prod (=) (λx y. y = snd x)"]); auto)+
qed
have[simp]: "rel_spmf (λx y. fst x = fst y)
(exec_gpv ?orc_lft 𝒜 (False, Void, None, Map.empty)) (exec_gpv ?orc_rgt 𝒜 (Void, None, Map.empty))"
by(rule rel_spmf_mono[where A="rel_prod (=) (λx y. y = snd x)"])
(auto simp add: gpv.rel_eq split_def intro!: rel_funI
exec_gpv_parametric[where CALL="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD])
show ?thesis
unfolding map_spmf_conv_bind_spmf exec_gpv_resource_of_oracle connect_def spmf_conv_measure_spmf
by(rule measure_spmf_parametric[where A="(=)", THEN rel_funD, THEN rel_funD])
(auto simp add: rel_pred_def spmf_rel_map map_spmf_conv_bind_spmf[symmetric] gpv.rel_eq split_def intro!: rel_funI)
qed
have fact4: "Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. snd x} ≤ q / real (2 ^ η)"
proof -
let ?orc_sum = "lazy_channel_insec' ⊕⇩O lazy_channel_send' ⊕⇩O lazy_channel_recv_f'"
have "Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. snd x}
= spmf (map_spmf (fst ∘ snd) (exec_gpv ?orc_sum 𝒜 (False, Void, None, Map.empty))) True"
unfolding game_def
by (simp add: split_def map_spmf_conv_bind_spmf[symmetric] measure_map_spmf)
(simp add: spmf_conv_measure_spmf measure_map_spmf vimage_def)
also have "… ≤ (1 / real (card (nlists (UNIV :: bool set) η))) * real q"
proof -
have *: "spmf (map_spmf (fst ∘ snd) (?orc_sum (False, ams, es, as) query)) True
≤ 1 / real (card (nlists (UNIV :: bool set) η))" for ams es as query
proof (cases query)
case (Inl adv_query)
then show ?thesis
by(cases "((ams, es, as), adv_query)" rule: lazy_channel_insec.cases)
(auto simp add: lazy_channel_insec'_def rnd_def map_spmf_conv_bind_spmf bind_spmf_const split: option.split)
next
case (Inr query')
note Snd_Rcv = this
then show ?thesis
proof (cases query')
case (Inr rcv_query)
with Snd_Rcv show ?thesis
by (cases ams, auto simp add: lazy_channel_recv_f'_def map_spmf_conv_bind_spmf split_def split:option.split)
(auto simp add: spmf_of_set map_spmf_conv_bind_spmf[symmetric] rnd_def spmf_map vimage_def spmf_conv_measure_spmf[symmetric] split: split_indicator)
qed (cases ams, simp_all add: lazy_channel_send'_def)
qed
show ?thesis by (rule oi_True.interaction_bounded_by_exec_gpv_bad[where bad="fst"]) (auto simp add: * assms)
qed
also have "... = 1 / real (2 ^ η) * real q" by (simp add: card_nlists)
finally show ?thesis by simp
qed
have "?LHS ≤ Sigma_Algebra.measure (measure_spmf (game 𝒜 lazy_channel_recv_f')) {x. snd x}"
using fact1 fact2 fact3 by arith
also note fact4
finally show ?thesis .
qed
private inductive S' :: "(((bool list × bool list) option + unit) × unit × bool list cstate) spmf ⇒
(bool list cstate × (bool list × bool list) option × (bool list ⇒ bool list option)) spmf ⇒ bool" where
"S' (return_spmf (Inl None, (), Void))
(return_spmf (Void, None, Map.empty))"
| "S' (return_spmf (Inl None, (), Store m))
(return_spmf (Store m, None, Map.empty))"
if "length m = id' η"
| "S' (return_spmf (Inr (), (), Collect m))
(return_spmf (Collect m, None, Map.empty))"
if "length m = id' η"
| "S' (return_spmf (Inl (Some (a, m)), (), Store m))
(return_spmf (Store m, None, [m ↦ a]))"
if "length m = id' η"
| "S' (return_spmf (Inr (), (), Collect m))
(return_spmf (Collect m, None, [m ↦ a]))"
if "length m = id' η"
| "S' (return_spmf (Inr (), (), Fail))
(return_spmf (Fail, None, Map.empty))"
| "S' (return_spmf (Inr (), (), Fail))
(return_spmf (Fail, None, [m ↦ x]))"
if "length m = id' η"
| "S' (return_spmf (Inr (), (), Void))
(return_spmf (Collect m', Some (a', m'), Map.empty))"
if "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inr (), (), Fail))
(return_spmf (Collect m', Some (a', m'), Map.empty))"
if "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inr (), (), Store m))
(return_spmf (Collect m', Some (a', m'), Map.empty))"
if "length m = id' η" and "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inl (Some (a', m')), (), Collect m'))
(return_spmf (Collect m', Some (a', m'), [m' ↦ a']))"
if "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inl None, (), cstate.Collect m))
(return_spmf (cstate.Collect m, None, Map.empty))"
if "length m = id' η"
| "S' (return_spmf (Inl None, (), cstate.Fail))
(return_spmf (cstate.Fail, None, Map.empty))"
| "S' (return_spmf (Inr (), (), Fail))
(return_spmf (Collect m', Some (a', m'), [m ↦ a]))"
if "length m = id' η" and "length m' = id' η" and "length a' = id' η" and "m ≠ m'"
| "S' (return_spmf (Inr (), (), Fail))
(return_spmf (Collect m', Some (a', m'), [m ↦ a]))"
if "length m = id' η" and "length m' = id' η" and "length a' = id' η" and "a ≠ a'"
| "S' (return_spmf (Inl None, (), Collect m'))
(return_spmf (Collect m', Some (a', m'), [m' ↦ a']))"
if "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inr (), (), Collect m'))
(return_spmf (Collect m', Some (a', m'), [m' ↦ a']))"
if "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inr (), (), Void))
(map_spmf (λa'. (Fail, None, [m' ↦ a'])) (spmf_of_set (nlists UNIV η)))"
if "length m' = id' η"
| "S' (return_spmf (Inr (), (), Fail))
(map_spmf (λa'. (Fail, None, [m' ↦ a'])) (spmf_of_set (nlists UNIV η)))"
if "length m' = id' η"
| "S' (return_spmf (Inr (), (), Store m))
(map_spmf (λa'. (Fail, None, [m' ↦ a'])) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η" and "length m' = id' η"
| "S' (return_spmf (Inr (), (), Fail))
(map_spmf (λa'. (Fail, None, [m ↦ a, m' ↦ a'])) (spmf_of_set (nlists UNIV η)))"
if "length m = id' η" and "length m' = id' η" and "m ≠ m'"
| "S' (return_spmf (Inl (Some (a', m')), (), Fail))
(return_spmf (Fail, None, [m' ↦ a']))"
if "length m' = id' η" and "length a' = id' η"
| "S' (return_spmf (Inl None, (), Fail))
(return_spmf (Fail, None, [m' ↦ a']))"
if "length m' = id' η" and "length a' = id' η"
private lemma trace_eq_sim:
shows "(valid_insecQ <+> nlists UNIV (id' η) <+> UNIV) ⊢⇩R
RES (callee_auth_channel sim ⊕⇩O ††channel.send_oracle ⊕⇩O ††channel.recv_oracle) (Inl None, (), Void)
≈
RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f) (Void, None, Map.empty)"
(is "?A ⊢⇩R RES (?L1 ⊕⇩O ?L2 ⊕⇩O ?L3) ?SL ≈ RES (?R1 ⊕⇩O ?R2 ⊕⇩O ?R3) ?SR")
proof -
note [simp] =
spmf.map_comp o_def map_bind_spmf bind_map_spmf bind_spmf_const exec_gpv_bind
auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps
rorc_channel_send_def rorc_channel_recv_def rnd_def
have *: "?A ⊢⇩C ?L1 ⊕⇩O ?L2 ⊕⇩O ?L3(?SL) ≈ ?R1 ⊕⇩O ?R2 ⊕⇩O ?R3(?SR)"
proof(rule trace'_eqI_sim[where S=S'], goal_cases Init_OK Output_OK State_OK)
case Init_OK
then show ?case by (rule S'.intros)
next
case (Output_OK p q query)
show ?case
proof (cases query)
case (Inl adv_query)
with Output_OK show ?thesis
proof (cases adv_query)
case (ForwardOrEdit foe)
with Output_OK Inl show ?thesis
proof (cases foe)
case (Some am')
obtain a' m' where "am' = (a', m')" by (cases am') simp
with Output_OK Inl ForwardOrEdit Some show ?thesis
by cases (simp_all add: id'_def)
qed (erule S'.cases, simp_all add: id'_def)
qed (erule S'.cases, simp_all add: id'_def)+
next
case (Inr query')
with Output_OK show ?thesis by (cases; cases query') (simp_all)
qed
next
case (State_OK p q query state answer state')
show ?case
proof (cases query)
case (Inl adv_query)
show ?thesis
proof (cases adv_query)
case Look
with State_OK Inl show ?thesis
proof cases
case (2 m)
have "S' (return_spmf (Inl (Some (x, m)), (), Store m)) (return_spmf (Store m, None, [m ↦ x]))" for x
by (rule S'.intros) (simp only: 2)
with 2 show ?thesis using State_OK(2-) Inl Look
by clarsimp (simp add: cond_spmf_spmf_of_set spmf_of_set_singleton map_spmf_conv_bind_spmf[symmetric]
split_beta cond_spmf_fst_def image_def vimage_def id'_def)
qed (auto simp add: map_spmf_const[symmetric] map_spmf_conv_bind_spmf[symmetric] image_def intro: S'.intros; simp add: id'_def)+
next
case (ForwardOrEdit foe)
show ?thesis
proof (cases foe)
case None
with State_OK Inl ForwardOrEdit show ?thesis
by cases(auto simp add: map_spmf_const[symmetric] map_spmf_conv_bind_spmf[symmetric] image_def S'.intros)
next
case (Some am')
obtain a' m' where [simp]: "am' = (a', m')" by (cases am')
from State_OK Inl ForwardOrEdit Some show ?thesis
proof cases
case (4 m a)
then show ?thesis using State_OK(2-) Inl ForwardOrEdit Some
by (auto simp add: if_distrib_exec_gpv if_distrib_map_spmf split_def image_def if_distrib[symmetric] intro: S'.intros cong: if_cong)
qed (auto simp add: map_spmf_const[symmetric] map_spmf_conv_bind_spmf[symmetric] image_def intro:S'.intros)
qed
next
case Drop
with State_OK Inl show ?thesis
by cases (auto simp add: map_spmf_const[symmetric] map_spmf_conv_bind_spmf[symmetric] image_def intro:S'.intros; simp add: id'_def)+
qed
next
case Snd_Rcv: (Inr query')
with State_OK show ?thesis
by(cases; cases query')
(auto simp add: map_spmf_const[symmetric] map_spmf_conv_bind_spmf[symmetric] image_def;
(rule S'.intros; simp add: in_nlists_UNIV id'_def))+
qed
qed
from * show ?thesis by simp
qed
private lemma real_resource_wiring: "macode.res (rnd η) (mac η) =
RES (††insec_channel.insec_oracle ⊕⇩O rorc_channel_send ⊕⇩O rorc_channel_recv) ((False, ()), Map.empty, Void)"
(is "?L = ?R") including lifting_syntax
proof -
have *: "(λx y. map_spmf (map_prod id lprodr) ((A ⊕⇩O B) (rprodl x) y))
= (λx yl. map_spmf (λp. ((), lprodr (snd p))) (A (rprodl x) yl)) ⊕⇩O
(λx yr. map_spmf (λp. (fst p, lprodr (snd p))) (B (rprodl x) yr)) " for A B C
proof -
have aux: "map_prod id g ∘ apfst h = apfst h ∘ map_prod id g" for f g h by auto
show ?thesis
by (auto simp add: aux plus_oracle_def spmf.map_comp[where f="apfst _", symmetric]
spmf.map_comp[where f="map_prod id lprodr"] sum.case_distrib[where h="map_spmf _"] cong:sum.case_cong split!:sum.splits)
(subst plus_oracle_def[symmetric], simp add: map_prod_def split_def)
qed
have "?L = RES (††insec_channel.insec_oracle ⊕⇩O (rprodl ---> id ---> map_spmf (map_prod id lprodr))
(lift_state_oracle extend_state_oracle (attach_callee
(λs m. if s
then Done ((), True)
else do {
r ← Pause (Inl m) Done;
a ← lift_spmf (mac η (projl r) m);
_ ← Pause (Inr (a, m)) Done;
( Done ((), True))}) ((rorc.rnd_oracle (rnd η))† ⊕⇩O †channel.send_oracle)) ⊕⇩O
††(λs q. do {
(amo, s') ← †channel.recv_oracle s ();
case amo of
None ⇒ return_spmf (None, s')
| Some (a, m) ⇒ do {
(r, s'') ← (rorc.rnd_oracle (rnd η))† s' m;
a'← mac η r m;
return_spmf (if a' = a then Some m else None, s'')}}))) ((False, ()), Map.empty, Void)"
proof -
note[simp] = attach_CNV_RES attach_callee_parallel_intercept attach_stateless_callee
resource_of_oracle_rprodl Rel_def prod.rel_eq[symmetric] extend_state_oracle_plus_oracle[symmetric]
conv_callee_parallel[symmetric] conv_callee_parallel_id_left[where s="()", symmetric]
o_def bind_map_spmf exec_gpv_bind split_def option.case_distrib[where h="λgpv. exec_gpv _ gpv _"]
show ?thesis
unfolding channel.res_def rorc.res_def macode.res_def macode.routing_def
macode.πE_def macode.enm_def macode.dem_def interface_wiring
by (subst lift_state_oracle_extend_state_oracle | auto cong del: option.case_cong_weak intro: extend_state_oracle_parametric)+
qed
also have "... = ?R"
unfolding rorc_channel_send_def rorc_channel_recv_def extend_state_oracle_def
by(simp add: * split_def o_def map_fun_def spmf.map_comp extend_state_oracle_def lift_state_oracle_def
exec_gpv_bind if_distrib[where f="λgpv. exec_gpv _ gpv _"] cong: if_cong)
(simp add: split_def o_def rprodl_def Pair_fst_Unity bind_map_spmf map_spmf_bind_spmf
if_distrib[where f="map_spmf _"] option.case_distrib[where h="map_spmf _"] cong: if_cong option.case_cong)
finally show ?thesis .
qed
private lemma ideal_resource_wiring: "(CNV callee s) |⇩= 1⇩C ⊳ channel.res auth_channel.auth_oracle =
RES (callee_auth_channel callee ⊕⇩O ††channel.send_oracle ⊕⇩O ††channel.recv_oracle ) (s, (), Void)" (is "?L1 ⊳ _ = ?R")
proof -
have[simp]: "ℐ_full, ℐ_full ⊕⇩ℐ (ℐ_full ⊕⇩ℐ ℐ_full) ⊢⇩C ?L1 ∼ ?L1" (is "_, ?I ⊢⇩C _ ∼ _")
by(rule eq_ℐ_converter_mono)
(rule parallel_converter2_eq_ℐ_cong eq_ℐ_converter_reflI WT_converter_ℐ_full ℐ_full_le_plus_ℐ order_refl plus_ℐ_mono)+
have[simp]: "?I ⊢c (auth_channel.auth_oracle ⊕⇩O channel.send_oracle ⊕⇩O channel.recv_oracle) s √" for s
by(rule WT_plus_oracleI WT_parallel_oracle WT_callee_full; (unfold split_paired_all)?)+
have[simp]: "?L1 ⊳ RES (auth_channel.auth_oracle ⊕⇩O channel.send_oracle ⊕⇩O channel.recv_oracle) Void = ?R"
by(simp add: conv_callee_parallel_id_right[where s'="()", symmetric] attach_CNV_RES
attach_callee_parallel_intercept resource_of_oracle_rprodl extend_state_oracle_plus_oracle)
show ?thesis unfolding channel.res_def
by (subst eq_ℐ_attach[OF WT_resource_of_oracle, where ℐ' = "?I" and conv="?L1" and conv'="?L1"]) simp_all
qed
lemma all_together:
defines "ℐ ≡ ℐ_uniform (Set.Collect (valid_mac_query η)) (insert None (Some ` (nlists UNIV η × nlists UNIV η))) ⊕⇩ℐ
(ℐ_uniform (vld η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` vld η)))"
assumes "η > 0"
and "interaction_bounded_by' (λ_. True) (𝒜 η) q"
and lossless: "plossless_gpv ℐ (𝒜 η)"
and WT: "ℐ ⊢g 𝒜 η √"
shows
"¦spmf (connect (𝒜 η) (CNV sim (Inl None) |⇩= 1⇩C ⊳ channel.res auth_channel.auth_oracle)) True -
spmf (connect (𝒜 η) (macode.res (rnd η) (mac η))) True¦ ≤ q / real (2 ^ η)"
proof -
have *: "∀a b. ma = Edit (a, b) ⟶ length a = η ∧ length b = η ⟹ valid_mac_query η ma" for ma a b
by(cases "(η, ma)" rule: valid_mac_query.cases)(auto simp add: vld_def in_nlists_UNIV)
have assm4_alt: "outs_gpv ℐ (𝒜 η) ⊆ valid_insecQ <+> nlists UNIV (id' η) <+> UNIV"
using assms(5)[THEN WT_gpv_outs_gpv] unfolding id'_def
by(rule ord_le_eq_trans) (auto simp add: * split: aquery.split option.split simp add: in_nlists_UNIV vld_def ℐ_def)
have "callee_invariant_on (callee_auth_channel sim ⊕⇩O ††channel.send_oracle ⊕⇩O ††channel.recv_oracle)
(λ(s1, _, s3). (∀x y. s1 = Inl (Some (x, y)) ⟶ length x = η ∧ length y = η) ∧ pred_cstate (λx. length x = η) s3) ℐ"
apply unfold_locales
subgoal for s x y s'
apply(cases "(fst s, projl x)" rule: sim.cases; cases "snd (snd s)")
apply(fastforce simp: channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce simp: auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(auto split: if_split_asm simp add: exec_gpv_bind auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(auto split: if_split_asm simp add: auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)[1]
apply(fastforce split: if_split_asm simp add: exec_gpv_bind auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)+
done
subgoal for s
apply(rule WT_calleeI)
subgoal for x
by(cases "(fst s, projl x)" rule: sim.cases; cases "snd (snd s)")
(auto split: if_split_asm simp add: exec_gpv_bind auth_channel.auth_oracle.simps channel.send_oracle.simps channel.recv_oracle.simps vld_def in_nlists_UNIV ℐ_def)
done
done
then have WT1: "ℐ ⊢res RES (callee_auth_channel sim ⊕⇩O ††channel.send_oracle ⊕⇩O ††channel.recv_oracle) (Inl None, (), Void) √"
by(rule callee_invariant_on.WT_resource_of_oracle) simp
have "callee_invariant_on (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f)
(λ(s1, s2, s3). pred_cstate (λx. length x = η) s1 ∧ pred_option (λ(x, y). length x = η ∧ length y = η) s2 ∧ ran s3 ⊆ nlists UNIV η)
ℐ"
apply unfold_locales
subgoal for s x y s'
using [[simproc del: defined_all]] apply(clarsimp simp add: ℐ_def; elim PlusE; clarsimp)
subgoal for _ _ _ x'
by(cases "(s, x')" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def split: option.split_asm)
subgoal by(cases "(s, projl (projr x))" rule: lazy_channel_send.cases)(auto simp add: vld_def in_nlists_UNIV)
subgoal by(cases "(s, ())" rule: lazy_channel_recv_f.cases)(auto 4 3 split: option.split_asm if_split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def)
done
subgoal for s
apply(clarsimp simp add: ℐ_def; intro conjI WT_calleeI; clarsimp)
subgoal for _ _ _ x
by(cases "(s, x)" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def ran_def split: option.split_asm)
subgoal by(cases "(s, ())" rule: lazy_channel_recv_f.cases)(auto 4 3 split: option.split_asm if_split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def)
done
done
then have WT2: "ℐ ⊢res RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv_f) (Void, None, Map.empty) √"
by(rule callee_invariant_on.WT_resource_of_oracle) simp
have "callee_invariant_on (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv)
(λ(s1, s2, s3). pred_cstate (λx. length x = η) s1 ∧ pred_option (λ(x, y). length x = η ∧ length y = η) s2 ∧ ran s3 ⊆ nlists UNIV η)
ℐ"
apply unfold_locales
subgoal for s x y s'
using [[simproc del: defined_all]] apply(clarsimp simp add: ℐ_def; elim PlusE; clarsimp)
subgoal for _ _ _ x'
by(cases "(s, x')" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def split: option.split_asm)
subgoal by(cases "(s, projl (projr x))" rule: lazy_channel_send.cases)(auto simp add: vld_def in_nlists_UNIV)
subgoal by(cases "(s, ())" rule: lazy_channel_recv.cases)(auto 4 3 split: option.split_asm if_split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def option.pred_set)
done
subgoal for s
apply(clarsimp simp add: ℐ_def; intro conjI WT_calleeI; clarsimp)
subgoal for _ _ _ x
by(cases "(s, x)" rule: lazy_channel_insec.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def ran_def split: option.split_asm)
subgoal by(cases "(s, ())" rule: lazy_channel_recv_f.cases)(auto 4 3 split: option.split_asm if_split_asm simp add: in_nlists_UNIV vld_def ran_def rnd_def)
done
done
then have WT3: "ℐ ⊢res RES (lazy_channel_insec ⊕⇩O lazy_channel_send ⊕⇩O lazy_channel_recv) (Void, None, Map.empty) √"
by(rule callee_invariant_on.WT_resource_of_oracle) simp
have "callee_invariant_on (††insec_channel.insec_oracle ⊕⇩O rorc_channel_send ⊕⇩O rorc_channel_recv)
(λ(_, m, s). ran m ⊆ nlists UNIV η ∧ pred_cstate (λ(x, y). length x = η ∧ length y = η) s) ℐ"
apply(unfold_locales)
subgoal for s x y s'
using [[simproc del: defined_all]] apply(clarsimp simp add: ℐ_def; elim PlusE; clarsimp)
subgoal for _ _ _ x'
by(cases "(snd (snd s), x')" rule: insec_channel.insec_oracle.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def insec_channel.insec_oracle.simps split: option.split_asm)
subgoal
by(cases "snd (snd s)")
(auto 4 3 simp add: channel.send_oracle.simps rorc_channel_send_def rorc.rnd_oracle.simps in_nlists_UNIV rnd_def vld_def mac_def ran_def split: option.split_asm if_split_asm)
subgoal
by(cases "snd (snd s)")
(auto 4 4 simp add: rorc_channel_recv_def channel.recv_oracle.simps rorc.rnd_oracle.simps rnd_def mac_def ran_def iff: in_nlists_UNIV split: option.split_asm if_split_asm)
done
subgoal for s
apply(clarsimp simp add: ℐ_def; intro conjI WT_calleeI; clarsimp)
subgoal for _ _ _ x'
by(cases "(snd (snd s), x')" rule: insec_channel.insec_oracle.cases)
(auto simp add: vld_def in_nlists_UNIV rnd_def insec_channel.insec_oracle.simps split: option.split_asm)
subgoal
by(cases "snd (snd s)")
(auto simp add: rorc_channel_recv_def channel.recv_oracle.simps rorc.rnd_oracle.simps rnd_def mac_def vld_def ran_def iff: in_nlists_UNIV split: option.split_asm if_split_asm)
done
done
then have WT4: "ℐ ⊢res RES (††insec_channel.insec_oracle ⊕⇩O rorc_channel_send ⊕⇩O rorc_channel_recv) ((False, ()), Map.empty, Void) √"
by(rule callee_invariant_on.WT_resource_of_oracle) simp
note game_difference[OF assms(3), folded ℐ_def, OF assms(4,5)]
also note connect_cong_trace[OF trace_eq_sim WT assm4_alt WT1 WT2, symmetric]
also note connect_cong_trace[OF trace_eq_lazy, OF assms(2), OF WT assm4_alt WT3 WT4]
also note ideal_resource_wiring[of sim, of "Inl None", symmetric]
also note real_resource_wiring[symmetric]
finally show ?thesis by simp
qed
end
context begin
interpretation MAC: macode "rnd η" "mac η" for η .
interpretation A_CHAN: auth_channel .
lemma WT_enm:
"X ≠ {} ⟹ ℐ_uniform (vld η) UNIV, ℐ_uniform (vld η) X ⊕⇩ℐ ℐ_uniform (X × vld η) UNIV ⊢⇩C MAC.enm η √"
unfolding MAC.enm_def
by(rule WT_converter_of_callee) (auto simp add: mac_def)
lemma WT_dem: "ℐ_uniform UNIV (insert None (Some ` vld η)), ℐ_full ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` (nlists UNIV η × nlists UNIV η))) ⊢⇩C MAC.dem η √"
unfolding MAC.dem_def
by (rule WT_converter_of_callee) (auto simp add: vld_def stateless_callee_def mac_def split: option.split_asm)
lemma valid_insec_query_of [simp]: "valid_mac_query η (insec_query_of x)"
by(cases x) simp_all
lemma secure_mac:
defines "ℐ_real ≡ λη. ℐ_uniform {x. valid_mac_query η x} (insert None (Some ` (nlists UNIV η × nlists UNIV η)))"
and "ℐ_ideal ≡ λη. ℐ_uniform UNIV (insert None (Some ` nlists UNIV η))"
and "ℐ_common ≡ λη. ℐ_uniform (vld η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` vld η))"
shows
"constructive_security MAC.res (λ_. A_CHAN.res) (λ_. CNV sim (Inl None))
ℐ_real ℐ_ideal ℐ_common (λ_. enat q) True (λ_. insec_auth_wiring)"
proof
show WT_res [WT_intro]: "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res MAC.res η √" for η
proof -
let ?I = "pred_cstate (λ(x, y). length x = η ∧ length y = η)"
have *: "callee_invariant_on (MAC.RO.rnd_oracle η ⊕⇩O MAC.RO.rnd_oracle η) (λm. ran m ⊆ vld η) (ℐ_uniform (vld η) (vld η) ⊕⇩ℐ ℐ_full)" for η
apply unfold_locales
subgoal for s x y s' by(cases x; clarsimp split: option.split_asm; auto simp add: rnd_def vld_def)
subgoal by(clarsimp intro!: WT_calleeI split: option.split_asm; auto simp add: rnd_def in_nlists_UNIV vld_def ran_def)
done
have [WT_intro]: "ℐ_uniform (vld η) (vld η) ⊕⇩ℐ ℐ_full ⊢res MAC.RO.res η √" for η
unfolding MAC.RO.res_def by(rule callee_invariant_on.WT_resource_of_oracle[OF *]) simp
have [simp]: "ℐ_real η ⊢c MAC.INSEC.insec_oracle s √" if "?I s" for s
apply(rule WT_calleeI)
subgoal for x using that by(cases "(s, x)" rule: MAC.INSEC.insec_oracle.cases)(auto simp add: ℐ_real_def in_nlists_UNIV)
done
have [simp]: " ℐ_uniform UNIV (insert None (Some ` (nlists UNIV η × nlists UNIV η))) ⊢c A_CHAN.recv_oracle s √"
if "?I s" for s :: "(bool list × bool list) cstate" using that
by(cases s)(auto intro!: WT_calleeI simp add: in_nlists_UNIV)
have *: "callee_invariant_on (MAC.INSEC.insec_oracle ⊕⇩O A_CHAN.send_oracle ⊕⇩O A_CHAN.recv_oracle) ?I
(ℐ_real η ⊕⇩ℐ (ℐ_uniform (vld η × vld η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` (nlists UNIV η × nlists UNIV η)))))"
apply unfold_locales
subgoal for s x y s'
by(cases s; cases "(s, projl x)" rule: MAC.INSEC.insec_oracle.cases)(auto simp add: ℐ_real_def vld_def in_nlists_UNIV)
subgoal by(auto intro: WT_calleeI)
done
have [WT_intro]: "ℐ_real η ⊕⇩ℐ (ℐ_uniform (vld η × vld η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` (nlists UNIV η × nlists UNIV η)))) ⊢res MAC.INSEC.res √"
unfolding MAC.INSEC.res_def
by(rule callee_invariant_on.WT_resource_of_oracle[OF *]) simp
show ?thesis
unfolding ℐ_common_def MAC.res_def
by(rule WT_intro WT_enm[where X="vld η"] WT_dem | (simp add: vld_def; fail))+
qed
let ?I = "λη. pred_cstate (λx. length x = η)"
have WT_auth: "ℐ_uniform UNIV (insert None (Some ` nlists UNIV η)) ⊢c A_CHAN.auth_oracle s √"
if "?I η s" for η s
apply(rule WT_calleeI)
subgoal for x using that by(cases "(s, x)" rule: A_CHAN.auth_oracle.cases; auto simp add: in_nlists_UNIV)
done
have WT_recv: "ℐ_uniform UNIV (insert None (Some ` vld η)) ⊢c A_CHAN.recv_oracle s √"
if "?I η s" for η s using that
by(cases s)(auto intro!: WT_calleeI simp add: vld_def in_nlists_UNIV)
have *: "callee_invariant_on (A_CHAN.auth_oracle ⊕⇩O A_CHAN.send_oracle ⊕⇩O A_CHAN.recv_oracle)
(?I η) (ℐ_ideal η ⊕⇩ℐ ℐ_common η)" for η
apply(unfold_locales)
subgoal for s x y s'
by(cases "(s, projl x)" rule: A_CHAN.auth_oracle.cases; cases "projr x")(auto simp add: ℐ_common_def vld_def in_nlists_UNIV)
subgoal for s using WT_auth WT_recv by(auto simp add: ℐ_common_def ℐ_ideal_def intro: WT_calleeI)
done
show WT_auth: "ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢res A_CHAN.res √" for η
unfolding A_CHAN.res_def by(rule callee_invariant_on.WT_resource_of_oracle[OF *]) simp
let ?I_sim = "λη (s :: (bool list × bool list) option + unit). ∀x y. s = Inl (Some (x, y)) ⟶ length x = η ∧ length y = η"
have "ℐ_real η, ℐ_ideal η ⊢⇩C CNV sim s √" if "?I_sim η s" for η s using that
apply(coinduction arbitrary: s)
subgoal for q r conv' s by(cases "(s, q)" rule: sim.cases)(auto simp add: ℐ_real_def ℐ_ideal_def vld_def in_nlists_UNIV)
done
then show [WT_intro]: "ℐ_real η, ℐ_ideal η ⊢⇩C CNV sim (Inl None) √" for η by simp
{ fix 𝒜 :: "security ⇒ ((bool list × bool list) insec_query + bool list + unit, (bool list × bool list) option + unit + bool list option) distinguisher"
assume WT: "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g 𝒜 η √" for η
assume bounded[simplified]: "interaction_bounded_by' (λ_. True) (𝒜 η) q" for η
assume lossless[simplified]: "True ⟹ plossless_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (𝒜 η)" for η
show "negligible (λη. advantage (𝒜 η) (CNV sim (Inl None) |⇩= 1⇩C ⊳ A_CHAN.res) (MAC.res η))"
proof -
have f1: "negligible (λη. q * (1 / real (2 ^ η)))" (is "negligible ?ov")
by(rule negligible_poly_times[where n=0]) (simp add: negligible_inverse_powerI)+
have f2: "(λη. spmf (connect (𝒜 η) (CNV sim (Inl None) |⇩= 1⇩C ⊳ A_CHAN.res)) True -
spmf (connect (𝒜 η) (MAC.res η)) True) ∈ O(?ov)" (is "?L ∈ _")
by (auto simp add: bigo_def intro!: all_together[simplified] bounded eventually_at_top_linorderI[where c=1]
exI[where x=1] lossless[unfolded ℐ_real_def ℐ_common_def] WT[unfolded ℐ_real_def ℐ_common_def])
have "negligible ?L" using f1 f2 by (rule negligible_mono[of "?ov"])
then show ?thesis by (simp add: advantage_def)
qed
next
let ?cnv = "map_converter id id insec_query_of auth_response_of 1⇩C"
show "∃cnv. ∀𝒟. (∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √) ⟶
(∀η. interaction_bounded_by' (λ_. True) (𝒟 η) q) ⟶
(∀η. True ⟶ plossless_gpv (ℐ_ideal η ⊕⇩ℐ ℐ_common η) (𝒟 η)) ⟶
(∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (insec_query_of, map_option snd)) ∧
negligible (λη. advantage (𝒟 η) A_CHAN.res (cnv η |⇩= 1⇩C ⊳ MAC.res η))"
proof(intro exI[where x="λ_. ?cnv"] strip conjI)
fix 𝒟 :: "security ⇒ (auth_query + bool list + unit, bool list option + unit + bool list option) distinguisher"
assume WT_D [rule_format, WT_intro]: "∀η. ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢g 𝒟 η √"
let ?A = "λη. UNIV <+> nlists UNIV η <+> UNIV"
have WT1: "ℐ_ideal η, map_ℐ insec_query_of (map_option snd) (ℐ_real η) ⊢⇩C 1⇩C √" for η
using WT_converter_id order_refl by(rule WT_converter_mono)(auto simp add: le_ℐ_def ℐ_ideal_def ℐ_real_def)
have WT0: "ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢res map_converter id id insec_query_of (map_option snd) 1⇩C |⇩= 1⇩C ⊳ MAC.res η √" for η
by(rule WT1 WT_intro | simp)+
have WT2: "ℐ_ideal η, map_ℐ insec_query_of (map_option snd) (ℐ_real η) ⊢⇩C 1⇩C √" for η
using WT_converter_id order_refl
by(rule WT_converter_mono)(auto simp add: le_ℐ_def ℐ_ideal_def ℐ_real_def)
have WT_cnv: "ℐ_ideal η, ℐ_real η ⊢⇩C ?cnv √" for η
by(rule WT_converter_map_converter)(simp_all add: WT2)
from eq_ℐ_converter_reflI[OF this] this
show "wiring (ℐ_ideal η) (ℐ_real η) ?cnv insec_auth_wiring" for η ..
define res' :: "security ⇒ _ ⇒ auth_query + (bool list + bool list × bool list) + bool list + unit ⇒ _"
where "res' η =
map_fun id (map_fun insec_query_of (map_spmf (map_prod (map_option snd) id))) †MAC.INSEC.insec_oracle ⊕⇩O
((MAC.RO.rnd_oracle η)† ⊕⇩O †A_CHAN.send_oracle) ⊕⇩O (MAC.RO.rnd_oracle η)† ⊕⇩O †A_CHAN.recv_oracle"
for η
have push: "map_resource (map_sum f id) (map_sum g id) ((1⇩C |⇩= conv) ⊳ res) =
(1⇩C |⇩= conv) ⊳ map_resource (map_sum f id) (map_sum g id) res"
for f g conv res
proof -
have "map_resource (map_sum f id) (map_sum g id) ((1⇩C |⇩= conv) ⊳ res) = map_converter f g id id 1⇩C |⇩= conv ⊳ res"
by(simp add: attach_map_converter parallel_converter2_map1_out sum.map_id0)
also have "… = (1⇩C |⇩= conv) ⊳ map_resource (map_sum f id) (map_sum g id) res"
by(subst map_converter_id_move_right)(simp add: parallel_converter2_map1_out sum.map_id0 attach_map_converter)
finally show ?thesis .
qed
have res': "map_resource (map_sum insec_query_of id) (map_sum (map_option snd) id) (MAC.res η) =
1⇩C |⇩= MAC.enm η |⇩= MAC.dem η ⊳ RES (res' η) (Map.empty, Void)" for η
unfolding MAC.res_def MAC.RO.res_def MAC.INSEC.res_def interface_wiring push
by(simp add: parallel_converter2_map1_out sum.map_id0 attach_map_converter map_resource_resource_of_oracle map_sum_plus_oracle prod.map_id0 option.map_id0 map_fun_id res'_def)
define res'' :: "security ⇒ (unit × bool × unit) × (bool list ⇒ bool list option) × _ cstate ⇒ auth_query + bool list + unit ⇒ _"
where "res'' η = map_fun rprodl (map_fun id (map_spmf (map_prod id lprodr)))
(lift_state_oracle extend_state_oracle †(map_fun id (map_fun insec_query_of (map_spmf (map_prod (map_option snd) id))) †MAC.INSEC.insec_oracle) ⊕⇩O
†(map_fun rprodl (map_fun id (map_spmf (map_prod id lprodr)))
(lift_state_oracle extend_state_oracle
(attach_callee
(λbs m. if bs then Done ((), True) else Pause (Inl m) Done ⤜ (λr. lift_spmf (mac η (projl r) m) ⤜ (λa. Pause (Inr (a, m)) Done ⤜ (λ_. Done ((), True)))))
((MAC.RO.rnd_oracle η)† ⊕⇩O †A_CHAN.send_oracle)) ⊕⇩O
††(λs q. †A_CHAN.recv_oracle s () ⤜
(λx. case x of (None, s') ⇒ return_spmf (None, s')
| (Some (x1, x2a), s') ⇒ (MAC.RO.rnd_oracle η)† s' x2a ⤜ (λ(x, s'). mac η x x2a ⤜ (λy. return_spmf (if y = x1 then Some x2a else None, s'))))))))"
for η
have "?cnv |⇩= 1⇩C ⊳ MAC.res η = 1⇩C |⇩= MAC.enm η |⇩= MAC.dem η ⊳ RES (res' η) (Map.empty, Void)" for η
by(simp add: parallel_converter2_map1_out attach_map_converter sum.map_id0 res' attach_compose[symmetric] comp_converter_parallel2 comp_converter_id_left)
also have "… η = RES (res'' η) (((), False, ()), Map.empty, Void)" for η
unfolding MAC.enm_def MAC.dem_def conv_callee_parallel[symmetric] conv_callee_parallel_id_left[where s="()", symmetric] attach_CNV_RES
unfolding res'_def res''_def attach_callee_parallel_intercept attach_stateless_callee attach_callee_id_oracle prod.rel_eq[symmetric]
by(simp add: extend_state_oracle_plus_oracle[symmetric] rprodl_extend_state_oracle sum.case_distrib[where h="λx. exec_gpv _ x _"]
option.case_distrib[where h="λx. exec_gpv _ x _"] prod.case_distrib[where h="λx. exec_gpv _ x _"] exec_gpv_bind bind_map_spmf o_def
cong: sum.case_cong option.case_cong)
also
define S :: "security ⇒ bool list cstate ⇒ (unit × bool × unit) × (bool list ⇒ bool list option) × (bool list × bool list) cstate ⇒ bool"
where "S η l r = (case (l, r) of
(Void, ((_, False, _), m, Void)) ⇒ m = Map.empty
| (Store x, ((_, True, _), m, Store (y, z))) ⇒ length x = η ∧ length y = η ∧ length z = η ∧ m = [z ↦ y] ∧ x = z
| (Collect x, ((_, True, _), m, Collect (y, z))) ⇒ length x = η ∧ length y = η ∧ length z = η ∧ m = [z ↦ y] ∧ x = z
| (Fail, ((_, True, _), m, Fail)) ⇒ True
| _ ⇒ False)" for η l r
note [simp] = spmf_rel_map bind_map_spmf exec_gpv_bind
have "connect (𝒟 η) (?cnv |⇩= 1⇩C ⊳ MAC.res η) = connect (𝒟 η) A_CHAN.res" for η
unfolding calculation using WT_D _ WT_auth
apply(rule connect_eq_resource_cong[symmetric])
unfolding A_CHAN.res_def
apply(rule eq_resource_on_resource_of_oracleI[where S="S η"])
apply(rule rel_funI)+
subgoal for s s' q q'
by(cases q; cases "projl q"; cases "projr q"; clarsimp simp add: eq_on_def S_def res''_def split: cstate.split_asm bool.split_asm; clarsimp simp add: rel_spmf_return_spmf1 rnd_def mac_def bind_UNION ℐ_common_def vld_def in_nlists_UNIV S_def)+
subgoal by(simp add: S_def)
done
then show adv: "negligible (λη. advantage (𝒟 η) A_CHAN.res (?cnv |⇩= 1⇩C ⊳ MAC.res η))"
by(simp add: advantage_def)
qed
}
qed
end
end