diff --git a/thys/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy b/thys/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy --- a/thys/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy +++ b/thys/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy @@ -1,1258 +1,1269 @@ 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) \\<^sub>R RES (lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv) (Void, None, Map.empty) \ RES (\\insec_channel.insec_oracle \\<^sub>O rorc_channel_send \\<^sub>O rorc_channel_recv) ((False, ()), Map.empty, Void)" (is "?A \\<^sub>R RES (?L1 \\<^sub>O ?L2 \\<^sub>O ?L3) ?SL \ RES (?R1 \\<^sub>O ?R2 \\<^sub>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 \\<^sub>C ?L1 \\<^sub>O ?L2 \\<^sub>O ?L3(?SL) \ ?R1 \\<^sub>O ?R2 \\<^sub>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 \))) \\<^sub>\ (\_uniform (vld \) UNIV \\<^sub>\ \_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 \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv_f) (Void, None, Map.empty))) True - spmf (connect \ (RES (lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>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' \\<^sub>O lazy_channel_send' \\<^sub>O recv_oracle) \ (False, Void, None, Map.empty)); return_spmf (b, flg) })" have fact1: "spmf (connect \ (RES (lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv_f) (Void, None, Map.empty))) True = spmf (connect \ (RES (lazy_channel_insec' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv_f') (False, Void, None, Map.empty))) True" proof - let ?orc_lft = "lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv_f" let ?orc_rgt = "lazy_channel_insec' \\<^sub>O lazy_channel_send' \\<^sub>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 \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv_f) (ams, es, as) query) ((lazy_channel_insec' \\<^sub>O lazy_channel_send' \\<^sub>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' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv_f') (False, Void, None, Map.empty))) True - spmf (connect \ (RES (lazy_channel_insec' \\<^sub>O lazy_channel_send' \\<^sub>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' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv_f'" let ?orc_rgt = "lazy_channel_insec' \\<^sub>O lazy_channel_send' \\<^sub>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 \\<^sub>\ (\_uniform (vld \) UNIV \\<^sub>\ \_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' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv_f') ?I \" apply(unfold_locales) subgoal for s x y s' 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' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv') ?I \" apply(unfold_locales) subgoal for s x y s' 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' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv') (False, Void, None, Map.empty))) True = spmf (connect \ (RES (lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv) (Void, None, Map.empty))) True" proof - let ?orc_lft = "lazy_channel_insec' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv'" let ?orc_rgt = "lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>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' \\<^sub>O lazy_channel_send' \\<^sub>O lazy_channel_recv') (flg, ams, es, as) query) ((lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>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' \\<^sub>O lazy_channel_send' \\<^sub>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) \\<^sub>R RES (callee_auth_channel sim \\<^sub>O \\channel.send_oracle \\<^sub>O \\channel.recv_oracle) (Inl None, (), Void) \ RES (lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>O lazy_channel_recv_f) (Void, None, Map.empty)" (is "?A \\<^sub>R RES (?L1 \\<^sub>O ?L2 \\<^sub>O ?L3) ?SL \ RES (?R1 \\<^sub>O ?R2 \\<^sub>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 \\<^sub>C ?L1 \\<^sub>O ?L2 \\<^sub>O ?L3(?SL) \ ?R1 \\<^sub>O ?R2 \\<^sub>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 \\<^sub>O rorc_channel_send \\<^sub>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 \\<^sub>O B) (rprodl x) y)) = (\x yl. map_spmf (\p. ((), lprodr (snd p))) (A (rprodl x) yl)) \\<^sub>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 \\<^sub>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 \))\ \\<^sub>O \channel.send_oracle)) \\<^sub>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) |\<^sub>= 1\<^sub>C \ channel.res auth_channel.auth_oracle = RES (callee_auth_channel callee \\<^sub>O \\channel.send_oracle \\<^sub>O \\channel.recv_oracle ) (s, (), Void)" (is "?L1 \ _ = ?R") proof - have[simp]: "\_full, \_full \\<^sub>\ (\_full \\<^sub>\ \_full) \\<^sub>C ?L1 \ ?L1" (is "_, ?I \\<^sub>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 \\<^sub>O channel.send_oracle \\<^sub>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 \\<^sub>O channel.send_oracle \\<^sub>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 \))) \\<^sub>\ (\_uniform (vld \) UNIV \\<^sub>\ \_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) |\<^sub>= 1\<^sub>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 \\<^sub>O \\channel.send_oracle \\<^sub>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' - 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) + apply(cases "(fst s, projl x)" rule: sim.cases; cases "snd (snd s)") (*A MESS, but neither fastforce nor auto works for all 36 subgoals*) + 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 \\<^sub>O \\channel.send_oracle \\<^sub>O \\channel.recv_oracle) (Inl None, (), Void) \" by(rule callee_invariant_on.WT_resource_of_oracle) simp have "callee_invariant_on (lazy_channel_insec \\<^sub>O lazy_channel_send \\<^sub>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' 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 \\<^sub>O lazy_channel_send \\<^sub>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 \\<^sub>O lazy_channel_send \\<^sub>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' 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 \\<^sub>O lazy_channel_send \\<^sub>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 \\<^sub>O rorc_channel_send \\<^sub>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' 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 \\<^sub>O rorc_channel_send \\<^sub>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 \\<^sub>\ \_uniform (X \ vld \) UNIV \\<^sub>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 \\<^sub>\ \_uniform UNIV (insert None (Some ` (nlists UNIV \ \ nlists UNIV \))) \\<^sub>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 \\<^sub>\ \_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 \ \\<^sub>\ \_common \ \res MAC.res \ \" for \ proof - let ?I = "pred_cstate (\(x, y). length x = \ \ length y = \)" have *: "callee_invariant_on (MAC.RO.rnd_oracle \ \\<^sub>O MAC.RO.rnd_oracle \) (\m. ran m \ vld \) (\_uniform (vld \) (vld \) \\<^sub>\ \_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 \) \\<^sub>\ \_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 \\<^sub>O A_CHAN.send_oracle \\<^sub>O A_CHAN.recv_oracle) ?I (\_real \ \\<^sub>\ (\_uniform (vld \ \ vld \) UNIV \\<^sub>\ \_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 \ \\<^sub>\ (\_uniform (vld \ \ vld \) UNIV \\<^sub>\ \_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 \\<^sub>O A_CHAN.send_oracle \\<^sub>O A_CHAN.recv_oracle) (?I \) (\_ideal \ \\<^sub>\ \_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 \ \\<^sub>\ \_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 \ \\<^sub>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 \ \\<^sub>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 \ \\<^sub>\ \_common \ \g \ \ \" for \ assume bounded[simplified]: "interaction_bounded_by' (\_. True) (\ \) q" for \ assume lossless[simplified]: "True \ plossless_gpv (\_real \ \\<^sub>\ \_common \) (\ \)" for \ show "negligible (\\. advantage (\ \) (CNV sim (Inl None) |\<^sub>= 1\<^sub>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) |\<^sub>= 1\<^sub>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\<^sub>C" show "\cnv. \\. (\\. \_ideal \ \\<^sub>\ \_common \ \g \ \ \) \ (\\. interaction_bounded_by' (\_. True) (\ \) q) \ (\\. True \ plossless_gpv (\_ideal \ \\<^sub>\ \_common \) (\ \)) \ (\\. wiring (\_ideal \) (\_real \) (cnv \) (insec_query_of, map_option snd)) \ negligible (\\. advantage (\ \) A_CHAN.res (cnv \ |\<^sub>= 1\<^sub>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 \ \\<^sub>\ \_common \ \g \ \ \" let ?A = "\\. UNIV <+> nlists UNIV \ <+> UNIV" have WT1: "\_ideal \, map_\ insec_query_of (map_option snd) (\_real \) \\<^sub>C 1\<^sub>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 \ \\<^sub>\ \_common \ \res map_converter id id insec_query_of (map_option snd) 1\<^sub>C |\<^sub>= 1\<^sub>C \ MAC.res \ \" for \ by(rule WT1 WT_intro | simp)+ have WT2: "\_ideal \, map_\ insec_query_of (map_option snd) (\_real \) \\<^sub>C 1\<^sub>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 \ \\<^sub>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 \\<^sub>O ((MAC.RO.rnd_oracle \)\ \\<^sub>O \A_CHAN.send_oracle) \\<^sub>O (MAC.RO.rnd_oracle \)\ \\<^sub>O \A_CHAN.recv_oracle" for \ have push: "map_resource (map_sum f id) (map_sum g id) ((1\<^sub>C |\<^sub>= conv) \ res) = (1\<^sub>C |\<^sub>= 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\<^sub>C |\<^sub>= conv) \ res) = map_converter f g id id 1\<^sub>C |\<^sub>= conv \ res" by(simp add: attach_map_converter parallel_converter2_map1_out sum.map_id0) also have "\ = (1\<^sub>C |\<^sub>= 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\<^sub>C |\<^sub>= MAC.enm \ |\<^sub>= 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) \\<^sub>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 \)\ \\<^sub>O \A_CHAN.send_oracle)) \\<^sub>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 |\<^sub>= 1\<^sub>C \ MAC.res \ = 1\<^sub>C |\<^sub>= MAC.enm \ |\<^sub>= 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 |\<^sub>= 1\<^sub>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 |\<^sub>= 1\<^sub>C \ MAC.res \))" by(simp add: advantage_def) qed } qed end end diff --git a/thys/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy b/thys/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy --- a/thys/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy +++ b/thys/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy @@ -1,130 +1,130 @@ section \Secure composition: Encrypt then MAC\ theory Secure_Channel imports One_Time_Pad Message_Authentication_Code begin context begin interpretation INSEC: insec_channel . interpretation MAC: macode "rnd \" "mac \" for \ . interpretation AUTH: auth_channel . interpretation CIPHER: cipher "key \" "enc \" "dec \" for \ . interpretation SEC: sec_channel . lemma plossless_enc [plossless_intro]: "plossless_converter (\_uniform (nlists UNIV \) UNIV) (\_uniform UNIV (nlists UNIV \) \\<^sub>\ \_uniform (nlists UNIV \) UNIV) (CIPHER.enc \)" unfolding CIPHER.enc_def by(rule plossless_converter_of_callee) (auto simp add: stateless_callee_def enc_def in_nlists_UNIV) lemma plossless_dec [plossless_intro]: "plossless_converter (\_uniform UNIV (insert None (Some ` nlists UNIV \))) (\_uniform UNIV (nlists UNIV \) \\<^sub>\ \_uniform UNIV (insert None (Some ` nlists UNIV \))) (CIPHER.dec \)" unfolding CIPHER.dec_def by(rule plossless_converter_of_callee) (auto simp add: stateless_callee_def dec_def in_nlists_UNIV split: option.split) lemma callee_invariant_on_key_oracle: "callee_invariant_on (CIPHER.KEY.key_oracle \ \\<^sub>O CIPHER.KEY.key_oracle \) (\x. case x of None \ True | Some x' \ length x' = \) (\_uniform UNIV (nlists UNIV \) \\<^sub>\ \_full)" proof(unfold_locales, goal_cases) case (1 s x y s') then show ?case by(cases x; clarsimp split: option.splits; simp add: key_def in_nlists_UNIV) next case (2 s) then show ?case by(clarsimp intro!: WT_calleeI split: option.split_asm)(simp_all add: in_nlists_UNIV key_def) qed interpretation key: callee_invariant_on "CIPHER.KEY.key_oracle \ \\<^sub>O CIPHER.KEY.key_oracle \" "\x. case x of None \ True | Some x' \ length x' = \" "\_uniform UNIV (nlists UNIV \) \\<^sub>\ \_full" for \ by(rule callee_invariant_on_key_oracle) lemma WT_enc [WT_intro]: "\_uniform (nlists UNIV \) UNIV, \_uniform UNIV (nlists UNIV \) \\<^sub>\ \_uniform (vld \) UNIV \\<^sub>C CIPHER.enc \ \" unfolding CIPHER.enc_def by (rule WT_converter_of_callee) (simp_all add: stateless_callee_def vld_def enc_def in_nlists_UNIV) lemma WT_dec [WT_intro]: "\_uniform UNIV (insert None (Some ` nlists UNIV \)), \_uniform UNIV (nlists UNIV \) \\<^sub>\ \_uniform UNIV (insert None (Some ` vld \)) \\<^sub>C CIPHER.dec \ \" unfolding CIPHER.dec_def by(rule WT_converter_of_callee)(auto simp add: stateless_callee_def dec_def vld_def in_nlists_UNIV) lemma bound_enc [interaction_bound]: "interaction_any_bounded_converter (CIPHER.enc \) (enat 2)" unfolding CIPHER.enc_def by (rule interaction_any_bounded_converter_of_callee) (auto simp add: stateless_callee_def map_gpv_id_bind_gpv zero_enat_def one_enat_def) lemma bound_dec [interaction_bound]: "interaction_any_bounded_converter (CIPHER.dec \) (enat 2)" unfolding CIPHER.dec_def by (rule interaction_any_bounded_converter_of_callee) (auto simp add: stateless_callee_def map_gpv_id_bind_gpv zero_enat_def one_enat_def split: sum.split option.split) theorem mac_otp: defines "\_real \ \\. \_uniform {x. valid_mac_query \ x} UNIV" and "\_ideal \ \_. \_full" and "\_common \ \\. \_uniform (vld \) UNIV \\<^sub>\ \_full" shows "constructive_security (\\. 1\<^sub>C |\<^sub>= (CIPHER.enc \ |\<^sub>= CIPHER.dec \) \ parallel_wiring \ parallel_resource1_wiring \ CIPHER.KEY.res \ \ (1\<^sub>C |\<^sub>= MAC.enm \ |\<^sub>= MAC.dem \ \ 1\<^sub>C |\<^sub>= parallel_wiring \ parallel_resource1_wiring \ MAC.RO.res \ \ INSEC.res)) (\_. SEC.res) (\\. CNV Message_Authentication_Code.sim (Inl None) \ CNV One_Time_Pad.sim None) (\\. \_uniform (Set.Collect (valid_mac_query \)) (insert None (Some ` (nlists UNIV \ \ nlists UNIV \)))) (\\. \_uniform UNIV {None, Some \}) (\\. \_uniform (nlists UNIV \) UNIV \\<^sub>\ \_uniform UNIV (insert None (Some ` nlists UNIV \))) (\_. enat q) True (\\. (id, map_option length) \\<^sub>w (insec_query_of, map_option snd))" proof(rule composability[OF one_time_pad[THEN constructive_security2.constructive_security, unfolded CIPHER.res_alt_def comp_converter_parallel2 comp_converter_id_left] secure_mac[unfolded MAC.res_def, THEN constructive_security.parallel_resource1, THEN constructive_security.lifting], where ?\_res2="\\. \_uniform UNIV (nlists UNIV \) \\<^sub>\ \_uniform UNIV (nlists UNIV \)" and ?bound_conv1="\_. 2" and ?q3 = "2 * q" and bound_sim = "\_. \", simplified] , goal_cases) case (1 \) have [simp]: "\_uniform UNIV (nlists UNIV \) \c CIPHER.KEY.key_oracle \ s \" if "pred_option (\x. length x = \) s" for s \ apply(rule WT_calleeI) subgoal for call using that by(cases s; cases call; clarsimp; auto simp add: key_def in_nlists_UNIV) done have *: "callee_invariant_on (CIPHER.KEY.key_oracle \ \\<^sub>O CIPHER.KEY.key_oracle \) (pred_option (\x. length x = \)) (\_uniform UNIV (nlists UNIV \) \\<^sub>\ \_uniform UNIV (nlists UNIV \))" for \ apply(unfold_locales) subgoal for s x y s' by(cases s; cases x; clarsimp; auto simp add: key_def in_nlists_UNIV) subgoal for s by auto done then show ?case unfolding CIPHER.KEY.res_def by(rule callee_invariant_on.WT_resource_of_oracle) simp case (2 \) show ?case unfolding CIPHER.KEY.res_def apply(rule callee_invariant_on.lossless_resource_of_oracle[OF *]) subgoal for s x by(cases s; cases x)(auto split: plus_oracle_split; simp add: key_def)+ subgoal by simp done case (3 \) show ?case by(rule WT_intro)+ case (4 \) show ?case by interaction_bound_converter code_simp case (5 \) - show ?case by (simp add: max_def) (simp add: times_enat_def) + show ?case by (simp add: mult_2_right) case (6 \) show ?case unfolding vld_def by(rule plossless_intro WT_intro[unfolded vld_def])+ qed end end