Theory One_Time_Pad
section ‹Security of one-time-pad encryption›
theory One_Time_Pad imports
System_Construction
begin
definition key :: "security ⇒ bool list spmf" where
"key η ≡ spmf_of_set (nlists UNIV η)"
definition enc :: "security ⇒ bool list ⇒ bool list ⇒ bool list spmf" where
"enc η k m ≡ return_spmf (k [⊕] m)"
definition dec :: "security ⇒ bool list ⇒ bool list ⇒ bool list option" where
"dec η k c ≡ Some (k [⊕] c)"
definition sim :: "'b list option ⇒ 'a ⇒ ('b list option × 'b list option, 'a, nat option) gpv" where
"sim c q ≡ (do {
lo ← Pause q Done;
(case lo of
Some n ⇒ if c = None
then do {
x ← lift_spmf (spmf_of_set (nlists UNIV n));
Done (Some x, Some x)}
else Done (c, c)
| None ⇒ Done (None, c))})"
context
fixes η :: "security"
begin
private definition key_channel_send :: "bool list option × bool list cstate
⇒ bool list ⇒ (unit × bool list option × bool list cstate) spmf" where
"key_channel_send s m ≡ do {
(k, s) ← (key.key_oracle (key η))† s ();
c ← enc η k m;
(_, s) ← †channel.send_oracle s c;
return_spmf ((), s)}"
private definition key_channel_recv :: "bool list option × bool list cstate
⇒ 'a ⇒ (bool list option × bool list option × bool list cstate) spmf" where
"key_channel_recv s m ≡do {
(c, s) ← †channel.recv_oracle s ();
(case c of None ⇒ return_spmf (None, s)
| Some c' ⇒ do {
(k, s) ← (key.key_oracle (key η))† s ();
return_spmf (dec η k c', s)})}"
private abbreviation callee_sec_channel where
"callee_sec_channel callee ≡ lift_state_oracle extend_state_oracle (attach_callee callee sec_channel.sec_oracle)"
private inductive S :: "(bool list option × unit × bool list cstate) spmf ⇒
(bool list option × bool list cstate) spmf ⇒ bool" where
"S (return_spmf (None, (), Void))
(return_spmf (None, Void))"
| "S (return_spmf (None, (), Store plain))
(map_spmf (λkey. (Some key, Store (key [⊕] plain))) (spmf_of_set (nlists UNIV η)))"
if "length plain = id' η"
| "S (return_spmf (None, (), Collect plain))
(map_spmf (λkey. (Some key, Collect (key [⊕] plain))) (spmf_of_set (nlists UNIV η)))"
if "length plain = id' η"
| "S (return_spmf (Some (key [⊕] plain), (), Store plain))
(return_spmf (Some key, Store (key [⊕] plain)))"
if "length plain = id' η" "length key = id' η" for key
| "S (return_spmf (Some (key [⊕] plain), (), Collect plain))
(return_spmf (Some key, Collect (key [⊕] plain)))"
if "length plain = id' η" "length key = id' η" for key
| "S (return_spmf (None, (), Fail))
(map_spmf (λx. (Some x, Fail)) (spmf_of_set (nlists UNIV η)))"
| "S (return_spmf (Some (key [⊕] plain), (), Fail))
(return_spmf (Some key, Fail))"
if "length plain = id' η" "length key = id' η" for key plain
lemma resources_indistinguishable:
shows "(UNIV <+> nlists UNIV (id' η) <+> UNIV) ⊢⇩R
RES (callee_sec_channel sim ⊕⇩O ††channel.send_oracle ⊕⇩O ††channel.recv_oracle) (None :: bool list option, (), Void)
≈
RES (†auth_channel.auth_oracle ⊕⇩O key_channel_send ⊕⇩O key_channel_recv) (None :: bool list option, Void)"
(is "?A ⊢⇩R RES (?L1 ⊕⇩O ?L2 ⊕⇩O ?L3) ?SL ≈ RES (?R1 ⊕⇩O ?R2 ⊕⇩O ?R3) ?SR")
proof -
note [simp] =
exec_gpv_bind spmf.map_comp o_def map_bind_spmf bind_map_spmf bind_spmf_const
sec_channel.sec_oracle.simps auth_channel.auth_oracle.simps
channel.send_oracle.simps key_channel_send_def
channel.recv_oracle.simps key_channel_recv_def
key.key_oracle.simps dec_def key_def enc_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
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 adv_query)
case Look
with Output_OK Inl show ?thesis
proof cases
case Store_State_Channel: (2 plain)
have*: "length plain = id' η ⟹
map_spmf (λx. Inl (Some x)) (spmf_of_set (nlists UNIV (id' η))) =
map_spmf (λx. Inl (Some x)) (map_spmf (λx. x [⊕] plain) (spmf_of_set (nlists UNIV η)))" for η
unfolding id'_def by (subst xor_list_commute, subst one_time_pad[where xs=plain, symmetric]) simp_all
from Store_State_Channel show ?thesis using Output_OK(2-) Inl Look
by(simp add: sim_def, simp add: map_spmf_conv_bind_spmf[symmetric])
(subst (2) spmf.map_comp[where f="λx. Inl (Some x)", symmetric, unfolded o_def], simp only: *)
qed (auto simp add: sim_def)
qed (auto simp add: sim_def id'_def elim: S.cases)
next
case Snd_Rcv: (Inr query')
with Output_OK show ?thesis
proof (cases query')
case (Inr rcv_query)
with Output_OK Snd_Rcv show ?thesis
proof cases
case Collect_State_Channel: (3 plain)
then show ?thesis using Output_OK(2-) Snd_Rcv Inr
by (simp cong: bind_spmf_cong_simp add: in_nlists_UNIV id'_def)
qed simp_all
qed (auto elim: S.cases)
qed
next
case (State_OK p q query state answer state')
then show ?case
proof (cases query)
case (Inl adv_query)
with State_OK show ?thesis
proof (cases adv_query)
case Look
with State_OK Inl show ?thesis
proof cases
case Store_State_Channel: (2 plain)
have *: "length plain = id' η ⟹ key ∈ nlists UNIV η ⟹
S (cond_spmf_fst (map_spmf (λx. (Inl (Some x), Some x, (), Store plain))
(spmf_of_set (nlists UNIV (id' η)))) (Inl (Some (key [⊕] plain))))
(cond_spmf_fst (map_spmf (λx. (Inl (Some (x [⊕] plain)), Some x, Store (x [⊕] plain)))
(spmf_of_set (nlists UNIV η))) (Inl (Some (key [⊕] plain))))" for key
proof(subst (1 2) cond_spmf_fst_map_Pair1, goal_cases)
case 2
note inj_onD[OF inj_on_xor_list_nlists, rotated, simplified xor_list_commute]
with 2 show ?case
unfolding inj_on_def by (auto simp add: id'_def)
next
case 5
note inj_onD[OF inj_on_xor_list_nlists, rotated, simplified xor_list_commute]
with 5 show ?case
by (subst (1 2 3) inv_into_f_f)
((clarsimp simp add: inj_on_def), (auto simp add: S.simps id'_def inj_on_def in_nlists_UNIV ))
qed (simp_all add: id'_def in_nlists_UNIV min_def inj_on_def)
from Store_State_Channel show ?thesis using State_OK(2-) Inl Look
by (clarsimp simp add: sim_def) (simp add: map_spmf_conv_bind_spmf[symmetric] * )
qed (auto simp add: sim_def map_spmf_conv_bind_spmf[symmetric] S.simps)
qed (erule S.cases; (simp add: sim_def, auto simp add: map_spmf_conv_bind_spmf[symmetric] S.simps))+
next
case Snd_Rcv: (Inr query')
with State_OK show ?thesis
proof (cases query')
case (Inr rcv_query)
with State_OK Snd_Rcv show ?thesis
proof cases
case Collect_State_Channel: (3 plain)
then show ?thesis using State_OK(2-) Snd_Rcv Inr
by clarsimp (simp add: S.simps in_nlists_UNIV id'_def map_spmf_conv_bind_spmf[symmetric] cong: bind_spmf_cong_simp)
qed (simp add: sim_def, auto simp add: map_spmf_conv_bind_spmf[symmetric] S.simps)
qed (erule S.cases,
(simp add: sim_def, auto simp add: map_spmf_conv_bind_spmf[symmetric] S.simps in_nlists_UNIV))
qed
qed
from * show ?thesis by simp
qed
lemma real_resource_wiring:
shows "cipher.res (key η) (enc η) (dec η)
= RES (†auth_channel.auth_oracle ⊕⇩O key_channel_send ⊕⇩O key_channel_recv) (None, Void)"
including lifting_syntax
proof -
note[simp]= Rel_def prod.rel_eq[symmetric] split_def split_beta o_def exec_gpv_bind bind_map_spmf
resource_of_oracle_rprodl rprodl_extend_state_oracle
conv_callee_parallel[symmetric] extend_state_oracle_plus_oracle[symmetric]
attach_CNV_RES attach_callee_parallel_intercept attach_stateless_callee
show ?thesis
unfolding channel.res_def cipher.res_def cipher.routing_def cipher.enc_def cipher.dec_def
interface_wiring cipher.πE_def key.res_def key_channel_send_def key_channel_recv_def
by (simp add: conv_callee_parallel_id_left[where s="()", symmetric])
((auto cong: option.case_cong simp add: option.case_distrib[where h="λgpv. exec_gpv _ gpv _"]
intro!: extend_state_oracle_parametric ) | subst lift_state_oracle_extend_state_oracle)+
qed
lemma ideal_resource_wiring:
shows "(CNV callee s) |⇩= 1⇩C ⊳ channel.res sec_channel.sec_oracle
= RES (callee_sec_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 (sec_channel.sec_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 (sec_channel.sec_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
end
lemma eq_ℐ_gpv_Done1:
"eq_ℐ_gpv A ℐ (Done x) gpv ⟷ lossless_spmf (the_gpv gpv) ∧ (∀a∈set_spmf (the_gpv gpv). eq_ℐ_generat A ℐ (eq_ℐ_gpv A ℐ) (Pure x) a)"
by(auto intro: eq_ℐ_gpv.intros simp add: rel_spmf_return_spmf1 elim: eq_ℐ_gpv.cases)
lemma eq_ℐ_gpv_Done2:
"eq_ℐ_gpv A ℐ gpv (Done x) ⟷ lossless_spmf (the_gpv gpv) ∧ (∀a∈set_spmf (the_gpv gpv). eq_ℐ_generat A ℐ (eq_ℐ_gpv A ℐ) a (Pure x))"
by(auto intro: eq_ℐ_gpv.intros simp add: rel_spmf_return_spmf2 elim: eq_ℐ_gpv.cases)
context begin
interpretation CIPHER: cipher "key η" "enc η" "dec η" for η .
interpretation S_CHAN: sec_channel .
lemma one_time_pad:
defines "ℐ_real ≡ λη. ℐ_uniform UNIV (insert None (Some ` nlists UNIV η))"
and "ℐ_ideal ≡ λη. ℐ_uniform UNIV {None, Some η}"
and "ℐ_common ≡ λη. ℐ_uniform (nlists UNIV η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` nlists UNIV η))"
shows
"constructive_security2 CIPHER.res (λ_. S_CHAN.res) (λ_. CNV sim None)
ℐ_real ℐ_ideal ℐ_common (λ_. ∞) False (λ_. auth_sec_wiring)"
proof
let ?ℐ_key = "λη. ℐ_uniform UNIV (nlists UNIV η)"
let ?ℐ_enc = "λη. ℐ_uniform (nlists UNIV η) UNIV"
let ?ℐ_dec = "λη. ℐ_uniform UNIV (insert None (Some ` nlists UNIV η))"
have i1 [WT_intro]: "ℐ_uniform (nlists UNIV η) UNIV, ?ℐ_key η ⊕⇩ℐ ?ℐ_enc η ⊢⇩C CIPHER.enc η √" for η
unfolding CIPHER.enc_def by(rule WT_converter_of_callee)(auto simp add: stateless_callee_def enc_def in_nlists_UNIV)
have i2 [WT_intro]: "?ℐ_dec η, ?ℐ_key η ⊕⇩ℐ ?ℐ_dec η ⊢⇩C CIPHER.dec η √" for η
unfolding CIPHER.dec_def by(rule WT_converter_of_callee)(auto simp add: stateless_callee_def dec_def in_nlists_UNIV)
have [WT_intro]: "ℐ_common η, (?ℐ_key η ⊕⇩ℐ ?ℐ_enc η) ⊕⇩ℐ (?ℐ_key η ⊕⇩ℐ ?ℐ_dec η) ⊢⇩C CIPHER.enc η |⇩= CIPHER.dec η √" for η
unfolding ℐ_common_def by(rule WT_intro)+
have key: "callee_invariant_on (CIPHER.KEY.key_oracle η ⊕⇩O CIPHER.KEY.key_oracle η) (pred_option (λx. length x = η))
(?ℐ_key η ⊕⇩ℐ ?ℐ_key η)" for η
apply unfold_locales
subgoal for s x y s' by(cases s; cases x)(auto simp add: option.pred_set, simp_all add: key_def in_nlists_UNIV)
subgoal for s by(cases s)(auto intro!: WT_calleeI, simp_all add: key_def in_nlists_UNIV)
done
have i3: "?ℐ_key η ⊕⇩ℐ ?ℐ_key η ⊢res CIPHER.KEY.res η √" for η
unfolding CIPHER.KEY.res_def by(rule callee_invariant_on.WT_resource_of_oracle[OF key]) simp
let ?I = "λη. pred_cstate (λx. length x = η)"
have WT_auth: "ℐ_real η ⊢c CIPHER.AUTH.auth_oracle s √" if "?I η s" for η s
apply(rule WT_calleeI)
subgoal for x y s' using that
by(cases "(s, x)" rule: CIPHER.AUTH.auth_oracle.cases)(auto simp add: ℐ_real_def in_nlists_UNIV intro!: imageI)
done
have WT_recv: "?ℐ_dec η ⊢c S_CHAN.recv_oracle s √" if "pred_cstate (λx. length x = η) s" for η s
using that by(cases s)(auto intro!: WT_calleeI simp add: in_nlists_UNIV)
have WT_send: "?ℐ_enc η ⊢c S_CHAN.send_oracle s √" for η s
by(rule WT_calleeI)(auto)
have *: "callee_invariant_on (CIPHER.AUTH.auth_oracle ⊕⇩O S_CHAN.send_oracle ⊕⇩O S_CHAN.recv_oracle) (?I η)
(ℐ_real η ⊕⇩ℐ ℐ_common η)" for η
apply unfold_locales
subgoal for s x y s'
by(cases x; cases "(s, projl x)" rule: CIPHER.AUTH.auth_oracle.cases; cases "projr x")(auto simp add: ℐ_common_def in_nlists_UNIV)
subgoal by(auto simp add: ℐ_common_def WT_auth WT_recv intro: WT_calleeI)
done
have i4 [unfolded ℐ_common_def, WT_intro]: "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res CIPHER.AUTH.res √" for η
unfolding CIPHER.AUTH.res_def by(rule callee_invariant_on.WT_resource_of_oracle[OF *]) simp
show cipher: "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res CIPHER.res η √" for η
unfolding CIPHER.res_def by(rule WT_intro i3)+
show secure: "ℐ_ideal η ⊕⇩ℐ ℐ_common η ⊢res S_CHAN.res √" for η
proof -
have[simp]:"ℐ_ideal η ⊢c S_CHAN.sec_oracle s √" if "?I η s" for s
proof (cases rule: WT_calleeI, goal_cases)
case (1 call ret s')
then show ?case using that by (cases "(s, call)" rule: S_CHAN.sec_oracle.cases) (simp_all add: ℐ_ideal_def)
qed
have[simp]: "ℐ_common η ⊢c (S_CHAN.send_oracle ⊕⇩O S_CHAN.recv_oracle) s √"
if "pred_cstate (λx. length x = η) s" for s
unfolding ℐ_common_def by(rule WT_plus_oracleI WT_send WT_recv that)+
have *: "callee_invariant_on (S_CHAN.sec_oracle ⊕⇩O S_CHAN.send_oracle ⊕⇩O S_CHAN.recv_oracle) (?I η) (ℐ_ideal η ⊕⇩ℐ ℐ_common η)"
apply(unfold_locales)
subgoal for s x y s'
by(cases "(s, projl x)" rule: S_CHAN.sec_oracle.cases; cases "projr x")(auto simp add: ℐ_common_def in_nlists_UNIV)
subgoal by simp
done
show ?thesis unfolding S_CHAN.res_def
by(rule callee_invariant_on.WT_resource_of_oracle[OF *]) simp
qed
have sim [WT_intro]: "ℐ_real η, ℐ_ideal η ⊢⇩C CNV sim s √" if "s ≠ None ⟶ length (the s) = η" for s η
using that by(coinduction arbitrary: s)(auto simp add: sim_def ℐ_ideal_def ℐ_real_def in_nlists_UNIV)
show "ℐ_real η, ℐ_ideal η ⊢⇩C CNV sim None √" for η by(rule sim) simp
{ fix 𝒜 :: "security ⇒ (auth_query + bool list + unit, bool list option + unit + bool list option) distinguisher"
assume WT: "⋀η. ℐ_real η ⊕⇩ℐ ℐ_common η ⊢g 𝒜 η √"
and bound: "⋀η. interaction_bounded_by (λ_. True) (𝒜 η) ∞"
have "connect (𝒜 η) (CNV sim None |⇩= 1⇩C ⊳ S_CHAN.res) = connect (𝒜 η) (CIPHER.res η)" for η
using _ WT
proof(rule connect_cong_trace)
show "(UNIV <+> nlists UNIV (id' η) <+> UNIV) ⊢⇩R CNV sim None |⇩= 1⇩C ⊳ S_CHAN.res ≈ CIPHER.res η"
unfolding ideal_resource_wiring real_resource_wiring
by(rule resources_indistinguishable)
show "outs_gpv (ℐ_real η ⊕⇩ℐ ℐ_common η) (𝒜 η) ⊆ UNIV <+> nlists UNIV (id' η) <+> UNIV"
using WT[of η, THEN WT_gpv_outs_gpv]
by(auto simp add: ℐ_real_def ℐ_common_def id'_def)
show "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res CIPHER.res η √" by(rule cipher)
show "ℐ_real η ⊕⇩ℐ ℐ_common η ⊢res CNV sim None |⇩= 1⇩C ⊳ S_CHAN.res √"
by(rule WT_intro secure | simp)+
qed
then show "negligible (λη. advantage (𝒜 η) (CNV sim None |⇩= 1⇩C ⊳ S_CHAN.res) (CIPHER.res η))"
by(simp add: advantage_def)
next
let ?cnv = "map_converter id id auth_query_of sec_response_of 1⇩C
:: (auth_query, nat option, auth_query, bool list option) converter"
have [simp]: "ℐ_full, map_ℐ id (map_option length) ℐ_full ⊢⇩C 1⇩C √"
using WT_converter_id order_refl
by(rule WT_converter_mono)(simp add: le_ℐ_def)
have WT [WT_intro]: "ℐ_ideal η, ℐ_real η ⊢⇩C ?cnv √" for η
by(rule WT_converter_map_converter)(auto simp add: ℐ_ideal_def ℐ_real_def intro!: WT_converter_mono[OF WT_converter_id order_refl] simp add: le_ℐ_def in_nlists_UNIV)
with eq_ℐ_converter_reflI[OF this]
have "wiring (ℐ_ideal η) (ℐ_real η) ?cnv auth_sec_wiring" for η ..
moreover
have eq: "ℐ_ideal η, ℐ_ideal η ⊢⇩C map_converter id (map_option length) id id (CNV sim s) ∼ 1⇩C"
if "s ≠ None ⟶ length (the s) = η" for η and s :: "bool list option"
unfolding map_converter_of_callee map_gpv_conv_map_gpv'[symmetric] using that
by(coinduction arbitrary: s)
(fastforce intro!: eq_ℐ_gpv_Pause simp add: ℐ_ideal_def in_nlists_UNIV eq_ℐ_gpv_Done2 gpv.map_sel eq_onp_same_args sim_def map_gpv_conv_bind[symmetric] id_def[symmetric] split!: option.split if_split_asm)
have "ℐ_ideal η, ℐ_ideal η ⊢⇩C ?cnv ⊙ CNV sim None √" for η by(rule WT WT_intro)+ simp
with _ have "wiring (ℐ_ideal η) (ℐ_ideal η) (?cnv ⊙ CNV sim None) (id, id)" for η
by(rule wiring.intros)(auto simp add: comp_converter_map_converter1 comp_converter_id_left eq)
ultimately show "∃cnv. ∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) auth_sec_wiring ∧
wiring (ℐ_ideal η) (ℐ_ideal η) (cnv η ⊙ CNV sim None) (id, id)"
by meson
}
qed
end
end