Theory Malicious_OT
subsection ‹Malicious OT›
text ‹Here we prove secure the 1-out-of-2 OT protocol given in \<^cite>‹"DBLP:series/isc/HazayL10"› (p190).
For party 1 reduce security to the DDH assumption and for party 2 we show information theoretic security.›
theory Malicious_OT imports
"HOL-Number_Theory.Cong"
Cyclic_Group_Ext
DH_Ext
Malicious_Defs
Number_Theory_Aux
OT_Functionalities
Uniform_Sampling
begin
type_synonym ('aux, 'grp', 'state) adv_1_P1 = "('grp' × 'grp') ⇒ 'grp' ⇒ 'grp' ⇒ 'grp' ⇒ 'grp' ⇒ 'grp' ⇒ 'aux ⇒ (('grp' × 'grp' × 'grp') × 'state) spmf"
type_synonym ('grp', 'state) adv_2_P1 = "'grp' ⇒ 'grp' ⇒ 'grp' ⇒ 'grp' ⇒ 'grp' ⇒ ('grp' × 'grp') ⇒ 'state ⇒ ((('grp' × 'grp') × ('grp' × 'grp')) × 'state) spmf"
type_synonym ('adv_out1,'state) adv_3_P1 = "'state ⇒ 'adv_out1 spmf"
type_synonym ('aux, 'grp', 'adv_out1, 'state) adv_mal_P1 = "(('aux, 'grp', 'state) adv_1_P1 × ('grp', 'state) adv_2_P1 × ('adv_out1,'state) adv_3_P1)"
type_synonym ('aux, 'grp','state) adv_1_P2 = "bool ⇒ 'aux ⇒ (('grp' × 'grp' × 'grp' × 'grp' × 'grp') × 'state) spmf"
type_synonym ('grp','state) adv_2_P2 = "('grp' × 'grp' × 'grp' × 'grp' × 'grp') ⇒ 'state ⇒ ((('grp' × 'grp' × 'grp') × nat) × 'state) spmf"
type_synonym ('grp', 'adv_out2, 'state) adv_3_P2 = "('grp' × 'grp') ⇒ ('grp' × 'grp') ⇒ 'state ⇒ 'adv_out2 spmf"
type_synonym ('aux, 'grp', 'adv_out2, 'state) adv_mal_P2 = "(('aux, 'grp','state) adv_1_P2 × ('grp','state) adv_2_P2 × ('grp', 'adv_out2,'state) adv_3_P2)"
locale ot_base =
fixes 𝒢 :: "'grp cyclic_group" (structure)
assumes finite_group: "finite (carrier 𝒢)"
and order_gt_0: "order 𝒢 > 0"
and prime_order: "prime (order 𝒢)"
begin
lemma prime_field: "a < (order 𝒢) ⟹ a ≠ 0 ⟹ coprime a (order 𝒢)"
by (metis dvd_imp_le neq0_conv not_le prime_imp_coprime prime_order coprime_commute)
text‹The protocol uses a call to an idealised functionality of a zero knowledge protocol for the
DDH relation, this is described by the functionality given below.›
fun funct_DH_ZK :: "('grp × 'grp × 'grp) ⇒ (('grp × 'grp × 'grp) × nat) ⇒ (bool × unit) spmf"
where "funct_DH_ZK (h,a,b) ((h',a',b'),r) = return_spmf (a = ❙g [^] r ∧ b = h [^] r ∧ (h,a,b) = (h',a',b'), ())"
text‹The probabilistic program that defines the output for both parties in the protocol.›
definition protocol_ot :: "('grp × 'grp) ⇒ bool ⇒ (unit × 'grp) spmf"
where "protocol_ot M σ = do {
let (x0,x1) = M;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = h0 [^] r ⊗ ❙g [^] (if σ then (1::nat) else 0);
let b1 = h1 [^] r ⊗ ❙g [^] (if σ then (1::nat) else 0);
let h = h0 ⊗ inv h1;
let b = b0 ⊗ inv b1;
_ :: unit ← assert_spmf (a = ❙g [^] r ∧ b = h [^] r);
u0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let w0 = a [^] u0 ⊗ ❙g [^] v0;
let e0 = (w0, z0);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let w1 = a [^] u1 ⊗ ❙g [^] v1;
let e1 = (w1, z1);
return_spmf ((), (if σ then (z1 ⊗ inv (w1 [^] α1)) else (z0 ⊗ inv (w0 [^] α0))))}"
text‹Party 1 sends three messages (including the output) in the protocol so we split the adversary into three parts, one part
to output each message. The real view of the protocol for party 1 outputs the correct output for party 2
and the adversary outputs the output for party 1.›
definition P1_real_model :: "('grp × 'grp) ⇒ bool ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out1, 'state) adv_mal_P1 ⇒ ('adv_out1 × 'grp) spmf"
where "P1_real_model M σ z 𝒜 = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = h0 [^] r ⊗ (if σ then ❙g else 𝟭);
let b1 = h1 [^] r ⊗ (if σ then ❙g else 𝟭);
((in1 :: 'grp, in2 ::'grp, in3 :: 'grp), s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(b :: bool, _ :: unit) ← funct_DH_ZK (in1, in2, in3) ((h,a,b), r);
_ :: unit ← assert_spmf (b);
(((w0,z0),(w1,z1)), s') ← 𝒜2 h0 h1 a b0 b1 M s;
adv_out :: 'adv_out1 ← 𝒜3 s';
return_spmf (adv_out, (if σ then (z1 ⊗ (inv w1 [^] α1)) else (z0 ⊗ (inv w0 [^] α0))))}"
text‹The first and second part of the simulator for party 1 are defined below.›
definition P1_S1 :: "('aux, 'grp, 'adv_out1, 'state) adv_mal_P1 ⇒ ('grp × 'grp) ⇒ 'aux ⇒ (('grp × 'grp) × 'state) spmf"
where "P1_S1 𝒜 M z = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = h0 [^] r;
let b1 = h1 [^] r ⊗ ❙g;
((in1 :: 'grp, in2 ::'grp, in3 :: 'grp), s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
_ :: unit ← assert_spmf ((in1, in2, in3) = (h,a,b));
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
let x0 = (z0 ⊗ (inv w0 [^] α0));
let x1 = (z1 ⊗ (inv w1 [^] α1));
return_spmf ((x0,x1), s')}"
definition P1_S2 :: "('aux, 'grp, 'adv_out1,'state) adv_mal_P1 ⇒ ('grp × 'grp) ⇒ 'aux ⇒ unit ⇒ 'state ⇒ 'adv_out1 spmf"
where "P1_S2 𝒜 M z out1 s' = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
𝒜3 s'}"
text‹We explicitly provide the unfolded definition of the ideal model for convieience in the proof.›
definition P1_ideal_model :: "('grp × 'grp) ⇒ bool ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out1,'state) adv_mal_P1 ⇒ ('adv_out1 × 'grp) spmf"
where "P1_ideal_model M σ z 𝒜 = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = h0 [^] r;
let b1 = h1 [^] r ⊗ ❙g;
((in1 :: 'grp, in2 ::'grp, in3 :: 'grp), s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
_ :: unit ← assert_spmf ((in1, in2, in3) = (h,a,b));
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
let x0' = z0 ⊗ inv w0 [^] α0;
let x1' = z1 ⊗ inv w1 [^] α1;
(_, f_out2) ← funct_OT_12 (x0', x1') σ;
adv_out :: 'adv_out1 ← 𝒜3 s';
return_spmf (adv_out, f_out2)}"
text‹The advantage associated with the unfolded definition of the ideal view.›
definition
"P1_adv_real_ideal_model (D :: ('adv_out1 × 'grp) ⇒ bool spmf) M σ 𝒜 z
= ¦spmf ((P1_real_model M σ z 𝒜) ⤜ (λ view. D view)) True
- spmf ((P1_ideal_model M σ z 𝒜) ⤜ (λ view. D view)) True¦"
text‹We now define the real view and simulators for party 2 in an analogous way.›
definition P2_real_model :: "('grp × 'grp) ⇒ bool ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out2,'state) adv_mal_P2 ⇒ (unit × 'adv_out2) spmf"
where "P2_real_model M σ z 𝒜 = do {
let (x0,x1) = M;
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3 :: 'grp), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
u0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let w0 = a [^] u0 ⊗ ❙g [^] v0;
let e0 = (w0, z0);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let w1 = a [^] u1 ⊗ ❙g [^] v1;
let e1 = (w1, z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
definition P2_S1 :: "('aux, 'grp, 'adv_out2,'state) adv_mal_P2 ⇒ bool ⇒ 'aux ⇒ (bool × ('grp × 'grp × 'grp × 'grp × 'grp) × 'state) spmf"
where "P2_S1 𝒜 σ z = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3 :: 'grp), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
let l = b0 ⊗ (inv (h0 [^] r));
return_spmf ((if l = 𝟭 then False else True), (h0,h1,a,b0,b1), s')}"
definition P2_S2 :: "('aux, 'grp, 'adv_out2,'state) adv_mal_P2 ⇒ bool ⇒ 'aux ⇒ 'grp ⇒ (('grp × 'grp × 'grp × 'grp × 'grp) × 'state) ⇒ 'adv_out2 spmf"
where "P2_S2 𝒜 σ' z xσ aux_out = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
let ((h0,h1,a,b0,b1),s) = aux_out;
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = a [^] u0 ⊗ ❙g [^] v0;
let w1 = a [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ (if σ' then 𝟭 else xσ);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ (if σ' then xσ else 𝟭);
let e0 = (w0,z0);
let e1 = (w1,z1);
𝒜3 e0 e1 s}"
sublocale mal_def : malicious_base funct_OT_12 protocol_ot P1_S1 P1_S2 P1_real_model P2_S1 P2_S2 P2_real_model .
text‹We prove the unfolded definition of the ideal views are equal to the definition we provide in the
abstract locale that defines security.›
lemma P1_ideal_ideal_eq:
shows "mal_def.ideal_view_1 x y z (P1_S1, P1_S2) 𝒜 = P1_ideal_model x y z 𝒜"
including monad_normalisation
unfolding mal_def.ideal_view_1_def mal_def.ideal_game_1_def P1_ideal_model_def P1_S1_def P1_S2_def Let_def split_def
by(simp add: split_def)
lemma P1_advantages_eq:
shows "mal_def.adv_P1 x y z (P1_S1, P1_S2) 𝒜 D = P1_adv_real_ideal_model D x y 𝒜 z"
by(simp add: mal_def.adv_P1_def P1_adv_real_ideal_model_def P1_ideal_ideal_eq)
fun P1_DDH_mal_adv_σ_false :: "('grp × 'grp) ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out1,'state) adv_mal_P1 ⇒ (('adv_out1 × 'grp) ⇒ bool spmf) ⇒ 'grp ddh.adversary"
where "P1_DDH_mal_adv_σ_false M z 𝒜 D h a t = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
α0 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = h;
let b0 = a [^] α0;
let b1 = t;
((in1 :: 'grp, in2 ::'grp, in3 :: 'grp),s) ← 𝒜1 M h0 h1 a b0 b1 z;
_ :: unit ← assert_spmf (in1 = h0 ⊗ inv h1 ∧ in2 = a ∧ in3 = b0 ⊗ inv b1);
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
let x0 = (z0 ⊗ (inv w0 [^] α0));
adv_out :: 'adv_out1 ← 𝒜3 s';
D (adv_out, x0)}"
fun P1_DDH_mal_adv_σ_true :: "('grp × 'grp) ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out1,'state) adv_mal_P1 ⇒ (('adv_out1 × 'grp) ⇒ bool spmf) ⇒ 'grp ddh.adversary"
where "P1_DDH_mal_adv_σ_true M z 𝒜 D h a t = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
α1 :: nat ← sample_uniform (order 𝒢);
let h1 = ❙g [^] α1;
let h0 = h;
let b0 = t;
let b1 = a [^] α1 ⊗ ❙g;
((in1 :: 'grp, in2 ::'grp, in3 :: 'grp),s) ← 𝒜1 M h0 h1 a b0 b1 z;
_ :: unit ← assert_spmf (in1 = h0 ⊗ inv h1 ∧ in2 = a ∧ in3 = b0 ⊗ inv b1);
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
let x1 = (z1 ⊗ (inv w1 [^] α1));
adv_out :: 'adv_out1 ← 𝒜3 s';
D (adv_out, x1)}"
definition P2_ideal_model :: "('grp × 'grp) ⇒ bool ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out2, 'state) adv_mal_P2 ⇒ (unit × 'adv_out2) spmf"
where "P2_ideal_model M σ z 𝒜 = do {
let (x0,x1) = M;
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1), s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
let l = b0 ⊗ (inv (h0 [^] r));
let σ' = (if l = 𝟭 then False else True);
(_ :: unit, xσ) ← funct_OT_12 (x0, x1) σ';
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = a [^] u0 ⊗ ❙g [^] v0;
let w1 = a [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ (if σ' then 𝟭 else xσ);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ (if σ' then xσ else 𝟭);
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
definition P2_ideal_model_end :: "('grp × 'grp) ⇒ 'grp ⇒ (('grp × 'grp × 'grp × 'grp × 'grp) × 'state)
⇒ ('grp, 'adv_out2, 'state) adv_3_P2 ⇒ (unit × 'adv_out2) spmf"
where "P2_ideal_model_end M l bs 𝒜3 = do {
let (x0,x1) = M;
let ((h0,h1,a,b0,b1),s) = bs;
let σ' = (if l = 𝟭 then False else True);
(_:: unit, xσ) ← funct_OT_12 (x0, x1) σ';
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = a [^] u0 ⊗ ❙g [^] v0;
let w1 = a [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ (if σ' then 𝟭 else xσ);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ (if σ' then xσ else 𝟭);
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s;
return_spmf ((), out)}"
definition P2_ideal_model' :: "('grp × 'grp) ⇒ bool ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out2, 'state) adv_mal_P2 ⇒ (unit × 'adv_out2) spmf"
where "P2_ideal_model' M σ z 𝒜 = do {
let (x0,x1) = M;
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3 :: 'grp), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
let l = b0 ⊗ (inv (h0 [^] r));
P2_ideal_model_end (x0,x1) l ((h0,h1,a,b0,b1),s') 𝒜3}"
lemma P2_ideal_model_rewrite: "P2_ideal_model M σ z 𝒜 = P2_ideal_model' M σ z 𝒜 "
by(simp add: P2_ideal_model'_def P2_ideal_model_def P2_ideal_model_end_def Let_def split_def)
definition P2_real_model_end :: "('grp × 'grp) ⇒ (('grp × 'grp × 'grp × 'grp × 'grp) × 'state)
⇒ ('grp, 'adv_out2,'state) adv_3_P2 ⇒ (unit × 'adv_out2) spmf"
where "P2_real_model_end M bs 𝒜3 = do {
let (x0,x1) = M;
let ((h0,h1,a,b0,b1),s) = bs;
u0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let w0 = a [^] u0 ⊗ ❙g [^] v0;
let e0 = (w0, z0);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let w1 = a [^] u1 ⊗ ❙g [^] v1;
let e1 = (w1, z1);
out ← 𝒜3 e0 e1 s;
return_spmf ((), out)}"
definition P2_real_model' ::"('grp × 'grp) ⇒ bool ⇒ 'aux ⇒ ('aux, 'grp, 'adv_out2, 'state) adv_mal_P2 ⇒ (unit × 'adv_out2) spmf"
where "P2_real_model' M σ z 𝒜 = do {
let (x0,x1) = M;
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3 :: 'grp), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
P2_real_model_end M ((h0,h1,a,b0,b1),s') 𝒜3}"
lemma P2_real_model_rewrite: "P2_real_model M σ z 𝒜 = P2_real_model' M σ z 𝒜"
by(simp add: P2_real_model'_def P2_real_model_def P2_real_model_end_def split_def)
lemma P2_ideal_view_unfold: "mal_def.ideal_view_2 (x0,x1) σ z (P2_S1, P2_S2) 𝒜 = P2_ideal_model (x0,x1) σ z 𝒜"
unfolding local.mal_def.ideal_view_2_def P2_ideal_model_def local.mal_def.ideal_game_2_def P2_S1_def P2_S2_def
by(auto simp add: Let_def split_def)
end
locale ot = ot_base + cyclic_group 𝒢
begin
lemma P1_assert_correct1:
shows "((❙g [^] (α0::nat)) [^] (r::nat) ⊗ ❙g ⊗ inv ((❙g [^] (α1::nat)) [^] r ⊗ ❙g)
= (❙g [^] α0 ⊗ inv (❙g [^] α1)) [^] r)"
(is "?lhs = ?rhs")
proof-
have in_carrier1: "(❙g [^] α1) [^] r ∈ carrier 𝒢" by simp
have in_carrier2: "inv ((❙g [^] α1) [^] r) ∈ carrier 𝒢" by simp
have 1:"?lhs = (❙g [^] α0) [^] r ⊗ ❙g ⊗ inv ((❙g [^] α1) [^] r) ⊗ inv ❙g"
using cyclic_group_assoc nat_pow_pow inverse_split in_carrier1 by simp
also have 2:"... = (❙g [^] α0) [^] r ⊗ (❙g ⊗ inv ((❙g [^] α1) [^] r)) ⊗ inv ❙g"
using cyclic_group_assoc in_carrier2 by simp
also have "... = (❙g [^] α0) [^] r ⊗ (inv ((❙g [^] α1) [^] r) ⊗ ❙g) ⊗ inv ❙g"
using in_carrier2 cyclic_group_commute by simp
also have 3: "... = (❙g [^] α0) [^] r ⊗ inv ((❙g [^] α1) [^] r) ⊗ (❙g ⊗ inv ❙g)"
using cyclic_group_assoc in_carrier2 by simp
also have "... = (❙g [^] α0) [^] r ⊗ inv ((❙g [^] α1) [^] r)" by simp
also have "... = (❙g [^] α0) [^] r ⊗ inv ((❙g [^] α1)) [^] r"
using inverse_pow_pow by simp
ultimately show ?thesis
by (simp add: cyclic_group_commute pow_mult_distrib)
qed
lemma P1_assert_correct2:
shows "(❙g [^] (α0::nat)) [^] (r::nat) ⊗ inv ((❙g [^] (α1::nat)) [^] r) = (❙g [^] α0 ⊗ inv (❙g [^] α1)) [^] r"
(is "?lhs = ?rhs")
proof-
have in_carrier2:"❙g [^] α1 ∈ carrier 𝒢" by simp
hence "?lhs = (❙g [^] α0) [^] r ⊗ inv ((❙g [^] α1)) [^] r"
using inverse_pow_pow by simp
thus ?thesis
by (simp add: cyclic_group_commute monoid_comm_monoidI pow_mult_distrib)
qed
sublocale ddh: ddh_ext
by (simp add: cyclic_group_axioms ddh_ext.intro)
lemma P1_real_ddh0_σ_false:
assumes "σ = False"
shows "((P1_real_model M σ z 𝒜) ⤜ (λ view. D view)) = (ddh.DDH0 (P1_DDH_mal_adv_σ_false M z 𝒜 D))"
including monad_normalisation
proof-
have
"(in2 = ❙g [^] (r::nat) ∧ in3 = in1 [^] r ∧ in1 = ❙g [^] (α0::nat) ⊗ inv (❙g [^] (α1::nat))
∧ in2 = ❙g [^] r ∧ in3 = (❙g [^] r) [^] α0 ⊗ inv ((❙g [^] α1) [^] r))
⟷ (in1 = ❙g [^] α0 ⊗ inv (❙g [^] α1) ∧ in2 = ❙g [^] r ∧ in3
= (❙g [^] r) [^] α0 ⊗ inv ((❙g [^] α1) [^] r))"
for in1 in2 in3 r α0 α1
by (auto simp add: P1_assert_correct2 power_swap)
moreover have "((P1_real_model M σ z 𝒜) ⤜ (λ view. D view)) = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = (❙g [^] r) [^] α0;
let b1 = h1 [^] r;
((in1, in2, in3),s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(b :: bool, _ :: unit) ← funct_DH_ZK (in1, in2, in3) ((h,a,b), r);
_ :: unit ← assert_spmf (b);
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
adv_out ← 𝒜3 s';
D (adv_out, ((z0 ⊗ (inv w0 [^] α0))))}"
by(simp add: P1_real_model_def assms split_def Let_def power_swap)
ultimately show ?thesis
by(simp add: P1_real_model_def ddh.DDH0_def Let_def)
qed
lemma P1_ideal_ddh1_σ_false:
assumes "σ = False"
shows "((P1_ideal_model M σ z 𝒜) ⤜ (λ view. D view)) = (ddh.DDH1 (P1_DDH_mal_adv_σ_false M z 𝒜 D))"
including monad_normalisation
proof-
have "((P1_ideal_model M σ z 𝒜) ⤜ (λ view. D view)) = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = (❙g [^] r) [^] α0;
let b1 = h1 [^] r ⊗ ❙g;
((in1, in2, in3),s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
_ :: unit ← assert_spmf ((in1, in2, in3) = (h,a,b));
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
let x0 = (z0 ⊗ (inv w0 [^] α0));
let x1 = (z1 ⊗ (inv w1 [^] α1));
(_, f_out2) ← funct_OT_12 (x0, x1) σ;
adv_out ← 𝒜3 s';
D (adv_out, f_out2)}"
by(simp add: P1_ideal_model_def assms split_def Let_def power_swap)
thus ?thesis
by(auto simp add: P1_ideal_model_def ddh.DDH1_def funct_OT_12_def Let_def assms )
qed
lemma P1_real_ddh1_σ_true:
assumes "σ = True"
shows "((P1_real_model M σ z 𝒜) ⤜ (λ view. D view)) = (ddh.DDH1 (P1_DDH_mal_adv_σ_true M z 𝒜 D))"
including monad_normalisation
proof-
have "(in2 = ❙g [^] (r::nat) ∧ in3 = in1 [^] r ∧ in1 = ❙g [^] (α0::nat) ⊗ inv (❙g [^] (α1::nat))
∧ in2 = ❙g [^] r ∧ in3 = (❙g [^] r) [^] α0 ⊗ ❙g ⊗ inv ((❙g [^] α1) [^] r ⊗ ❙g))
⟷ (in1 = ❙g [^] α0 ⊗ inv (❙g [^] α1) ∧ in2 = ❙g [^] r
∧ in3 = (❙g [^] α0) [^] r ⊗ ❙g ⊗ inv ((❙g [^] r) [^] α1 ⊗ ❙g))"
for in1 in2 in3 r α0 α1
by (auto simp add: P1_assert_correct1 power_swap)
moreover have "((P1_real_model M σ z 𝒜) ⤜ (λ view. D view)) = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = ((❙g [^] r) [^] α0) ⊗ ❙g;
let b1 = (h1 [^] r) ⊗ ❙g;
((in1, in2, in3),s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(b :: bool, _ :: unit) ← funct_DH_ZK (in1, in2, in3) ((h,a,b), r);
_ :: unit ← assert_spmf (b);
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
adv_out ← 𝒜3 s';
D (adv_out, ((z1 ⊗ (inv w1 [^] α1))))}"
by(simp add: P1_real_model_def assms split_def Let_def power_swap)
ultimately show ?thesis
by(simp add: Let_def P1_real_model_def ddh.DDH1_def assms power_swap)
qed
lemma P1_ideal_ddh0_σ_true:
assumes "σ = True"
shows "((P1_ideal_model M σ z 𝒜) ⤜ (λ view. D view)) = (ddh.DDH0 (P1_DDH_mal_adv_σ_true M z 𝒜 D))"
including monad_normalisation
proof-
have "((P1_ideal_model M σ z 𝒜) ⤜ (λ view. D view)) = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
r ← sample_uniform (order 𝒢);
α0 ← sample_uniform (order 𝒢);
α1 ← sample_uniform (order 𝒢);
let h0 = ❙g [^] α0;
let h1 = ❙g [^] α1;
let a = ❙g [^] r;
let b0 = (❙g [^] r) [^] α0;
let b1 = h1 [^] r ⊗ ❙g;
((in1, in2, in3),s) ← 𝒜1 M h0 h1 a b0 b1 z;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
_ :: unit ← assert_spmf ((in1, in2, in3) = (h,a,b));
(((w0,z0),(w1,z1)),s') ← 𝒜2 h0 h1 a b0 b1 M s;
let x0 = (z0 ⊗ (inv w0 [^] α0));
let x1 = (z1 ⊗ (inv w1 [^] α1));
(_, f_out2) ← funct_OT_12 (x0, x1) σ;
adv_out ← 𝒜3 s';
D (adv_out, f_out2)}"
by(simp add: P1_ideal_model_def assms Let_def split_def power_swap)
thus ?thesis
by(simp add: split_def Let_def P1_ideal_model_def ddh.DDH0_def assms funct_OT_12_def power_swap)
qed
lemma P1_real_ideal_DDH_advantage_false:
assumes "σ = False"
shows "mal_def.adv_P1 M σ z (P1_S1, P1_S2) 𝒜 D = ddh.DDH_advantage (P1_DDH_mal_adv_σ_false M z 𝒜 D)"
by(simp add: P1_adv_real_ideal_model_def ddh.DDH_advantage_def P1_ideal_ddh1_σ_false P1_real_ddh0_σ_false assms P1_advantages_eq)
lemma P1_real_ideal_DDH_advantage_false_bound:
assumes "σ = False"
shows "mal_def.adv_P1 M σ z (P1_S1, P1_S2) 𝒜 D
≤ ddh.advantage (P1_DDH_mal_adv_σ_false M z 𝒜 D)
+ ddh.advantage (ddh.DDH_𝒜' (P1_DDH_mal_adv_σ_false M z 𝒜 D))"
using P1_real_ideal_DDH_advantage_false ddh.DDH_advantage_bound assms by metis
lemma P1_real_ideal_DDH_advantage_true:
assumes "σ = True"
shows "mal_def.adv_P1 M σ z (P1_S1, P1_S2) 𝒜 D = ddh.DDH_advantage (P1_DDH_mal_adv_σ_true M z 𝒜 D)"
by(simp add: P1_adv_real_ideal_model_def ddh.DDH_advantage_def P1_real_ddh1_σ_true P1_ideal_ddh0_σ_true assms P1_advantages_eq)
lemma P1_real_ideal_DDH_advantage_true_bound:
assumes "σ = True"
shows "mal_def.adv_P1 M σ z (P1_S1, P1_S2) 𝒜 D
≤ ddh.advantage (P1_DDH_mal_adv_σ_true M z 𝒜 D)
+ ddh.advantage (ddh.DDH_𝒜' (P1_DDH_mal_adv_σ_true M z 𝒜 D))"
using P1_real_ideal_DDH_advantage_true ddh.DDH_advantage_bound assms by metis
lemma P2_output_rewrite:
assumes "s < order 𝒢"
shows "(❙g [^] (r * u1 + v1), ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] u1)
= (❙g [^] (r * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢),
❙g [^] (r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α)
⊗ inv ❙g [^] ((s + u1) mod order 𝒢 + (order 𝒢 - s)))"
proof-
have "❙g [^] (r * u1 + v1) = ❙g [^] (r * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢)"
proof-
have "[(r * u1 + v1) = (r * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢)] (mod (order 𝒢))"
proof-
have "[(r * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢) = r * (s + u1) + (r * order 𝒢 - r * s + v1)] (mod (order 𝒢))"
by (metis (no_types, opaque_lifting) cong_def mod_add_left_eq mod_add_right_eq mod_mult_right_eq)
hence "[(r * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢) = r * s + r * u1 + r * order 𝒢 - r * s + v1] (mod (order 𝒢))"
by (metis (no_types, lifting) Nat.add_diff_assoc add.assoc assms distrib_left less_or_eq_imp_le mult_le_mono)
hence "[(r * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢) = r * u1 + r * order 𝒢 + v1] (mod (order 𝒢))" by simp
thus ?thesis
by (simp add: cong_def semiring_normalization_rules(23))
qed
then show ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
moreover have " ❙g [^] (r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α)
⊗ inv ❙g [^] ((s + u1) mod order 𝒢 + (order 𝒢 - s))
= ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] u1"
proof-
have "❙g [^] (r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α) = ❙g [^] (r * α * u1 + v1 * α)"
proof-
have "[(r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α) = r * α * u1 + v1 * α] (mod (order 𝒢))"
proof-
have "[(r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α)
= r * α * (s + u1) + (r * order 𝒢 - r * s + v1) * α] (mod (order 𝒢))"
using cong_def mod_add_cong mod_mult_left_eq mod_mult_right_eq by blast
hence "[(r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α)
= r * α * s + r * α * u1 + (r * order 𝒢 - r * s + v1) * α] (mod (order 𝒢))"
by (simp add: distrib_left)
hence "[(r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α)
= r * α * s + r * α * u1 + r * order 𝒢 * α - r * s * α + v1 * α] (mod (order 𝒢))" using distrib_right assms
by (smt Groups.mult_ac(3) order_gt_0 Nat.add_diff_assoc2 add.commute diff_mult_distrib2 mult.commute mult_strict_mono order.strict_implies_order semiring_normalization_rules(25) zero_order(1))
hence "[(r * α * ((s + u1) mod order 𝒢) + (r * order 𝒢 - r * s + v1) mod order 𝒢 * α)
= r * α * u1 + r * order 𝒢 * α + v1 * α] (mod (order 𝒢))" by simp
thus ?thesis
by (simp add: cong_def semiring_normalization_rules(16) semiring_normalization_rules(23))
qed
thus ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
also have "inv ❙g [^] ((s + u1) mod order 𝒢 + (order 𝒢 - s)) = inv ❙g [^] u1"
proof-
have "[((s + u1) mod order 𝒢 + (order 𝒢 - s)) = u1] (mod (order 𝒢))"
proof-
have "[((s + u1) mod order 𝒢 + (order 𝒢 - s)) = s + u1 + (order 𝒢 - s)] (mod (order 𝒢))"
by (simp add: add.commute mod_add_right_eq cong_def)
hence "[((s + u1) mod order 𝒢 + (order 𝒢 - s)) = u1 + order 𝒢] (mod (order 𝒢))"
using assms by simp
thus ?thesis by (simp add: cong_def)
qed
hence "❙g [^] ((s + u1) mod order 𝒢 + (order 𝒢 - s)) = ❙g [^] u1"
using finite_group pow_generator_eq_iff_cong by blast
thus ?thesis
by (metis generator_closed inverse_pow_pow)
qed
ultimately show ?thesis by argo
qed
ultimately show ?thesis by simp
qed
lemma P2_inv_g_rewrite:
assumes "s < order 𝒢"
shows "(inv ❙g) [^] (u1' + (order 𝒢 - s)) = ❙g [^] s ⊗ inv (❙g [^] u1')"
proof-
have power_commute_rewrite: "❙g [^] (((order 𝒢 - s) + u1') mod order 𝒢) = ❙g [^] (u1' + (order 𝒢 - s))"
using add.commute pow_generator_mod by metis
have "(order 𝒢 - s + u1') mod order 𝒢 = (int (order 𝒢) - int s + int u1') mod order 𝒢"
by (metis of_nat_add of_nat_diff order.strict_implies_order zmod_int assms(1))
also have "... = (- int s + int u1') mod order 𝒢"
by (metis (full_types) add.commute minus_mod_self1 mod_add_right_eq)
ultimately have "(order 𝒢 - s + u1') mod order 𝒢 = (- int s mod (order 𝒢) + int u1' mod (order 𝒢)) mod order 𝒢"
by presburger
hence "❙g [^] (((order 𝒢 - s) + u1') mod order 𝒢)
= ❙g [^] ((- int s mod (order 𝒢) + int u1' mod (order 𝒢)) mod order 𝒢)"
by (metis int_pow_int)
hence "❙g [^] (u1' + (order 𝒢 - s))
= ❙g [^] ((- int s mod (order 𝒢) + int u1' mod (order 𝒢)) mod order 𝒢)"
using power_commute_rewrite by argo
also have "...
= ❙g [^] (- int s mod (order 𝒢) + int u1' mod (order 𝒢))"
using pow_generator_mod_int by blast
also have "... = ❙g [^] (- int s mod (order 𝒢)) ⊗ ❙g [^] (int u1' mod (order 𝒢))"
by (simp add: int_pow_mult)
also have "... = ❙g [^] (- int s) ⊗ ❙g [^] (int u1')"
using pow_generator_mod_int by simp
ultimately have "inv (❙g [^] (u1' + (order 𝒢 - s))) = inv (❙g [^] (- int s) ⊗ ❙g [^] (int u1'))" by simp
hence "inv (❙g [^] ((u1' + (order 𝒢 - s)) mod (order 𝒢)) ) = inv (❙g [^] (- int s)) ⊗ inv (❙g [^] (int u1'))"
using pow_generator_mod
by (simp add: inverse_split)
also have "... = ❙g [^] (int s) ⊗ inv (❙g [^] (int u1'))"
by (simp add: int_pow_neg)
also have "... = ❙g [^] s ⊗ inv (❙g [^] u1')"
by (simp add: int_pow_int)
ultimately show ?thesis
by (simp add: inverse_pow_pow pow_generator_mod )
qed
lemma P2_inv_g_s_rewrite:
assumes "s < order 𝒢"
shows "❙g [^] ((r::nat) * α * u1 + v1 * α) ⊗ inv ❙g [^] (u1 + (order 𝒢 - s)) = ❙g [^] (r * α * u1 + v1 * α) ⊗ ❙g [^] s ⊗ inv ❙g [^] u1"
proof-
have in_carrier1: "inv ❙g [^] (u1 + (order 𝒢 - s)) ∈ carrier 𝒢" by blast
have in_carrier2: "inv ❙g [^] u1 ∈ carrier 𝒢" by simp
have in_carrier_3: "❙g [^] (r * α * u1 + v1 * α) ∈ carrier 𝒢" by simp
have "❙g [^] (r * α * u1 + v1 * α) ⊗ (inv ❙g [^] (u1 + (order 𝒢 - s))) = ❙g [^] (r * α * u1 + v1 * α) ⊗ (❙g [^] s ⊗ inv ❙g [^] u1)"
using P2_inv_g_rewrite assms
by (simp add: inverse_pow_pow)
thus ?thesis using cyclic_group_assoc in_carrier1 in_carrier2 by auto
qed
lemma P2_e0_rewrite:
assumes "s < order 𝒢 "
shows "(❙g [^] (r * x + xa), ❙g [^] (r * α * x + xa * α) ⊗ ❙g [^] x) =
(❙g [^] (r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢),
❙g [^] (r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
⊗ ❙g [^] ((order 𝒢 - s + x) mod order 𝒢 + s))"
proof-
have "❙g [^] (r * x + xa) = ❙g [^] (r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)"
proof-
have "[(r * x + xa) = (r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)] (mod order 𝒢)"
proof-
have "[(r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)
= (r * ((order 𝒢 - s + x)) + (r * s + xa))] (mod order 𝒢)"
by (metis (no_types, lifting) mod_mod_trivial cong_add cong_def mod_mult_right_eq)
hence "[(r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)
= r * (order 𝒢 - s) + r * x + r * s + xa] (mod order 𝒢)"
by (simp add: add.assoc distrib_left)
hence "[(r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)
= r * x + r * s + r * (order 𝒢 - s) + xa] (mod order 𝒢)"
by (metis add.assoc add.commute)
hence "[(r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)
= r * x + r * s + r * order 𝒢 - r * s + xa] (mod order 𝒢)"
proof -
have "[(xa + r * s) mod order 𝒢 + r * ((x + (order 𝒢 - s)) mod order 𝒢) = xa + r * (s + x + (order 𝒢 - s))] (mod order 𝒢)"
by (metis (no_types) ‹[r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 = r * x + r * s + r * (order 𝒢 - s) + xa] (mod order 𝒢)› add.commute distrib_left)
then show ?thesis
by (simp add: assms add.commute distrib_left order.strict_implies_order)
qed
hence "[(r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢)
= r * x + xa] (mod order 𝒢)"
proof -
have "[(xa + r * s) mod order 𝒢 + r * ((x + (order 𝒢 - s)) mod order 𝒢) = xa + (r * x + r * order 𝒢)] (mod order 𝒢)"
by (metis (no_types) ‹[r * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 = r * x + r * s + r * order 𝒢 - r * s + xa] (mod order 𝒢)› add.commute add.left_commute add_diff_cancel_left')
then show ?thesis
by (metis (no_types) add.commute cong_add_lcancel_nat cong_def distrib_left mod_add_self2 mod_mult_right_eq)
qed
then show ?thesis using cong_def by metis
qed
then show ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
moreover have "❙g [^] (r * α * x + xa * α) ⊗ ❙g [^] x =
❙g [^] (r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
⊗ ❙g [^] ((order 𝒢 - s + x) mod order 𝒢 + s)"
proof-
have "❙g [^] (r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= ❙g [^] (r * α * x + xa * α)"
proof-
have "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α) = r * α * x + xa * α] (mod order 𝒢)"
proof-
have "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= (r * α * ((order 𝒢 - s) + x) + (r * s + xa) * α)] (mod order 𝒢)"
by (metis (no_types, lifting) cong_add cong_def mod_mult_left_eq mod_mult_right_eq)
hence "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= r * α * (order 𝒢 - s) + r * α * x + r * s * α + xa * α] (mod order 𝒢)"
by (simp add: add.assoc distrib_left distrib_right)
hence "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= r * α * x + r * s * α + r * α * (order 𝒢 - s) + xa * α] (mod order 𝒢)"
by (simp add: add.commute add.left_commute)
hence "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= r * α * x + r * s * α + r * α * order 𝒢 - r * α * s + xa * α] (mod order 𝒢)"
proof -
have "∀n na. ¬ (n::nat) ≤ na ∨ n + (na - n) = na"
by (meson ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
then have "r * α * s + r * α * (order 𝒢 - s) = r * α * order 𝒢"
by (metis add_mult_distrib2 assms less_or_eq_imp_le)
then have "r * α * x + r * s * α + r * α * order 𝒢 = r * α * s + r * α * (order 𝒢 - s) + (r * α * x + r * s * α)"
by presburger
then have f1: "r * α * x + r * s * α + r * α * order 𝒢 - r * α * s = r * α * s + r * α * (order 𝒢 - s) - r * α * s + (r * α * x + r * s * α)"
by simp
have "r * α * s + r * α * (order 𝒢 - s) = r * α * (order 𝒢 - s) + r * α * s"
by presburger
then have "r * α * x + r * s * α + r * α * order 𝒢 - r * α * s = r * α * x + r * s * α + r * α * (order 𝒢 - s)"
using f1 diff_add_inverse2 by presburger
then show ?thesis
using ‹[r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α = r * α * x + r * s * α + r * α * (order 𝒢 - s) + xa * α] (mod order 𝒢)› by presburger
qed
hence "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= r * α * x + r * α * s + r * α * order 𝒢 - r * α * s + xa * α] (mod order 𝒢)"
using add.commute add.assoc by force
hence "[(r * α * ((order 𝒢 - s + x) mod order 𝒢) + (r * s + xa) mod order 𝒢 * α)
= r * α * x + r * α * order 𝒢 + xa * α] (mod order 𝒢)" by simp
thus ?thesis using cong_def semiring_normalization_rules(23)
by (simp add: ‹⋀c b a. [b = c] (mod a) = (b mod a = c mod a)› ‹⋀c b a. a + b + c = a + c + b›)
qed
thus ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
also have "❙g [^] ((order 𝒢 - s + x) mod order 𝒢 + s) = ❙g [^] x"
proof-
have "[((order 𝒢 - s + x) mod order 𝒢 + s) = x] (mod order 𝒢)"
proof-
have "[((order 𝒢 - s + x) mod order 𝒢 + s) = (order 𝒢 - s + x+ s)] (mod order 𝒢)"
by (simp add: add.commute cong_def mod_add_right_eq)
hence "[((order 𝒢 - s + x) mod order 𝒢 + s) = (order 𝒢 + x)] (mod order 𝒢)"
using assms by auto
thus ?thesis
by (simp add: cong_def)
qed
thus ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
ultimately show ?thesis by argo
qed
ultimately show ?thesis by simp
qed
lemma P2_case_l_new_1_gt_e0_rewrite:
assumes "s < order 𝒢"
shows "(❙g [^] (r * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢),
❙g [^] (r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α) ⊗
❙g [^] (t * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢
+ s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))) = (❙g [^] (r * x + xa), ❙g [^] (r * α * x + xa * α) ⊗ ❙g [^] (t * x))"
proof-
have "❙g [^] ((r::nat) * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢)
= ❙g [^] (r * x + xa)"
proof(cases "r = 0")
case True
then show ?thesis
by (simp add: pow_generator_mod)
next
case False
have "[(r::nat) * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 = r * x + xa] (mod order 𝒢)"
proof-
have "[r * ((order 𝒢 * order 𝒢 - s * (nat (fst (bezw t (order 𝒢))) mod order 𝒢) + x) mod order 𝒢)
+ (r * s * nat (fst (bezw t (order 𝒢))) + xa) mod order 𝒢
= (r * (((order 𝒢 * order 𝒢 - s * (nat (fst (bezw t (order 𝒢))) mod order 𝒢)) + x))
+ (r * s * nat (fst (bezw t (order 𝒢))) + xa))] (mod order 𝒢)"
proof -
have "order 𝒢 ≠ 0"
using order_gt_0 by simp
then show ?thesis
using cong_add cong_def mod_mult_right_eq
by (smt mod_mod_trivial)
qed
hence "[r * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢
= r * (order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))) + r * x
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa)] (mod order 𝒢)"
proof -
have "[r * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
= r * (order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))) + r * x] (mod order 𝒢)"
by (simp add: cong_def distrib_left mod_mult_right_eq)
then show ?thesis
using assms cong_add gr_implies_not0 by fastforce
qed
hence "[r * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢
= r * order 𝒢 * order 𝒢 - r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + r * x
+ r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa] (mod order 𝒢)"
by (simp add: ab_semigroup_mult_class.mult_ac(1) right_diff_distrib' add.assoc)
hence "[r * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢
= r * order 𝒢 * order 𝒢 + r * x + xa] (mod order 𝒢)"
proof-
have "r * order 𝒢 * order 𝒢 - r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) > 0"
proof-
have "order 𝒢 * order 𝒢 > s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))"
proof-
have "(nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) ≤ order 𝒢"
proof -
have "∀x0 x1. ((x0::int) mod x1 < x1) = (¬ x1 + - 1 * (x0 mod x1) ≤ 0)"
by linarith
then have "¬ int (order 𝒢) + - 1 * (fst (bezw t (order 𝒢)) mod int (order 𝒢)) ≤ 0"
using of_nat_0_less_iff order_gt_0 by fastforce
then show ?thesis
by linarith
qed
thus ?thesis using assms
proof -
have "∀n na. ¬ n ≤ na ∨ ¬ na * order 𝒢 < n * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢))"
by (meson ‹nat (fst (bezw (t::nat) (order 𝒢)) mod int (order 𝒢)) ≤ order 𝒢› mult_le_mono not_le)
then show ?thesis
by(metis (no_types, opaque_lifting) ‹(s::nat) < order 𝒢› mult_less_cancel2 nat_less_le not_le not_less_zero)
qed
qed
thus ?thesis using False
by auto
qed
thus ?thesis
proof -
have "r * order 𝒢 * order 𝒢 + r * x + xa = r * (order 𝒢 * order 𝒢 - s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢))) + (r * s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) + xa) + r * x"
using ‹(0::nat) < (r::nat) * order 𝒢 * order 𝒢 - r * (s::nat) * nat (fst (bezw (t::nat) (order 𝒢)) mod int (order 𝒢))› diff_mult_distrib2 by force
then show ?thesis
by (metis (no_types) ‹[(r::nat) * ((order 𝒢 * order 𝒢 - (s::nat) * nat (fst (bezw (t::nat) (order 𝒢)) mod int (order 𝒢)) + (x::nat)) mod order 𝒢) + (r * s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) + (xa::nat)) mod order 𝒢 = r * (order 𝒢 * order 𝒢 - s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢))) + r * x + (r * s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) + xa)] (mod order 𝒢)› semiring_normalization_rules(23))
qed
qed
hence "[r * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢
= r * x + xa] (mod order 𝒢)"
by (metis (no_types, lifting) mod_mult_self4 add.assoc mult.commute cong_def)
thus ?thesis by blast
qed
then show ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
moreover have "❙g [^] (r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢)
+ (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α) ⊗
❙g [^] (t * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢
+ s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))
= ❙g [^] (r * α * x + xa * α) ⊗ ❙g [^] (t * x)"
proof-
have "❙g [^] (r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α)
= ❙g [^] (r * α * x + xa * α)"
proof-
have "[r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α
= r * α * x + xa * α] (mod order 𝒢)"
proof-
have "[r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α
= r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))) + x) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) * α] (mod order 𝒢)"
proof -
show ?thesis
by (meson cong_def mod_add_cong mod_mult_left_eq mod_mult_right_eq)
qed
hence mod_eq: "[r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α
= r * α * (order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))) + r * α * x + r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) * α + xa * α] (mod order 𝒢)"
by (simp add: distrib_left distrib_right add.assoc)
hence mod_eq': "[r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α
= r * α * order 𝒢 * order 𝒢 - r * α * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + r * α * x + r * α * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa * α] (mod order 𝒢)"
by (simp add: semiring_normalization_rules(16) diff_mult_distrib2 semiring_normalization_rules(18))
hence "[r * α * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢) + (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + xa) mod order 𝒢 * α
= r * α * order 𝒢 * order 𝒢 + r * α * x + xa * α] (mod order 𝒢)"
proof(cases "r * α = 0")
case True
then show ?thesis
by (metis mod_eq' diff_zero mult_0 plus_nat.add_0)
next
case False
hence bound: " r * α * order 𝒢 * order 𝒢 - r * α * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) > 0"
proof-
have "s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) < order 𝒢 * order 𝒢"
using assms
by (simp add: mult_strict_mono nat_less_iff)
thus ?thesis
using False by auto
qed
thus ?thesis
proof -
have "r * α * order 𝒢 * order 𝒢 = r * α * (order 𝒢 * order 𝒢 - s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)))
+ r * s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) * α"
using bound diff_mult_distrib2 by force
then have "r * α * order 𝒢 * order 𝒢 + r * α * x = r * α * (order 𝒢 * order 𝒢 - s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)))
+ r * α * x + r * s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) * α"
by presburger
then show ?thesis
using mod_eq by presburger
qed
qed
thus ?thesis
by (metis (mono_tags, lifting) add.assoc cong_def mod_mult_self3)
qed
then show ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
also have "❙g [^] (t * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢 + s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))
= ❙g [^] (t * x)"
proof-
have "[t * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢 + s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))) = t * x] (mod order 𝒢)"
proof-
have "[t * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢 + s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))
= (t * (order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x + s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))] (mod order 𝒢)"
using cong_def mod_add_left_eq mod_mult_cong by blast
hence "[t * ((order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + x) mod order 𝒢 + s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))
= t * (order 𝒢 * order 𝒢 + x )] (mod order 𝒢)"
proof-
have "order 𝒢 * order 𝒢 - s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) > 0"
proof-
have "(nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) ≤ order 𝒢"
using nat_le_iff order.strict_implies_order order_gt_0
by (simp add: order.strict_implies_order)
thus ?thesis
by (metis assms diff_mult_distrib le0 linorder_neqE_nat mult_strict_mono not_le zero_less_diff)
qed
thus ?thesis
using ‹[(t::nat) * ((order 𝒢 * order 𝒢 - (s::nat) * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) + (x::nat)) mod order 𝒢 + s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢))) = t * (order 𝒢 * order 𝒢 - s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)) + x + s * nat (fst (bezw t (order 𝒢)) mod int (order 𝒢)))] (mod order 𝒢)› by auto
qed
thus ?thesis
by (metis (no_types, opaque_lifting) add.commute cong_def mod_mult_right_eq mod_mult_self1)
qed
thus ?thesis using finite_group pow_generator_eq_iff_cong by blast
qed
ultimately show ?thesis by argo
qed
ultimately show ?thesis by simp
qed
lemma P2_case_l_neq_1_gt_x0_rewrite:
assumes "t < order 𝒢"
and "t ≠ 0"
shows "❙g [^] (t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))) = ❙g [^] (t * u0) ⊗ ❙g [^] s"
proof-
from assms have gcd: "gcd t (order 𝒢) = 1"
using prime_field coprime_imp_gcd_eq_1 by blast
hence inverse_t: "[ s * (t * (fst (bezw t (order 𝒢)))) = s * 1] (mod order 𝒢)"
by (metis Num.of_nat_simps(2) Num.of_nat_simps(5) cong_scalar_left order_gt_0 inverse)
hence inverse_t': "[t * u0 + s * (t * (fst (bezw t (order 𝒢)))) =t * u0 + s * 1] (mod order 𝒢)"
using cong_add_lcancel by fastforce
have eq: "int (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) = (fst (bezw t (order 𝒢))) mod order 𝒢"
proof-
have "(fst (bezw t (order 𝒢))) mod order 𝒢 ≥ 0" using order_gt_0 by simp
hence "(nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) = (fst (bezw t (order 𝒢))) mod order 𝒢" by linarith
thus ?thesis by blast
qed
have "[(t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))) = t * u0 + s] (mod order 𝒢)"
proof-
have "[t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))) = t * u0 + t * (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))] (mod order 𝒢)"
by (simp add: distrib_left)
hence "[t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))) = t * u0 + s * (t * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))] (mod order 𝒢)"
by (simp add: ab_semigroup_mult_class.mult_ac(1) mult.left_commute)
hence "[t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))) = t * u0 + s * (t * ( ((fst (bezw t (order 𝒢))) mod order 𝒢)))] (mod order 𝒢)"
using eq
by (simp add: distrib_left mult.commute semiring_normalization_rules(18))
hence "[t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))) = t * u0 + s * (t * (fst (bezw t (order 𝒢))))] (mod order 𝒢)"
by (metis (no_types, opaque_lifting) cong_def mod_add_right_eq mod_mult_right_eq)
hence "[t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))) = t * u0 + s * 1] (mod order 𝒢)" using inverse_t'
using cong_trans cong_int_iff by blast
thus ?thesis by simp
qed
hence "❙g [^] (t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢))))) = ❙g [^] (t * u0 + s)" using finite_group pow_generator_eq_iff_cong by blast
thus ?thesis
by (simp add: nat_pow_mult)
qed
text ‹ Now we show the two end definitions are equal when the input for l (in the ideal model, the second input) is the one constructed by the simulator ›
lemma P2_ideal_real_end_eq:
assumes b0_inv_b1: "b0 ⊗ inv b1 = (h0 ⊗ inv h1) [^] r"
and assert_in_carrier: "h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢"
and x1_in_carrier: "x1 ∈ carrier 𝒢"
and x0_in_carrier: "x0 ∈ carrier 𝒢"
shows "P2_ideal_model_end (x0,x1) (b0 ⊗ (inv (h0 [^] r))) ((h0,h1, ❙g [^] (r::nat),b0,b1),s') 𝒜3 = P2_real_model_end (x0,x1) ((h0,h1, ❙g [^] (r::nat),b0,b1),s') 𝒜3"
including monad_normalisation
proof(cases "(b0 ⊗ (inv (h0 [^] r))) = 𝟭")
case True
have b1_h1: "b1 = h1 [^] r"
proof-
from b0_inv_b1 assert_in_carrier have "b0 ⊗ inv b1 = h0 [^] r ⊗ inv h1 [^] r"
by (simp add: pow_mult_distrib cyclic_group_commute monoid_comm_monoidI)
hence "b0 ⊗ inv h0 [^] r = b1 ⊗ inv h1 [^] r"
by (metis Units_eq Units_l_cancel local.inv_equality True assert_in_carrier
cyclic_group.inverse_pow_pow cyclic_group_axioms
inv_closed nat_pow_closed r_inv)
with True have "𝟭 = b1 ⊗ inv h1 [^] r"
by (simp add: assert_in_carrier inverse_pow_pow)
hence "𝟭 ⊗ h1 [^] r = b1"
by (metis assert_in_carrier cyclic_group.inverse_pow_pow cyclic_group_axioms inv_closed inv_inv l_one local.inv_equality nat_pow_closed)
thus ?thesis
using assert_in_carrier l_one by blast
qed
obtain α :: nat where α: "❙g [^] α = h1" and "α < order 𝒢"
by (metis mod_less_divisor assert_in_carrier generatorE order_gt_0 pow_generator_mod)
obtain s :: nat where s: "❙g [^] s = x1" and s_lt: "s < order 𝒢"
by (metis assms(3) mod_less_divisor generatorE order_gt_0 pow_generator_mod)
have "b1 ⊗ inv ❙g = ❙g [^] (r * α) ⊗ inv ❙g"
by (metis α b1_h1 generator_closed mult.commute nat_pow_pow)
have a_g_exp_rewrite: "(❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0 = ❙g [^] (r * u0 + v0)"
for u0 v0
by (simp add: nat_pow_mult nat_pow_pow)
have z1_rewrite: "(b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ 𝟭 = ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] u1"
for u1 v1 :: nat
by (smt α b1_h1 pow_mult_distrib cyclic_group_commute generator_closed inv_closed m_assoc m_closed monoid_comm_monoidI mult.commute nat_pow_closed nat_pow_mult nat_pow_pow r_one)
have z1_rewrite': "❙g [^] (r * α * u1 + v1 * α) ⊗ ❙g [^] s ⊗ inv ❙g [^] u1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1"
for u1 v1
using assert_in_carrier cyclic_group_commute m_assoc s z1_rewrite by auto
have "P2_ideal_model_end (x0,x1) (b0 ⊗ (inv (h0 [^] r))) ((h0,h1, ❙g [^] (r::nat),b0,b1),s') 𝒜3 = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ 𝟭;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: P2_ideal_model_end_def True funct_OT_12_def)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] u1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: z1_rewrite)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = ❙g [^] (r * u1 + v1);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] u1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: a_g_exp_rewrite)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← map_spmf (λ u1'. (s + u1') mod (order 𝒢)) (sample_uniform (order 𝒢));
v1 ← map_spmf (λ v1'. ((r * order 𝒢 - r * s) + v1') mod (order 𝒢)) (sample_uniform (order 𝒢));
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = ❙g [^] (r * u1 + v1);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] (u1 + (order 𝒢 - s));
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
apply(simp add: bind_map_spmf o_def Let_def)
using P2_output_rewrite assms s_lt assms by presburger
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = ❙g [^] (r * u1 + v1);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = ❙g [^] (r * α * u1 + v1 * α) ⊗ inv ❙g [^] (u1 + (order 𝒢 - s));
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: samp_uni_plus_one_time_pad)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = ❙g [^] (r * u1 + v1);
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = ❙g [^] (r * α * u1 + v1 * α) ⊗ ❙g [^] s ⊗ inv ❙g [^] u1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: P2_inv_g_s_rewrite assms s_lt cong: bind_spmf_cong_simp)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: a_g_exp_rewrite z1_rewrite')
ultimately show ?thesis
by(simp add: P2_real_model_end_def)
next
obtain α :: nat where α: "❙g [^] α = h0"
using generatorE assms
using assert_in_carrier by auto
have w0_rewrite: "❙g [^] (r * u0 + v0) = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0"
for u0 v0
by (simp add: nat_pow_mult nat_pow_pow)
have order_gt_0: "order 𝒢 > 0" using order_gt_0 by simp
obtain s :: nat where s: "❙g [^] s = x0" and s_lt: "s < order 𝒢"
by (metis mod_less_divisor generatorE order_gt_0 pow_generator_mod x0_in_carrier)
case False
hence l_neq_1: "(b0 ⊗ (inv (h0 [^] r))) ≠ 𝟭"by auto
then show ?thesis
proof(cases "(b0 ⊗ (inv (h0 [^] r))) = ❙g")
case True
hence "b0 = ❙g ⊗ h0 [^] r"
by (metis assert_in_carrier generator_closed inv_solve_right nat_pow_closed)
hence "b0 = ❙g ⊗ ❙g [^] (r * α)"
by (metis α generator_closed mult.commute nat_pow_pow)
have z0_rewrite: "b0 [^] u0 ⊗ h0 [^] v0 ⊗ 𝟭 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] u0"
for u0 v0 :: nat
by (smt α ‹b0 = ❙g ⊗ ❙g [^] (r * α)› pow_mult_distrib cyclic_group_commute generator_closed m_assoc monoid_comm_monoidI mult.commute nat_pow_closed nat_pow_mult nat_pow_pow r_one)
have z0_rewrite': "❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (u0 + s) = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] u0 ⊗ ❙g [^] s"
for u0 v0
by (simp add: add.assoc nat_pow_mult)
have z0_rewrite'': "❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] u0 ⊗ x0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0"
for u0 v0 using z0_rewrite
using assert_in_carrier by auto
have "P2_ideal_model_end (x0,x1) (b0 ⊗ (inv (h0 [^] r))) ((h0,h1,❙g [^] (r::nat),b0,b1),s') 𝒜3 = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ 𝟭;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
apply(simp add: P2_ideal_model_end_def True funct_OT_12_def)
using order_gt_0 order_gt_1_gen_not_1 True l_neq_1 by auto
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] u0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: z0_rewrite w0_rewrite)
also have "... = do {
u0 ← map_spmf (λ u0. ((order 𝒢 - s) + u0) mod (order 𝒢)) (sample_uniform (order 𝒢));
v0 ← map_spmf (λ v0. (r * s + v0) mod (order 𝒢)) (sample_uniform (order 𝒢));
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (u0 + s);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
apply(simp add: bind_map_spmf o_def Let_def cong: bind_spmf_cong_simp)
using P2_e0_rewrite assms s_lt assms by presburger
also have "... = do {
u0 ← map_spmf (λ u0. ((order 𝒢 - s) + u0) mod (order 𝒢)) (sample_uniform (order 𝒢));
v0 ← map_spmf (λ v0. (r * s + v0) mod (order 𝒢)) (sample_uniform (order 𝒢));
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] u0 ⊗ x0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: z0_rewrite' s)
also have "... = do {
u0 ← map_spmf (λ u0. ((order 𝒢 - s) + u0) mod (order 𝒢)) (sample_uniform (order 𝒢));
v0 ← map_spmf (λ v0. (r * s + v0) mod (order 𝒢)) (sample_uniform (order 𝒢));
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: w0_rewrite z0_rewrite'')
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: samp_uni_plus_one_time_pad)
ultimately show ?thesis
by(simp add: P2_real_model_end_def)
next
case False
have b0_l: "b0 = (b0 ⊗ (inv (h0 [^] r))) ⊗ h0 [^] r"
by (simp add: assert_in_carrier m_assoc)
have b0_g_r:"b0 = (b0 ⊗ (inv (h0 [^] r))) ⊗ ❙g [^] (r * α)"
by (metis α b0_l generator_closed mult.commute nat_pow_pow)
obtain t :: nat where t: "❙g [^] t = (b0 ⊗ (inv (h0 [^] r)))" and t_lt_order_g: "t < order 𝒢"
by (metis (full_types) mod_less_divisor order_gt_0 pow_generator_mod
assert_in_carrier cyclic_group.generatorE cyclic_group_axioms
inv_closed m_closed nat_pow_closed)
with l_neq_1 have t_neq_0: "t ≠ 0" using l_neq_1_exp_neq_0 by simp
have z0_rewrite: "b0 [^] u0 ⊗ h0 [^] v0 ⊗ 𝟭 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ((b0 ⊗ (inv (h0 [^] r)))) [^] u0"
for u0 v0
proof-
from b0_l have "b0 [^] u0 ⊗ h0 [^] v0 = ((b0 ⊗ (inv (h0 [^] r))) ⊗ h0 [^] r) [^] u0 ⊗ h0 [^] v0" by simp
hence "b0 [^] u0 ⊗ h0 [^] v0 = ((b0 ⊗ (inv (h0 [^] r)))) [^] u0 ⊗ (h0 [^] r) [^] u0 ⊗ h0 [^] v0"
by (simp add: assert_in_carrier pow_mult_distrib cyclic_group_commute monoid_comm_monoidI)
hence "b0 [^] u0 ⊗ h0 [^] v0 = ((❙g [^] α) [^] r) [^] u0 ⊗ (❙g [^] α) [^] v0 ⊗ ((b0 ⊗ (inv (h0 [^] r)))) [^] u0"
using cyclic_group_assoc cyclic_group_commute assert_in_carrier α by simp
hence "b0 [^] u0 ⊗ h0 [^] v0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ((b0 ⊗ (inv (h0 [^] r)))) [^] u0"
by (simp add: monoid.nat_pow_pow mult.commute nat_pow_mult)
thus ?thesis
by (simp add: assert_in_carrier)
qed
have z0_rewrite': "❙g [^] (r * α * u0 + v0 * α) ⊗ ((b0 ⊗ (inv (h0 [^] r)))) [^] u0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (t * u0)"
for u0 v0
by (metis generator_closed nat_pow_pow t)
have z0_rewrite'': "❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (t * u0) ⊗ ❙g [^] s = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0"
for u0 v0
using assert_in_carrier s z0_rewrite z0_rewrite' by auto
have "P2_ideal_model_end (x0,x1) (b0 ⊗ (inv (h0 [^] r))) ((h0,h1,❙g [^] (r::nat),b0,b1),s') 𝒜3 = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ((b0 ⊗ (inv (h0 [^] r)))) [^] u0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: P2_ideal_model_end_def l_neq_1 funct_OT_12_def w0_rewrite z0_rewrite)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (t * u0);
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: z0_rewrite')
also have "... = do {
u0 ← map_spmf (λ u0. (order 𝒢 * order 𝒢 - (s * ((nat (((fst (bezw t (order 𝒢)))) mod (order 𝒢))))) + u0) mod (order 𝒢)) (sample_uniform (order 𝒢));
v0 ← map_spmf (λ v0. (r * s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)) + v0) mod (order 𝒢)) (sample_uniform (order 𝒢));
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))));
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: bind_map_spmf o_def Let_def s_lt P2_case_l_new_1_gt_e0_rewrite cong: bind_spmf_cong_simp)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (t * (u0 + (s * (nat ((fst (bezw t (order 𝒢))) mod order 𝒢)))));
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: samp_uni_plus_one_time_pad)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = ❙g [^] (r * u0 + v0);
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = ❙g [^] (r * α * u0 + v0 * α) ⊗ ❙g [^] (t * u0) ⊗ ❙g [^] s;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: P2_case_l_neq_1_gt_x0_rewrite t_lt_order_g t_neq_0 cyclic_group_assoc)
also have "... = do {
u0 ← sample_uniform (order 𝒢);
v0 ← sample_uniform (order 𝒢);
u1 ← sample_uniform (order 𝒢);
v1 ← sample_uniform (order 𝒢);
let w0 = (❙g [^] (r::nat)) [^] u0 ⊗ ❙g [^] v0;
let w1 = (❙g [^] (r::nat)) [^] u1 ⊗ ❙g [^] v1;
let z0 = b0 [^] u0 ⊗ h0 [^] v0 ⊗ x0;
let z1 = (b1 ⊗ inv ❙g) [^] u1 ⊗ h1 [^] v1 ⊗ x1;
let e0 = (w0,z0);
let e1 = (w1,z1);
out ← 𝒜3 e0 e1 s';
return_spmf ((), out)}"
by(simp add: w0_rewrite z0_rewrite'')
ultimately show ?thesis
by(simp add: P2_real_model_end_def)
qed
qed
lemma P2_ideal_real_eq:
assumes x1_in_carrier: "x1 ∈ carrier 𝒢"
and x0_in_carrier: "x0 ∈ carrier 𝒢"
shows "P2_real_model (x0,x1) σ z 𝒜 = P2_ideal_model (x0,x1) σ z 𝒜"
proof-
have "P2_real_model' (x0, x1) σ z 𝒜 = P2_ideal_model' (x0, x1) σ z 𝒜"
proof-
have 1:"do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
let l = b0 ⊗ (inv (h0 [^] r));
P2_ideal_model_end (x0,x1) l ((h0,h1,a,b0,b1),s') 𝒜3} = P2_ideal_model' (x0,x1) σ z 𝒜"
unfolding P2_ideal_model'_def by simp
have "P2_real_model' (x0, x1) σ z 𝒜 = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
P2_real_model_end (x0, x1) ((h0,h1,a,b0,b1),s') 𝒜3}"
by(simp add: P2_real_model'_def)
also have "... = do {
let (𝒜1, 𝒜2, 𝒜3) = 𝒜;
((h0,h1,a,b0,b1),s) ← 𝒜1 σ z;
_ :: unit ← assert_spmf (h0 ∈ carrier 𝒢 ∧ h1 ∈ carrier 𝒢 ∧ a ∈ carrier 𝒢 ∧ b0 ∈ carrier 𝒢 ∧ b1 ∈ carrier 𝒢);
(((in1, in2, in3), r),s') ← 𝒜2 (h0,h1,a,b0,b1) s;
let (h,a,b) = (h0 ⊗ inv h1, a, b0 ⊗ inv b1);
(out_zk_funct, _) ← funct_DH_ZK (h,a,b) ((in1, in2, in3), r);
_ :: unit ← assert_spmf out_zk_funct;
let l = b0 ⊗ (inv (h0 [^] r));
P2_ideal_model_end (x0,x1) l ((h0,h1,a,b0,b1),s') 𝒜3}"
by(simp add: P2_ideal_real_end_eq assms cong: bind_spmf_cong_simp)
ultimately show ?thesis by(simp add: P2_real_model'_def P2_ideal_model'_def)
qed
thus ?thesis by(simp add: P2_ideal_model_rewrite P2_real_model_rewrite)
qed
lemma malicious_sec_P2:
assumes x1_in_carrier: "x1 ∈ carrier 𝒢"
and x0_in_carrier: "x0 ∈ carrier 𝒢"
shows "mal_def.perfect_sec_P2 (x0,x1) σ z (P2_S1, P2_S2) 𝒜"
unfolding malicious_base.perfect_sec_P2_def
by (simp add: P2_ideal_real_eq P2_ideal_view_unfold assms)
lemma correct:
assumes "x0 ∈ carrier 𝒢"
and "x1 ∈ carrier 𝒢"
shows "funct_OT_12 (x0, x1) σ = protocol_ot (x0,x1) σ"
proof-
have σ_eq_0_output_correct:
"((❙g [^] α0) [^] r) [^] u0 ⊗ (❙g [^] α0) [^] v0 ⊗ x0 ⊗
inv (((❙g [^] r) [^] u0 ⊗ ❙g [^] v0) [^] α0) = x0"
(is "?lhs = ?rhs")
for α0 r u0 v0 :: nat
proof-
have mult_com: "r * u0 * α0 = α0 * r * u0" by simp
have in_carrier1: "((❙g [^] (r * u0 * α0))) ⊗ (❙g [^] (v0 * α0)) ∈ carrier 𝒢" by simp
have in_carrier2: "inv ((❙g [^] (r * u0 * α0))) ⊗ (❙g [^] (v0 * α0)) ∈ carrier 𝒢" by simp
have "?lhs = ((❙g [^] (α0 * r * u0))) ⊗ (❙g [^] (α0 * v0)) ⊗ x0 ⊗
inv (((❙g [^] (r * u0 * α0)) ⊗ ❙g [^] (v0 * α0)))"
by (simp add: nat_pow_pow pow_mult_distrib cyclic_group_commute monoid_comm_monoidI)
also have "... = (((❙g [^] (r * u0 * α0))) ⊗ (❙g [^] (v0 * α0))) ⊗ x0 ⊗
(inv (((❙g [^] (r * u0 * α0)) ⊗ ❙g [^] (v0 * α0))))"
using mult.commute mult.assoc mult_com
by (metis (no_types) mult.commute)
also have "... = x0 ⊗ (((❙g [^] (r * u0 * α0))) ⊗ (❙g [^] (v0 * α0))) ⊗
(inv (((❙g [^] (r * u0 * α0)) ⊗ ❙g [^] (v0 * α0))))"
using cyclic_group_commute in_carrier1 assms by simp
also have "... = x0 ⊗ ((((❙g [^] (r * u0 * α0))) ⊗ (❙g [^] (v0 * α0))) ⊗
(inv (((❙g [^] (r * u0 * α0)) ⊗ ❙g [^] (v0 * α0)))))"
using cyclic_group_assoc in_carrier1 in_carrier2 assms by auto
ultimately show ?thesis using assms by simp
qed
have σ_eq_1_output_correct:
"((❙g [^] α1) [^] r ⊗ ❙g ⊗ inv ❙g) [^] u1 ⊗ (❙g [^] α1) [^] v1 ⊗ x1 ⊗
inv (((❙g [^] r) [^] u1 ⊗ ❙g [^] v1) [^] α1) = x1"
(is "?lhs = ?rhs")
for α1 r u1 v1 :: nat
proof-
have com1: "α1 * r * u1 = r * u1 * α1" "v1 * α1 = α1 * v1" by simp+
have in_carrier1: "(❙g [^] (r * u1 * α1)) ⊗ (❙g [^] (v1 * α1)) ∈ carrier 𝒢" by simp
have in_carrier2: "inv ((❙g [^] (r * u1 * α1)) ⊗ (❙g [^] (v1 * α1))) ∈ carrier 𝒢" by simp
have lhs: "?lhs = ((❙g [^] (α1*r)) ⊗ ❙g ⊗ inv ❙g) [^] u1 ⊗ (❙g [^] (α1 * v1)) ⊗ x1 ⊗
inv ((❙g [^] (r * u1 * α1)) ⊗ ❙g [^] (v1*α1))"
by (simp add: nat_pow_pow pow_mult_distrib cyclic_group_commute monoid_comm_monoidI)
also have lhs1: "... = (❙g [^] (α1 * r)) [^] u1 ⊗ (❙g [^] (α1 * v1)) ⊗ x1 ⊗
inv ((❙g [^] (r * u1 * α1)) ⊗ ❙g [^] (v1*α1))"
by (simp add: cyclic_group_assoc)
also have lhs2: "... = (❙g [^] (r * u1 * α1)) ⊗ (❙g [^] (v1 * α1)) ⊗ x1 ⊗
inv ((❙g [^] (r * u1 * α1)) ⊗ ❙g [^] (v1 * α1))"
by (simp add: nat_pow_pow pow_mult_distrib cyclic_group_commute monoid_comm_monoidI com1)
also have "... = (((❙g [^] (r * u1 * α1)) ⊗ (❙g [^] (v1 * α1))) ⊗ x1) ⊗
inv ((❙g [^] (r * u1 * α1)) ⊗ ❙g [^] (v1 * α1))"
using in_carrier1 in_carrier2 assms cyclic_group_assoc by blast
also have "... = (x1 ⊗ ((❙g [^] (r * u1 * α1)) ⊗ (❙g [^] (v1 * α1)))) ⊗
inv ((❙g [^] (r * u1 * α1)) ⊗ ❙g [^] (v1 * α1))"
using in_carrier1 assms cyclic_group_commute by simp
ultimately show ?thesis
using cyclic_group_assoc assms in_carrier1 in_carrier1 assms cyclic_group_commute lhs1 lhs2 lhs by force
qed
show ?thesis
unfolding funct_OT_12_def protocol_ot_def Let_def
by(cases σ; auto simp add: assms σ_eq_1_output_correct σ_eq_0_output_correct bind_spmf_const
lossless_sample_uniform_units order_gt_0 P1_assert_correct1 P1_assert_correct2 lossless_weight_spmfD)
qed
lemma correctness:
assumes "x0 ∈ carrier 𝒢"
and "x1 ∈ carrier 𝒢"
shows "mal_def.correct (x0,x1) σ"
unfolding mal_def.correct_def
by(simp add: correct assms)
end
locale OT_asymp =
fixes 𝒢 :: "nat ⇒ 'grp cyclic_group"
assumes ot: "⋀η. ot (𝒢 η)"
begin
sublocale ot "𝒢 n" for n using ot by simp
lemma correctness_asym:
assumes "x0 ∈ carrier (𝒢 n)"
and "x1 ∈ carrier (𝒢 n)"
shows "mal_def.correct n (x0,x1) σ"
using assms correctness by simp
lemma P1_security_asym:
"negligible (λ n. mal_def.adv_P1 n M σ z (P1_S1 n, P1_S2) 𝒜 D)"
if neg1: "negligible (λ n. ddh.advantage n (P1_DDH_mal_adv_σ_true n M z 𝒜 D))"
and neg2: "negligible (λ n. ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_true n M z 𝒜 D)))"
and neg3: "negligible (λ n. ddh.advantage n (P1_DDH_mal_adv_σ_false n M z 𝒜 D))"
and neg4: "negligible (λ n. ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_false n M z 𝒜 D)))"
proof-
have neg_add1: "negligible (λ n. ddh.advantage n (P1_DDH_mal_adv_σ_true n M z 𝒜 D)
+ ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_true n M z 𝒜 D)))"
and neg_add2: "negligible (λ n. ddh.advantage n (P1_DDH_mal_adv_σ_false n M z 𝒜 D)
+ ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_false n M z 𝒜 D)))"
using neg1 neg2 neg3 neg4 negligible_plus by(blast)+
show ?thesis
proof(cases σ)
case True
have bound_mod: "¦mal_def.adv_P1 n M σ z (P1_S1 n, P1_S2) 𝒜 D¦
≤ ddh.advantage n (P1_DDH_mal_adv_σ_true n M z 𝒜 D)
+ ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_true n M z 𝒜 D))" for n
by (metis (no_types) True abs_idempotent P1_adv_real_ideal_model_def P1_advantages_eq P1_real_ideal_DDH_advantage_true_bound)
then show ?thesis
using P1_real_ideal_DDH_advantage_true_bound that bound_mod that negligible_le neg_add1 by presburger
next
case False
have bound_mod: "¦mal_def.adv_P1 n M σ z (P1_S1 n, P1_S2) 𝒜 D¦
≤ ddh.advantage n (P1_DDH_mal_adv_σ_false n M z 𝒜 D)
+ ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_false n M z 𝒜 D))" for n
proof -
have "¦spmf (P1_real_model n M σ z 𝒜 ⤜ D) True - spmf (P1_ideal_model n M σ z 𝒜 ⤜ D) True¦
≤ local.ddh.advantage n (P1_DDH_mal_adv_σ_false n M z 𝒜 D)
+ local.ddh.advantage n (ddh.DDH_𝒜' n (P1_DDH_mal_adv_σ_false n M z 𝒜 D))"
by (metis (no_types) False P1_adv_real_ideal_model_def P1_advantages_eq P1_real_ideal_DDH_advantage_false_bound)
then show ?thesis
by (simp add: P1_adv_real_ideal_model_def P1_advantages_eq)
qed
then show ?thesis using P1_real_ideal_DDH_advantage_false_bound bound_mod that negligible_le neg_add2 by presburger
qed
qed
lemma P2_security_asym:
assumes x1_in_carrier: "x1 ∈ carrier (𝒢 n)"
and x0_in_carrier: "x0 ∈ carrier (𝒢 n)"
shows "mal_def.perfect_sec_P2 n (x0,x1) σ z (P2_S1 n, P2_S2 n) 𝒜"
using assms malicious_sec_P2 by fast
end
end