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 𝒢)))