gistfile1.txt

import data.zmod.basic data.nat.prime 
 number_theory.quadratic_reciprocity
 tactic.find tactic.omega data.vector
 
lemma zip_with_len_l {α β γ : Type*} {l₁ : list α} {l₂ : list β} {f : α → β → γ}
  (h : list.length l₁ = list.length l₂) : 
  list.length (list.zip_with f l₁ l₂) = list.length l₁ :=
begin
  induction l₁ with x xs ih generalizing l₂,
    {simp [list.zip_with]},
    {
      cases l₂ with y ys,
        {injection h},
        {simp only [list.zip_with, list.length], finish}
    }
end

lemma map_with_len_l {α β : Type*} {l₁ : list α} {f : α → β} : 
  list.length (list.map f l₁) = list.length l₁ :=
begin
  induction l₁ with x xs ih, 
  {simp [list.map]}, 
  {simp [list.map]},
end





namespace encryption
    
variables 
  (p q k : ℕ) (g h pubkey : zmod p) (prikey : zmod q)
  [Hk : 2 ≤ k] [Hp : fact (nat.prime p)] [Hq : fact (nat.prime q)]
  [Hdiv : p = q * k + 1]  [H₁ : h ≠ 0] [H₂ : h^k ≠ 1]
  [H₃ : g = h^k] [H₄ : g^prikey.val = pubkey]

/- ElGamal Encryption -/
def elgamal_enc (m : zmod p) (r : zmod q) := 
  (g ^ r.val, g ^ m.val * pubkey ^ r.val)


/- ElGamal Decryption -/
def elgamal_dec (c : zmod p × zmod p) := 
  c.2 * (c.1 ^ prikey.val)⁻¹  
 
/- ElGamal Reencryption -/ 
def elgamal_reenc (c : zmod p × zmod p) (r : zmod q) :=  
  (c.1 * g ^ r.val, c.2 * pubkey ^ r.val)

/- Multiplication of two ciphertext -/
def ciphertext_mult (c d : zmod p × zmod p) :=  
  (c.1 * d.1, c.2 * d.2)

 
/- Encryption of a ballot (vector of length n) -/
def elgamal_enc_ballot : list (zmod p) → list (zmod q) → list (zmod p × zmod p) 
| [] [] := []
| [] (r :: rs) := [] 
| (m :: ms) [] := []
| (m :: ms) (r :: rs) := 
    (elgamal_enc p q g pubkey m r) :: elgamal_enc_ballot ms rs 

/- Encryption of a ballot (vector of length n) 
def vector_elgamal_enc {n : ℕ} :  
  vector (zmod p) n -> vector (zmod q) n -> vector (zmod p × zmod p) n  
  | ⟨ms, Hm⟩  ⟨rs, Hr⟩ := 
    ⟨list.zip_with (elgamal_enc p q g pubkey) ms rs, 
    begin
      have Ht : list.length ms = list.length rs :=  
      begin rw [Hm, Hr] end,
      rw <- Hm, apply zip_with_len_l, exact Ht
    end⟩ -/

def elgamal_dec_ballot : list (zmod p × zmod p) → list (zmod p) 
| [] :=  [] 
| (c :: cs) := elgamal_dec p q prikey c :: elgamal_dec_ballot cs 

/- Decryption of a ballot (vector of length n) 
def vector_elgamal_dec {n : ℕ} :  
  vector (zmod p × zmod p) n -> vector (zmod p) n  
  | ⟨cs, Hc⟩  := 
    ⟨list.map (elgamal_dec p q prikey) cs, 
    begin 
      rw <- Hc, apply map_with_len_l, 
    end⟩ -/

def elgamal_reenc_ballot : list (zmod p × zmod p) → list (zmod q) → list (zmod p × zmod p)
| [] [] := []
| [] (r :: rs) := [] 
| (c :: cs) [] := []
| (c :: cs) (r :: rs) :=  
  (elgamal_reenc p q g pubkey c r) :: elgamal_reenc_ballot cs rs 

/- Reencryption of ballot (vector of length n)
def vector_elgamal_reenc {n : ℕ} :  
  vector (zmod p × zmod p) n -> vector (zmod q) n -> vector (zmod p × zmod p) n  
  | ⟨cs, Hc⟩  ⟨rs, Hr⟩ := 
    ⟨list.zip_with (elgamal_reenc p q g pubkey) cs rs, 
    begin 
      have Ht : list.length cs = list.length rs :=  
      begin rw [Hc, Hr] end,
      rw <- Hc, apply zip_with_len_l, exact Ht
    end⟩ -/

def ciphertext_mult_ballot : list (zmod p × zmod p) → list (zmod p × zmod p) → list (zmod p × zmod p)
| [] [] := []
| [] (c₂ :: cs₂) := [] 
| (c₁ :: cs₁) [] := []
| (c₁ :: cs₁) (c₂:: cs₂) := 
        (ciphertext_mult p c₁ c₂) :: ciphertext_mult_ballot cs₁ cs₂ 

        
/- Component wise multiplication of two ballot of same length (vector of length n )
def vector_ciphertext_mult {n : ℕ} :  
  vector (zmod p × zmod p) n -> vector (zmod p × zmod p) n -> vector (zmod p × zmod p) n  
  | ⟨cs₁, Hc₁⟩  ⟨cs₂, Hc₂⟩ := 
    ⟨list.zip_with (ciphertext_mult p) cs₁  cs₂, 
    begin 
      have Ht : list.length cs₁ = list.length cs₂ :=  
      begin rw [Hc₁, Hc₂] end,
      rw <- Hc₁, apply zip_with_len_l, exact Ht,
    end⟩-/

def raise_message_to_generator : list (zmod p) → list (zmod p)
| [] := [] 
| (m :: ms) := (g ^ m.val) :: raise_message_to_generator ms 

/- Decrypting additive ElGamal gives g^m 
def raise_message_to_generator {n : ℕ} : vector (zmod p) n → vector (zmod p) n
| ⟨ms, Hm⟩ := ⟨list.map (λ (m : zmod p), g ^ m.val) ms, 
  begin
    rw map_with_len_l, exact Hm
  end⟩ -/


/- Compute finally tally, which is multiplying all the ballots 
   component wise. In final count, these ballots will be 
   passed through a (formally verified) mix-net with zero-knowledge 
   proof -/


 
/- proof that g is a generator of the group -/
include Hp Hq Hdiv H₁ H₂ H₃ H₄ 
lemma generator_proof : g ^ q = 1 := 
begin
  rw [H₃, ← pow_mul, mul_comm],
  have H : p - 1 = q * k := nat.pred_eq_of_eq_succ Hdiv,
  rw ← H, exact zmod.pow_card_sub_one_eq_one H₁, 
end  

/- correctness property of encryption and decryption -/
theorem elgamal_enc_dec_identity : ∀ m r c, 
  c = elgamal_enc p q g pubkey m r →
  elgamal_dec p q prikey c = g ^ m.val := 
begin
  unfold elgamal_enc elgamal_dec, simp, 
  intros m r c Hc, rw [Hc, ←H₄, ←pow_mul, ←pow_mul, mul_assoc],
  have Hc : prikey.val * r.val = r.val * prikey.val := 
    mul_comm (zmod.val prikey) (zmod.val r), 
  have Hd : g ≠ 0 :=  begin rw H₃, 
    exact pow_ne_zero k H₁ end, 
  rw [Hc, mul_inv_cancel], simp, 
  exact pow_ne_zero _ Hd, 
end

/- re-encryption correctness -/
theorem elgamal_reenc_correct : ∀ r r₁ m c₁ c₂, c₁ = elgamal_enc p q g pubkey m r → 
  c₂ = elgamal_reenc p q g pubkey c₁ r₁ →  elgamal_dec p q prikey c₂ = g ^ m.val :=
begin
  intros  r r₁ m c₁ c₂ Hc₁ Hc₂, symmetry,
  rw [Hc₂, Hc₁], unfold elgamal_reenc elgamal_enc elgamal_dec, simp, 
  rw [←H₄, tactic.ring.pow_add_rev g (zmod.val r) (zmod.val r₁)],
  rw @tactic.ring_exp.pow_e_pf_exp _ _ (g ^ prikey.val) g prikey.val r.val _ rfl rfl,
  rw @tactic.ring_exp.pow_e_pf_exp _ _ (g ^ prikey.val) g prikey.val r₁.val _ rfl rfl,
  rw @tactic.ring_exp.pow_e_pf_exp _ _ (g ^ (r.val + r₁.val)) g (r.val + r₁.val) prikey.val _ rfl rfl,
  have Ha : g ^ m.val * g ^ (prikey.val * r.val) * g ^ (prikey.val * r₁.val) * 
    (g ^ ((r.val + r₁.val) * prikey.val))⁻¹ = g ^ m.val * 
    (g ^ (prikey.val * r.val) * g ^ (prikey.val * r₁.val)) * (g ^ ((r.val + r₁.val) * prikey.val))⁻¹, ring, 
  rw [Ha, tactic.ring.pow_add_rev g (prikey.val * r.val) (prikey.val * r₁.val)], clear Ha,
  have Hb : g ^ (prikey.val * r.val + prikey.val * r₁.val) = g ^ (prikey.val * (r.val + r₁.val)), ring, 
  rw [Hb, mul_comm prikey.val (r.val + r₁.val), mul_assoc,  mul_inv_cancel], ring, 
  apply pow_ne_zero, rw H₃, apply pow_ne_zero, exact H₁,
end  


theorem additive_homomorphic_property : ∀ c d m₁ m₂ r₁ r₂,
 c = elgamal_enc p q g pubkey m₁ r₁ ->
 d = elgamal_enc p q g pubkey m₂ r₂ -> 
 (g ^ (r₁.val + r₂.val), g ^ (m₁.val + m₂.val) * 
 pubkey ^ (r₁.val + r₂.val)) = ciphertext_mult p c d := 
begin 
  unfold elgamal_enc ciphertext_mult, 
  intros c d m₁ m₂ r₁ r₂ Hc Hd, rw [Hc, Hd], simp,
  have Ht₁ : g ^ (r₁.val + r₂.val) = g ^ r₁.val * g ^ r₂.val := 
    pow_add g r₁.val r₂.val,
  have Ht₂ : g ^ (m₁.val + m₂.val) * pubkey ^ (r₁.val + r₂.val) =  
    g ^ m₁.val * pubkey ^ r₁.val * (g ^ m₂.val * pubkey ^ r₂.val) :=  
    begin rw [pow_add, pow_add], simp, ring end,
  exact and.intro Ht₁ Ht₂,
end 

theorem ballot_elgamal_enc_dec_identity : ∀ (ms : list (zmod p)) (rs : list (zmod q)) cs,
  list.length ms = list.length rs → cs = elgamal_enc_ballot p q g pubkey ms rs → 
  elgamal_dec_ballot p q prikey cs = raise_message_to_generator p g ms 
  | [] [] := 
    begin 
      simp [elgamal_enc_ballot, elgamal_dec_ballot, 
        raise_message_to_generator], 
    end 
  | [] (rsh :: rst) := λ cs Hl, begin contradiction, end
  | (msh :: mst) [] := λ cs Hl, begin contradiction, end
  | (msh :: mst) (rsh :: rst) := λ cs Hl Hcs,
    begin 
      rw Hcs, cases cs with csh cst, contradiction, 
      simp [elgamal_enc_ballot] at Hcs, 
      simp [elgamal_enc_ballot, elgamal_dec_ballot, 
        raise_message_to_generator], 
      split, 
      /- why can't I apply the elgamal_enc_dec_identity -/
      apply elgamal_enc_dec_identity, 
      
      cases Hcs, 
      specialize (ballot_elgamal_enc_dec_identity mst rst cst _ Hcs_right),
      rw ← Hcs_right, assumption, simp [list.length] at Hl, exact Hl,  
    end 

invalid apply tactic, failed to synthesize type class instance

pqk: ℕ
ghpubkey: zmod p
prikey: zmod q
Hp: fact (nat.prime p)
Hq: fact (nat.prime q)
Hdiv: p = q * k + 1
H₁: h ≠ 0
H₂: h ^ k ≠ 1
H₃: g = h ^ k
H₄: g ^ prikey.val = pubkey
ballot_elgamal_enc_dec_identity: ∀ (ms : list (zmod p)) (rs : list (zmod q)) (cs : list (zmod p × zmod p)), ms.length = rs.length → cs = elgamal_enc_ballot p q g pubkey ms rs → elgamal_dec_ballot p q prikey cs = raise_message_to_generator p g ms
msh: zmod p
mst: list (zmod p)
rsh: zmod q
rst: list (zmod q)
Hl: (msh :: mst).length = (rsh :: rst).length
csh: zmod p × zmod p
cst: list (zmod p × zmod p)
Hcs: csh = elgamal_enc p q g pubkey msh rsh ∧ cst = elgamal_enc_ballot p q g pubkey mst rst
⊢ elgamal_dec p q prikey (elgamal_enc p q g pubkey msh rsh) = g ^ msh.val