Read about our upcoming Code of Conduct on this issue

Commit 34af7bfd authored by Gerwin Klein's avatar Gerwin Klein
Browse files

merge from afp-2021

......@@ -10403,3 +10403,41 @@ abstract =
for basis reduction, based on the efficient Hermite normal form
algorithm.
 
[Constructive_Cryptography_CM]
title = Constructive Cryptography in HOL: the Communication Modeling Aspect
author = Andreas Lochbihler <http://www.andreas-lochbihler.de>, S. Reza Sefidgar <>
topic = Computer science/Security/Cryptography, Mathematics/Probability theory
date = 2021-03-17
notify = mail@andreas-lochbihler.de, reza.sefidgar@inf.ethz.ch
abstract =
Constructive Cryptography (CC) [<a
href="https://conference.iiis.tsinghua.edu.cn/ICS2011/content/papers/14.html">ICS
2011</a>, <a
href="https://doi.org/10.1007/978-3-642-27375-9_3">TOSCA
2011</a>, <a
href="https://doi.org/10.1007/978-3-662-53641-4_1">TCC
2016</a>] introduces an abstract approach to composable security
statements that allows one to focus on a particular aspect of security
proofs at a time. Instead of proving the properties of concrete
systems, CC studies system classes, i.e., the shared behavior of
similar systems, and their transformations. Modeling of systems
communication plays a crucial role in composability and reusability of
security statements; yet, this aspect has not been studied in any of
the existing CC results. We extend our previous CC formalization
[<a href="https://isa-afp.org/entries/Constructive_Cryptography.html">Constructive_Cryptography</a>,
<a href="https://doi.org/10.1109/CSF.2019.00018">CSF
2019</a>] with a new semantic domain called Fused Resource
Templates (FRT) that abstracts over the systems communication patterns
in CC proofs. This widens the scope of cryptography proof
formalizations in the CryptHOL library [<a
href="https://isa-afp.org/entries/CryptHOL.html">CryptHOL</a>,
<a
href="https://doi.org/10.1007/978-3-662-49498-1_20">ESOP
2016</a>, <a
href="https://doi.org/10.1007/s00145-019-09341-z">J
Cryptol 2020</a>]. This formalization is described in <a
href="http://www.andreas-lochbihler.de/pub/basin2021.pdf">Abstract
Modeling of Systems Communication in Constructive Cryptography using
CryptHOL</a>.
theory Asymptotic_Security imports Concrete_Security begin
section \<open>Asymptotic security definition\<close>
locale constructive_security_obsf' =
fixes real_resource :: "security \<Rightarrow> ('a + 'e, 'b + 'f) resource"
and ideal_resource :: "security \<Rightarrow> ('c + 'e, 'd + 'f) resource"
and sim :: "security \<Rightarrow> ('a, 'b, 'c, 'd) converter"
and \<I>_real :: "security \<Rightarrow> ('a, 'b) \<I>"
and \<I>_ideal :: "security \<Rightarrow> ('c, 'd) \<I>"
and \<I>_common :: "security \<Rightarrow> ('e, 'f) \<I>"
and \<A> :: "security \<Rightarrow> ('a + 'e, 'b + 'f) distinguisher_obsf"
assumes constructive_security_aux_obsf: "\<And>\<eta>.
constructive_security_aux_obsf (real_resource \<eta>) (ideal_resource \<eta>) (sim \<eta>) (\<I>_real \<eta>) (\<I>_ideal \<eta>) (\<I>_common \<eta>) 0"
and adv: "\<lbrakk> \<And>\<eta>. exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) \<turnstile>g \<A> \<eta> \<surd> \<rbrakk>
\<Longrightarrow> negligible (\<lambda>\<eta>. advantage (\<A> \<eta>) (obsf_resource (sim \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal_resource \<eta>)) (obsf_resource (real_resource \<eta>)))"
begin
sublocale constructive_security_aux_obsf
"real_resource \<eta>"
"ideal_resource \<eta>"
"sim \<eta>"
"\<I>_real \<eta>"
"\<I>_ideal \<eta>"
"\<I>_common \<eta>"
"0"
for \<eta> by(rule constructive_security_aux_obsf)
lemma constructive_security_obsf'D:
"constructive_security_obsf (real_resource \<eta>) (ideal_resource \<eta>) (sim \<eta>) (\<I>_real \<eta>) (\<I>_ideal \<eta>) (\<I>_common \<eta>) (\<A> \<eta>)
(advantage (\<A> \<eta>) (obsf_resource (sim \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal_resource \<eta>)) (obsf_resource (real_resource \<eta>)))"
by(rule constructive_security_obsf_refl)
end
lemma constructive_security_obsf'I:
assumes "\<And>\<eta>. constructive_security_obsf (real_resource \<eta>) (ideal_resource \<eta>) (sim \<eta>) (\<I>_real \<eta>) (\<I>_ideal \<eta>) (\<I>_common \<eta>) (\<A> \<eta>) (adv \<eta>)"
and "(\<And>\<eta>. exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) \<turnstile>g \<A> \<eta> \<surd>) \<Longrightarrow> negligible adv"
shows "constructive_security_obsf' real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common \<A>"
proof -
interpret constructive_security_obsf
"real_resource \<eta>"
"ideal_resource \<eta>"
"sim \<eta>"
"\<I>_real \<eta>"
"\<I>_ideal \<eta>"
"\<I>_common \<eta>"
"\<A> \<eta>"
"adv \<eta>"
for \<eta> by fact
show ?thesis
proof
show "negligible (\<lambda>\<eta>. advantage (\<A> \<eta>) (obsf_resource (sim \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal_resource \<eta>)) (obsf_resource (real_resource \<eta>)))"
if "\<And>\<eta>. exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) \<turnstile>g \<A> \<eta> \<surd>" using assms(2)[OF that]
by(rule negligible_mono)(auto intro!: eventuallyI landau_o.big_mono simp add: advantage_nonneg adv_nonneg adv[OF that])
qed(rule WT_intro pfinite_intro order_refl)+
qed
lemma constructive_security_obsf'_into_constructive_security:
assumes "\<And>\<A> :: security \<Rightarrow> ('a + 'b, 'c + 'd) distinguisher_obsf.
\<lbrakk> \<And>\<eta>. interaction_bounded_by (\<lambda>_. True) (\<A> \<eta>) (bound \<eta>);
\<And>\<eta>. lossless \<Longrightarrow> plossless_gpv (exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>)) (\<A> \<eta>) \<rbrakk>
\<Longrightarrow> constructive_security_obsf' real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common \<A>"
and correct: "\<exists>cnv. \<forall>\<D>. (\<forall>\<eta>. \<I>_ideal \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta> \<turnstile>g \<D> \<eta> \<surd>) \<longrightarrow>
(\<forall>\<eta>. interaction_any_bounded_by (\<D> \<eta>) (bound \<eta>)) \<longrightarrow>
(\<forall>\<eta>. lossless \<longrightarrow> plossless_gpv (\<I>_ideal \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) (\<D> \<eta>)) \<longrightarrow>
(\<forall>\<eta>. wiring (\<I>_ideal \<eta>) (\<I>_real \<eta>) (cnv \<eta>) (w \<eta>)) \<and>
Negligible.negligible (\<lambda>\<eta>. advantage (\<D> \<eta>) (ideal_resource \<eta>) (cnv \<eta> |\<^sub>= 1\<^sub>C \<rhd> real_resource \<eta>))"
shows "constructive_security real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common bound lossless w"
proof
interpret constructive_security_obsf' real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common \<open>\<lambda>_. Done undefined\<close>
by(rule assms) simp_all
show "\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta> \<turnstile>res real_resource \<eta> \<surd>"
and "\<I>_ideal \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta> \<turnstile>res ideal_resource \<eta> \<surd>"
and "\<I>_real \<eta>, \<I>_ideal \<eta> \<turnstile>\<^sub>C sim \<eta> \<surd>" for \<eta> by(rule WT_intro)+
show "\<exists>cnv. \<forall>\<D>. (\<forall>\<eta>. \<I>_ideal \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta> \<turnstile>g \<D> \<eta> \<surd>) \<longrightarrow>
(\<forall>\<eta>. interaction_any_bounded_by (\<D> \<eta>) (bound \<eta>)) \<longrightarrow>
(\<forall>\<eta>. lossless \<longrightarrow> plossless_gpv (\<I>_ideal \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) (\<D> \<eta>)) \<longrightarrow>
(\<forall>\<eta>. wiring (\<I>_ideal \<eta>) (\<I>_real \<eta>) (cnv \<eta>) (w \<eta>)) \<and>
Negligible.negligible (\<lambda>\<eta>. advantage (\<D> \<eta>) (ideal_resource \<eta>) (cnv \<eta> |\<^sub>= 1\<^sub>C \<rhd> real_resource \<eta>))"
by fact
next
fix \<A> :: "security \<Rightarrow> ('a + 'b, 'c + 'd) distinguisher"
assume WT_adv [WT_intro]: "\<And>\<eta>. \<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta> \<turnstile>g \<A> \<eta> \<surd>"
and bound [interaction_bound]: "\<And>\<eta>. interaction_any_bounded_by (\<A> \<eta>) (bound \<eta>)"
and lossless: "\<And>\<eta>. lossless \<Longrightarrow> plossless_gpv (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) (\<A> \<eta>)"
let ?\<A> = "\<lambda>\<eta>. obsf_distinguisher (\<A> \<eta>)"
interpret constructive_security_obsf' real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common ?\<A>
proof(rule assms)
show "interaction_any_bounded_by (?\<A> \<eta>) (bound \<eta>)" for \<eta> by(rule interaction_bound)+
show "plossless_gpv (exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>)) (?\<A> \<eta>)" if lossless for \<eta>
using WT_adv[of \<eta>] lossless that by(simp)
qed
have "negligible (\<lambda>\<eta>. advantage (?\<A> \<eta>) (obsf_resource (sim \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal_resource \<eta>)) (obsf_resource (real_resource \<eta>)))"
by(rule adv)(rule WT_intro)+
then show "negligible (\<lambda>\<eta>. advantage (\<A> \<eta>) (sim \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal_resource \<eta>) (real_resource \<eta>))"
unfolding advantage_obsf_distinguisher .
qed
subsection \<open>Composition theorems\<close>
theorem constructive_security_obsf'_composability:
fixes real
assumes "constructive_security_obsf' middle ideal sim_inner \<I>_middle \<I>_inner \<I>_common (\<lambda>\<eta>. absorb (\<A> \<eta>) (obsf_converter (sim_outer \<eta> |\<^sub>= 1\<^sub>C)))"
assumes "constructive_security_obsf' real middle sim_outer \<I>_real \<I>_middle \<I>_common \<A>"
shows "constructive_security_obsf' real ideal (\<lambda>\<eta>. sim_outer \<eta> \<odot> sim_inner \<eta>) \<I>_real \<I>_inner \<I>_common \<A>"
proof(rule constructive_security_obsf'I)
let ?\<A> = "\<lambda>\<eta>. absorb (\<A> \<eta>) (obsf_converter (sim_outer \<eta> |\<^sub>= 1\<^sub>C))"
interpret inner: constructive_security_obsf' middle ideal sim_inner \<I>_middle \<I>_inner \<I>_common ?\<A> by fact
interpret outer: constructive_security_obsf' real middle sim_outer \<I>_real \<I>_middle \<I>_common \<A> by fact
let ?adv1 = "\<lambda>\<eta>. advantage (?\<A> \<eta>) (obsf_resource (sim_inner \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal \<eta>)) (obsf_resource (middle \<eta>))"
let ?adv2 = "\<lambda>\<eta>. advantage (\<A> \<eta>) (obsf_resource (sim_outer \<eta> |\<^sub>= 1\<^sub>C \<rhd> middle \<eta>)) (obsf_resource (real \<eta>))"
let ?adv = "\<lambda>\<eta>. ?adv1 \<eta> + ?adv2 \<eta>"
show "constructive_security_obsf (real \<eta>) (ideal \<eta>) (sim_outer \<eta> \<odot> sim_inner \<eta>) (\<I>_real \<eta>) (\<I>_inner \<eta>) (\<I>_common \<eta>) (\<A> \<eta>) (?adv \<eta>)" for \<eta>
using inner.constructive_security_obsf'D outer.constructive_security_obsf'D
by(rule constructive_security_obsf_composability)
assume [WT_intro]: "exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta>) \<turnstile>g \<A> \<eta> \<surd>" for \<eta>
have "negligible ?adv1" by(rule inner.adv)(rule WT_intro)+
also have "negligible ?adv2" by(rule outer.adv)(rule WT_intro)+
finally (negligible_plus) show "negligible ?adv" .
qed
theorem constructive_security_obsf'_lifting: (* TODO: generalize! *)
assumes sec: "constructive_security_obsf' real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common (\<lambda>\<eta>. absorb (\<A> \<eta>) (obsf_converter (1\<^sub>C |\<^sub>= conv \<eta>)))"
assumes WT_conv [WT_intro]: "\<And>\<eta>. \<I>_common' \<eta>, \<I>_common \<eta> \<turnstile>\<^sub>C conv \<eta> \<surd>"
and pfinite [pfinite_intro]: "\<And>\<eta>. pfinite_converter (\<I>_common' \<eta>) (\<I>_common \<eta>) (conv \<eta>)"
shows "constructive_security_obsf'
(\<lambda>\<eta>. 1\<^sub>C |\<^sub>= conv \<eta> \<rhd> real_resource \<eta>) (\<lambda>\<eta>. 1\<^sub>C |\<^sub>= conv \<eta> \<rhd> ideal_resource \<eta>) sim
\<I>_real \<I>_ideal \<I>_common' \<A>"
proof(rule constructive_security_obsf'I)
let ?\<A> = "\<lambda>\<eta>. absorb (\<A> \<eta>) (obsf_converter (1\<^sub>C |\<^sub>= conv \<eta>))"
interpret constructive_security_obsf' real_resource ideal_resource sim \<I>_real \<I>_ideal \<I>_common ?\<A> by fact
let ?adv = "\<lambda>\<eta>. advantage (?\<A> \<eta>) (obsf_resource (sim \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal_resource \<eta>)) (obsf_resource (real_resource \<eta>))"
fix \<eta> :: security
show "constructive_security_obsf (1\<^sub>C |\<^sub>= conv \<eta> \<rhd> real_resource \<eta>) (1\<^sub>C |\<^sub>= conv \<eta> \<rhd> ideal_resource \<eta>) (sim \<eta>)
(\<I>_real \<eta>) (\<I>_ideal \<eta>) (\<I>_common' \<eta>) (\<A> \<eta>)
(?adv \<eta>)"
using constructive_security_obsf.constructive_security_aux_obsf[OF constructive_security_obsf'D]
constructive_security_obsf.constructive_security_sim_obsf[OF constructive_security_obsf'D]
by(rule constructive_security_obsf_lifting_usr)(rule WT_intro pfinite_intro)+
show "negligible ?adv" if [WT_intro]: "\<And>\<eta>. exception_\<I> (\<I>_real \<eta> \<oplus>\<^sub>\<I> \<I>_common' \<eta>) \<turnstile>g \<A> \<eta> \<surd>"
by(rule adv)(rule WT_intro)+
qed
theorem constructive_security_obsf'_trivial:
fixes res
assumes [WT_intro]: "\<And>\<eta>. \<I> \<eta> \<oplus>\<^sub>\<I> \<I>_common \<eta> \<turnstile>res res \<eta> \<surd>"
shows "constructive_security_obsf' res res (\<lambda>_. 1\<^sub>C) \<I> \<I> \<I>_common \<A>"
proof(rule constructive_security_obsf'I)
show "constructive_security_obsf (res \<eta>) (res \<eta>) 1\<^sub>C (\<I> \<eta>) (\<I> \<eta>) (\<I>_common \<eta>) (\<A> \<eta>) 0" for \<eta>
using assms by(rule constructive_security_obsf_trivial)
qed simp
theorem parallel_constructive_security_obsf':
assumes "constructive_security_obsf' real1 ideal1 sim1 \<I>_real1 \<I>_inner1 \<I>_common1 (\<lambda>\<eta>. absorb (\<A> \<eta>) (obsf_converter (parallel_wiring \<odot> parallel_converter 1\<^sub>C (converter_of_resource (sim2 \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal2 \<eta>)))))"
(is "constructive_security_obsf' _ _ _ _ _ _ ?\<A>1")
assumes "constructive_security_obsf' real2 ideal2 sim2 \<I>_real2 \<I>_inner2 \<I>_common2 (\<lambda>\<eta>. absorb (\<A> \<eta>) (obsf_converter (parallel_wiring \<odot> parallel_converter (converter_of_resource (real1 \<eta>)) 1\<^sub>C)))"
(is "constructive_security_obsf' _ _ _ _ _ _ ?\<A>2")
shows "constructive_security_obsf' (\<lambda>\<eta>. parallel_wiring \<rhd> real1 \<eta> \<parallel> real2 \<eta>) (\<lambda>\<eta>. parallel_wiring \<rhd> ideal1 \<eta> \<parallel> ideal2 \<eta>) (\<lambda>\<eta>. sim1 \<eta> |\<^sub>= sim2 \<eta>)
(\<lambda>\<eta>. \<I>_real1 \<eta> \<oplus>\<^sub>\<I> \<I>_real2 \<eta>) (\<lambda>\<eta>. \<I>_inner1 \<eta> \<oplus>\<^sub>\<I> \<I>_inner2 \<eta>) (\<lambda>\<eta>. \<I>_common1 \<eta> \<oplus>\<^sub>\<I> \<I>_common2 \<eta>) \<A>"
proof(rule constructive_security_obsf'I)
interpret sec1: constructive_security_obsf' real1 ideal1 sim1 \<I>_real1 \<I>_inner1 \<I>_common1 ?\<A>1 by fact
interpret sec2: constructive_security_obsf' real2 ideal2 sim2 \<I>_real2 \<I>_inner2 \<I>_common2 ?\<A>2 by fact
let ?adv1 = "\<lambda>\<eta>. advantage (?\<A>1 \<eta>) (obsf_resource (sim1 \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal1 \<eta>)) (obsf_resource (real1 \<eta>))"
let ?adv2 = "\<lambda>\<eta>. advantage (?\<A>2 \<eta>) (obsf_resource (sim2 \<eta> |\<^sub>= 1\<^sub>C \<rhd> ideal2 \<eta>)) (obsf_resource (real2 \<eta>))"
let ?adv = "\<lambda>\<eta>. ?adv1 \<eta> + ?adv2 \<eta>"
show "constructive_security_obsf (parallel_wiring \<rhd> real1 \<eta> \<parallel> real2 \<eta>) (parallel_wiring \<rhd> ideal1 \<eta> \<parallel> ideal2 \<eta>)
(sim1 \<eta> |\<^sub>= sim2 \<eta>) (\<I>_real1 \<eta> \<oplus>\<^sub>\<I> \<I>_real2 \<eta>) (\<I>_inner1 \<eta> \<oplus>\<^sub>\<I> \<I>_inner2 \<eta>) (\<I>_common1 \<eta> \<oplus>\<^sub>\<I> \<I>_common2 \<eta>) (\<A> \<eta>)
(?adv \<eta>)" for \<eta>
using sec1.constructive_security_obsf'D sec2.constructive_security_obsf'D
by(rule parallel_constructive_security_obsf)
assume [WT_intro]: "exception_\<I> ((\<I>_real1 \<eta> \<oplus>\<^sub>\<I> \<I>_real2 \<eta>) \<oplus>\<^sub>\<I> (\<I>_common1 \<eta> \<oplus>\<^sub>\<I> \<I>_common2 \<eta>)) \<turnstile>g \<A> \<eta> \<surd>" for \<eta>
have "negligible ?adv1" by(rule sec1.adv)(rule WT_intro)+
also have "negligible ?adv2" by(rule sec2.adv)(rule WT_intro)+
finally (negligible_plus) show "negligible ?adv" .
qed
end
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
theory DH_OTP imports
One_Time_Pad
Diffie_Hellman_CC
begin
text \<open>
We need both a group structure and a boolean algebra.
Unfortunately, records allow only one extension slot, so we can't have just a single
structure with both operations.
\<close>
context diffie_hellman begin
lemma WT_ideal_rest [WT_intro]:
assumes WT_auth1_rest [WT_intro]: "WT_rest \<I>_adv_rest1 \<I>_usr_rest1 I_auth1_rest auth1_rest"
and WT_auth2_rest [WT_intro]: "WT_rest \<I>_adv_rest2 \<I>_usr_rest2 I_auth2_rest auth2_rest"
shows "WT_rest (\<I>_full \<oplus>\<^sub>\<I> (\<I>_adv_rest1 \<oplus>\<^sub>\<I> \<I>_adv_rest2)) ((\<I>_full \<oplus>\<^sub>\<I> \<I>_full) \<oplus>\<^sub>\<I> (\<I>_usr_rest1 \<oplus>\<^sub>\<I> \<I>_usr_rest2))
(\<lambda>(_, s). pred_prod I_auth1_rest I_auth2_rest s) (ideal_rest auth1_rest auth2_rest)"
apply(rule WT_rest.intros)
subgoal
by(auto 4 4 split: sum.splits simp add: translate_eoracle_def parallel_eoracle_def dest: assms[THEN WT_restD_rfunc_adv])
subgoal
apply(auto 4 4 split: sum.splits simp add: translate_eoracle_def parallel_eoracle_def plus_eoracle_def dest: assms[THEN WT_restD_rfunc_usr])
apply(simp add: map_sum_def split: sum.splits)
done
subgoal by(simp add: assms[THEN WT_restD_rinit])
done
end
locale dh_otp = dh: diffie_hellman \<G> + otp: one_time_pad \<L>
for \<G> :: "'grp cyclic_group"
and \<L> :: "'grp boolean_algebra" +
assumes carrier_\<G>_\<L>: "carrier \<G> = carrier \<L>"
begin
theorem secure:
assumes "WT_rest \<I>_adv_resta \<I>_usr_resta I_auth_rest auth_rest"
and "WT_rest \<I>_adv_rest1 \<I>_usr_rest1 I_auth1_rest auth1_rest"
and "WT_rest \<I>_adv_rest2 \<I>_usr_rest2 I_auth2_rest auth2_rest"
shows
"constructive_security_obsf
(1\<^sub>C |\<^sub>= wiring_c1r22_c1r22 (CNV otp.enc_callee ()) (CNV otp.dec_callee ()) |\<^sub>= 1\<^sub>C \<rhd>
fused_wiring \<rhd> diffie_hellman.real_resource \<G> auth1_rest auth2_rest \<parallel> dh.auth.resource auth_rest)
(otp.sec.resource (otp.ideal_rest (dh.ideal_rest auth1_rest auth2_rest) auth_rest))
((1\<^sub>C \<odot>
(parallel_wiring \<odot> ((let sim = CNV dh.sim_callee None in (sim |\<^sub>= 1\<^sub>C) \<odot> lassocr\<^sub>C) |\<^sub>= 1\<^sub>C) \<odot> parallel_wiring) \<odot>
1\<^sub>C) \<odot>
(otp.sim |\<^sub>= 1\<^sub>C))
((((\<I>_full \<oplus>\<^sub>\<I> (\<I>_full \<oplus>\<^sub>\<I> \<I>_uniform (otp.sec.Inp_Fedit ` carrier \<G>) UNIV)) \<oplus>\<^sub>\<I>
(\<I>_full \<oplus>\<^sub>\<I> (\<I>_full \<oplus>\<^sub>\<I> \<I>_uniform (otp.sec.Inp_Fedit ` carrier \<G>) UNIV))) \<oplus>\<^sub>\<I>
(\<I>_full \<oplus>\<^sub>\<I> (\<I>_full \<oplus>\<^sub>\<I> \<I>_uniform (otp.sec.Inp_Fedit ` carrier \<L>) UNIV))) \<oplus>\<^sub>\<I>
((\<I>_adv_rest1 \<oplus>\<^sub>\<I> \<I>_adv_rest2) \<oplus>\<^sub>\<I> \<I>_adv_resta))
((\<I>_full \<oplus>\<^sub>\<I> (\<I>_full \<oplus>\<^sub>\<I> \<I>_uniform (otp.sec.Inp_Fedit ` carrier \<L>) UNIV)) \<oplus>\<^sub>\<I>
((\<I>_full \<oplus>\<^sub>\<I> (\<I>_adv_rest1 \<oplus>\<^sub>\<I> \<I>_adv_rest2)) \<oplus>\<^sub>\<I> \<I>_adv_resta))
((\<I>_uniform (otp.sec.Inp_Send ` carrier \<L>) UNIV \<oplus>\<^sub>\<I> \<I>_uniform UNIV (otp.sec.Out_Recv ` carrier \<L>)) \<oplus>\<^sub>\<I>
(((\<I>_full \<oplus>\<^sub>\<I> \<I>_full) \<oplus>\<^sub>\<I> (\<I>_usr_rest1 \<oplus>\<^sub>\<I> \<I>_usr_rest2)) \<oplus>\<^sub>\<I> \<I>_usr_resta))
\<A> (0 + (ddh.advantage \<G>
(diffie_hellman.DH_adversary \<G> auth1_rest auth2_rest
(absorb
(absorb \<A>
(obsf_converter (1\<^sub>C |\<^sub>= wiring_c1r22_c1r22 (CNV otp.enc_callee ()) (CNV otp.dec_callee ()) |\<^sub>= 1\<^sub>C)))
(obsf_converter
(fused_wiring \<odot> (1\<^sub>C |\<^sub>\<propto> converter_of_resource (1\<^sub>C |\<^sub>= 1\<^sub>C \<rhd> dh.auth.resource auth_rest)))))) +
0))"
using assms apply -
apply(rule constructive_security_obsf_composability)
apply(rule otp.secure)
apply(rule WT_intro, assumption+)
unfolding otp.real_resource_def attach_c1f22_c1f22_def[abs_def] attach_compose
apply(rule constructive_security_obsf_lifting_[where w_adv_real="1\<^sub>C" and w_adv_ideal_inv="1\<^sub>C"])
apply(rule parallel_constructive_security_obsf_fuse)
apply(fold carrier_\<G>_\<L>)[1]
apply(rule dh.secure, assumption, assumption, rule constructive_security_obsf_trivial)
defer
defer
defer
apply(rule WT_intro)+
apply(simp add: comp_converter_id_left)
apply(rule parallel_converter2_id_id pfinite_intro wiring_intro)+
apply(rule WT_intro|assumption)+
apply simp
apply(unfold wiring_c1r22_c1r22_def)
apply(rule WT_intro)+
apply(fold carrier_\<G>_\<L>)[1]
apply(rule WT_intro)+
apply(rule pfinite_intro)
apply(rule pfinite_intro)
apply(rule pfinite_intro)
apply(rule pfinite_intro)
apply(rule pfinite_intro)
apply(unfold carrier_\<G>_\<L>)
apply(rule pfinite_intro)
apply(rule WT_intro)+
apply(rule pfinite_intro)
done
end
end
\ No newline at end of file
theory Fold_Spmf
imports
More_CC
begin
primrec (transfer)
foldl_spmf :: "('b \<Rightarrow> 'a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf \<Rightarrow> 'a list \<Rightarrow> 'b spmf"
where
foldl_spmf_Nil: "foldl_spmf f p [] = p"
| foldl_spmf_Cons: "foldl_spmf f p (x # xs) = foldl_spmf f (bind_spmf p (\<lambda>a. f a x)) xs"
lemma foldl_spmf_return_pmf_None [simp]:
"foldl_spmf f (return_pmf None) xs = return_pmf None"
by(induction xs) simp_all
lemma foldl_spmf_bind_spmf: "foldl_spmf f (bind_spmf p g) xs = bind_spmf p (\<lambda>a. foldl_spmf f (g a) xs)"
by(induction xs arbitrary: g) simp_all
lemma bind_foldl_spmf_return:
"bind_spmf p (\<lambda>x. foldl_spmf f (return_spmf x) xs) = foldl_spmf f p xs"
by(simp add: foldl_spmf_bind_spmf[symmetric])
lemma foldl_spmf_map [simp]: "foldl_spmf f p (map g xs) = foldl_spmf (map_fun id (map_fun g id) f) p xs"
by(induction xs arbitrary: p) simp_all
lemma foldl_spmf_identity [simp]: "foldl_spmf (\<lambda>s x. return_spmf s) p xs = p"
by(induction xs arbitrary: p) simp_all
lemma foldl_spmf_conv_foldl:
"foldl_spmf (\<lambda>s x. return_spmf (f s x)) p xs = map_spmf (\<lambda>s. foldl f s xs) p"
by(induction xs arbitrary: p)(simp_all add: map_spmf_conv_bind_spmf[symmetric] spmf.map_comp o_def)
lemma foldl_spmf_Cons':
"foldl_spmf f (return_spmf a) (x # xs) = bind_spmf (f a x) (\<lambda>a'. foldl_spmf f (return_spmf a') xs)"
by(simp add: bind_foldl_spmf_return)
lemma foldl_spmf_append: "foldl_spmf f p (xs @ ys) = foldl_spmf f (foldl_spmf f p xs) ys"
by(induction xs arbitrary: p) simp_all
lemma
foldl_spmf_helper:
assumes "\<And>x. h (f x) = x"
assumes "\<And>x. f (h x) = x"
shows "foldl_spmf (\<lambda>a e. map_spmf h (g (f a) e)) acc es =
map_spmf h (foldl_spmf g (map_spmf f acc) es)"
using assms proof (induction es arbitrary: acc)
case (Cons a es)
then show ?case
by (simp add: spmf.map_comp map_bind_spmf bind_map_spmf o_def)
qed (simp add: map_spmf_conv_bind_spmf)
lemma
foldl_spmf_helper2:
assumes "\<And>x y. p (f x y) = x"
assumes "\<And>x y. q (f x y) = y"
assumes "\<And>x. f (p x) (q x) = x"
shows "foldl_spmf (\<lambda>a e. map_spmf (f (p a)) (g (q a) e)) acc es =
bind_spmf acc (\<lambda>acc'. map_spmf (f (p acc')) (foldl_spmf g (return_spmf (q acc')) es))"
proof (induction es arbitrary: acc)
note [simp] = spmf.map_comp map_bind_spmf bind_map_spmf o_def
case (Cons e es)
then show ?case
apply (simp add: map_spmf_conv_bind_spmf assms)
apply (subst bind_spmf_assoc[symmetric])
by (simp add: bind_foldl_spmf_return)
qed (simp add: assms(3))
lemma foldl_pair_constl: "foldl (\<lambda>s e. map_prod (\<lambda>_. c) (\<lambda>r. f r e) s) (c, sr) l =
Pair c (foldl (\<lambda>s e. f s e) sr l)"
by (induction l arbitrary: sr) (auto simp add: map_prod_def split_def)
lemma foldl_spmf_pair_left:
"foldl_spmf (\<lambda>(l, r) e. map_spmf (\<lambda>l'. (l', r)) (f l e)) (return_spmf (l, r)) es =
map_spmf (\<lambda>l'. (l', r)) (foldl_spmf f (return_spmf l) es)"
apply (induction es arbitrary: l)
apply simp_all
apply (subst (2) map_spmf_conv_bind_spmf)
apply (subst foldl_spmf_bind_spmf)
apply (subst (2) bind_foldl_spmf_return[symmetric])
by (simp add: map_spmf_conv_bind_spmf)
lemma foldl_spmf_pair_left2:
"foldl_spmf (\<lambda>(l, _) e. map_spmf (\<lambda>l'. (l', c')) (f l e)) (return_spmf (l, c)) es =
map_spmf (\<lambda>l'. (l', if es = [] then c else c')) (foldl_spmf f (return_spmf l) es)"
apply (induction es arbitrary: l c c')
apply simp_all
apply (subst (2) map_spmf_conv_bind_spmf)
apply (subst foldl_spmf_bind_spmf)
apply (subst (2) bind_foldl_spmf_return[symmetric])
by (simp add: map_spmf_conv_bind_spmf)
lemma foldl_pair_constr: "foldl (\<lambda>s e. map_prod (\<lambda>l. f l e) (\<lambda>_. c) s) (sl, c) l =
Pair (foldl (\<lambda>s e. f s e) sl l) c"
by (induction l arbitrary: sl) (auto simp add: map_prod_def split_def)
lemma foldl_spmf_pair_right:
"foldl_spmf (\<lambda>(l, r) e. map_spmf (\<lambda>r'. (l, r')) (f r e)) (return_spmf (l, r)) es =
map_spmf (\<lambda>r'. (l, r')) (foldl_spmf f (return_spmf r) es)"
apply (induction es arbitrary: r)
apply simp_all
apply (subst (2) map_spmf_conv_bind_spmf)
apply (subst foldl_spmf_bind_spmf)
apply (subst (2) bind_foldl_spmf_return[symmetric])
by (simp add: map_spmf_conv_bind_spmf)
lemma foldl_spmf_pair_right2:
"foldl_spmf (\<lambda>(_, r) e. map_spmf (\<lambda>r'. (c', r')) (f r e)) (return_spmf (c, r)) es =
map_spmf (\<lambda>r'. (if es = [] then c else c', r')) (foldl_spmf f (return_spmf r) es)"
apply (induction es arbitrary: r c c')
apply simp_all
apply (subst (2) map_spmf_conv_bind_spmf)
apply (subst foldl_spmf_bind_spmf)
apply (subst (2) bind_foldl_spmf_return[symmetric])
by (auto simp add: map_spmf_conv_bind_spmf split_def)
lemma foldl_spmf_pair_right3:
"foldl_spmf (\<lambda>(l, r) e. map_spmf (Pair (g e)) (f r e)) (return_spmf (l, r)) es =
map_spmf (Pair (if es = [] then l else g (last es))) (foldl_spmf f (return_spmf r) es)"
apply (induction es arbitrary: r l)
apply simp_all
apply (subst (2) map_spmf_conv_bind_spmf)
apply (subst foldl_spmf_bind_spmf)
apply (subst (2) bind_foldl_spmf_return[symmetric])
by (clarsimp simp add: split_def map_bind_spmf o_def)
lemma foldl_pullout: "bind_spmf f (\<lambda>x. bind_spmf (foldl_spmf g init (events x)) (\<lambda>y. h x y)) =
bind_spmf (bind_spmf f (\<lambda>x. foldl_spmf (\<lambda>(l, r) e. map_spmf (Pair l) (g r e)) (map_spmf (Pair x) init) (events x)))
(\<lambda>(x, y). h x y)" for f g h init events
apply (simp add: foldl_spmf_helper2[where f=Pair and p=fst and q=snd, simplified] split_def)
apply (clarsimp simp add: map_spmf_conv_bind_spmf)
by (subst bind_spmf_assoc[symmetric]) (auto simp add: bind_foldl_spmf_return)
lemma bind_foldl_spmf_pair_append: "
bind_spmf
(foldl_spmf (\<lambda>(x, y) e. map_spmf (apfst ((@) x)) (f y e)) (return_spmf (a @ c, b)) es)
(\<lambda>(x, y). g x y) =
bind_spmf
(foldl_spmf (\<lambda>(x, y) e. map_spmf (apfst ((@) x)) (f y e)) (return_spmf (c, b)) es)
(\<lambda>(x, y). g (a @ x) y)"
apply (induction es arbitrary: c b)
apply (simp_all add: split_def map_spmf_conv_bind_spmf apfst_def map_prod_def)
apply (subst (1 2) foldl_spmf_bind_spmf)
by simp
lemma foldl_spmf_chain: "
(foldl_spmf (\<lambda>(oevents, s_event) event. map_spmf (map_prod ((@) oevents) id) (fff s_event event)) (return_spmf ([], s_event)) ievents)
\<bind> (\<lambda>(oevents, s_event'). foldl_spmf ggg (return_spmf s_core) oevents
\<bind> (\<lambda>s_core'. return_spmf (f s_core' s_event'))) =
foldl_spmf (\<lambda>(s_event, s_core) event. fff s_event event \<bind> (\<lambda>(oevents, s_event').
map_spmf (Pair s_event') (foldl_spmf ggg (return_spmf s_core) oevents))) (return_spmf (s_event, s_core)) ievents
\<bind> (\<lambda>(s_event', s_core'). return_spmf (f s_core' s_event'))"
proof (induction ievents arbitrary: s_event s_core)
case Nil
show ?case by simp
next
case (Cons e es)
show ?case
apply (subst (1 2) foldl_spmf_Cons')
apply (simp add: split_def)
apply (subst map_spmf_conv_bind_spmf)
apply simp
apply (rule bind_spmf_cong[OF refl])
apply (subst (2) map_spmf_conv_bind_spmf)
apply simp
apply (subst Cons.IH[symmetric, simplified split_def])
apply (subst bind_commute_spmf)
apply (subst (2) map_spmf_conv_bind_spmf[symmetric])
apply (subst map_bind_spmf[symmetric, simplified o_def])
apply (subst (1) foldl_spmf_bind_spmf[symmetric])
apply (subst (3) map_spmf_conv_bind_spmf)
apply (simp add: foldl_spmf_append[symmetric] map_prod_def split_def)
subgoal for x
apply (cases x)
subgoal for a b
apply (simp add: split_def)
apply (subst bind_foldl_spmf_pair_append[where c="[]" and a=a and b=b and es=es, simplified apfst_def map_prod_def append_Nil2 split_def id_def])
by simp
done
done
qed
\<comment> \<open>pauses\<close>
primrec pauses :: "'a list \<Rightarrow> (unit, 'a, 'b) gpv" where
"pauses [] = Done ()"
| "pauses (x # xs) = Pause x (\<lambda>_. pauses xs)"
lemma WT_gpv_pauses [WT_intro]:
"\<I> \<turnstile>g pauses xs \<surd>" if "set xs \<subseteq> outs_\<I> \<I>"
using that by(induction xs) auto
lemma exec_gpv_pauses:
"exec_gpv callee (pauses xs) s =
map_spmf (Pair ()) (foldl_spmf (map_fun id (map_fun id (map_spmf snd)) callee) (return_spmf s) xs)"
by(induction xs arbitrary: s)(simp_all add: split_def foldl_spmf_Cons' map_bind_spmf bind_map_spmf o_def del: foldl_spmf_Cons)
end
\ No newline at end of file
This diff is collapsed.
theory Goodies
imports
Main
begin
primrec
inits :: "'a list \<Rightarrow> 'a list list"
where
"inits [] = []"
| "inits (x # xs) = [x] # map ((#) x) (inits xs)"
definition
inits_self :: "'a list \<Rightarrow> ('a list \<times> 'a) list"
where
"inits_self xs = zip ([] # inits xs) xs"
lemma inits_map: "inits (map f xs) = map (map f) (inits xs)"
by(induction xs) simp_all
lemma inits_append [simp]: "inits (xs @ ys) = inits xs @ map ((@) xs) (inits ys)"
by(induction xs) (simp_all)
lemma inits_self_simps [simp]:
"inits_self [] = []"
"inits_self (x # xs) = ([], x) # map (apfst ((#) x)) (inits_self xs)"
by(simp_all add: inits_self_def apfst_def map_prod_def zip_map1[symmetric])
lemma inits_self_map: "inits_self (map f xs) = map (map_prod (map f) f) (inits_self xs)"
by(induction xs) (simp_all add: apfst_def prod.map_comp o_def)
lemma in_set_inits_self: "(ys, z) \<in> set (inits_self xs) \<longleftrightarrow> (\<exists>zs. xs = ys @ z # zs)"
by(induction xs arbitrary: ys z)(auto simp add: Cons_eq_append_conv apfst_def map_prod_def)
lemma foldl_append: "foldl (\<lambda>s e. s @ [e]) s l = s @ l"
by (induction l arbitrary: s) auto
lemma foldl_insert: "foldl (\<lambda>A x. insert (f x) A) A xs = A \<union> (f ` set xs)"
by(induction xs arbitrary: A) simp_all
lemma foldl_concat_prodl: "foldl (\<lambda>(l, r) x. (l @ g r x, f r x)) (l, r) xs =
(l @ concat (map (\<lambda>(ys, x). g (foldl f r ys) x) (inits_self xs)), foldl f r xs)"
by(induction xs arbitrary: l r) (simp_all add: split_def o_def)
end
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
chapter AFP
session Constructive_Cryptography_CM (AFP) = Constructive_Cryptography +
options [timeout = 1500]
sessions
"Game_Based_Crypto"
"Sigma_Commit_Crypto"
directories
"Constructions"
"Specifications"
theories
"Constructions/DH_OTP"
document_files
"root.tex"
"root.bib"
theory Channel
imports
"../Fused_Resource"
begin
section \<open>Channel specification\<close>