Theory Diffie_Hellman
section βΉSpecifying security using gamesβΊ
theory Diffie_Hellman imports
CryptHOL.Cyclic_Group_SPMF
CryptHOL.Computational_Model
begin
subsection βΉThe DDH gameβΊ
locale ddh =
fixes π’ :: "'grp cyclic_group" (structure)
begin
type_synonym 'grp' adversary = "'grp' β 'grp' β 'grp' β bool spmf"
definition ddh_0 :: "'grp adversary β bool spmf"
where "ddh_0 π = do {
x β sample_uniform (order π’);
y β sample_uniform (order π’);
π (βg [^] x) (βg [^] y) (βg [^] (x * y))
}"
definition ddh_1 :: "'grp adversary β bool spmf"
where "ddh_1 π = do {
x β sample_uniform (order π’);
y β sample_uniform (order π’);
z β sample_uniform (order π’);
π (βg [^] x) (βg [^] y) (βg [^] z)
}"
definition advantage :: "'grp adversary β real"
where "advantage π = Β¦spmf (ddh_0 π) True - spmf (ddh_1 π) TrueΒ¦"
definition lossless :: "'grp adversary β bool"
where "lossless π β· (βΞ± Ξ² Ξ³. lossless_spmf (π Ξ± Ξ² Ξ³))"
lemma lossless_ddh_0:
"β¦ lossless π; 0 < order π’ β§
βΉ lossless_spmf (ddh_0 π)"
by(auto simp add: lossless_def ddh_0_def split_def Let_def)
lemma lossless_ddh_1:
"β¦ lossless π; 0 < order π’ β§
βΉ lossless_spmf (ddh_1 π)"
by(auto simp add: lossless_def ddh_1_def split_def Let_def)
end
subsection βΉThe LCDH gameβΊ
locale lcdh =
fixes π’ :: "'grp cyclic_group" (structure)
begin
type_synonym 'grp' adversary = "'grp' β 'grp' β 'grp' set spmf"
definition lcdh :: "'grp adversary β bool spmf"
where "lcdh π = do {
x β sample_uniform (order π’);
y β sample_uniform (order π’);
zs β π (βg [^] x) (βg [^] y);
return_spmf (βg [^] (x * y) β zs)
}"
definition advantage :: "'grp adversary β real"
where "advantage π = spmf (lcdh π) True"
definition lossless :: "'grp adversary β bool"
where "lossless π β· (βΞ± Ξ². lossless_spmf (π Ξ± Ξ²))"
lemma lossless_lcdh:
"β¦ lossless π; 0 < order π’ β§
βΉ lossless_spmf (lcdh π)"
by(auto simp add: lossless_def lcdh_def split_def Let_def)
end
end