{-# OPTIONS --without-K #-}
open import Type
open import Data.Product
open import Relation.Binary.PropositionalEquality.NP

module Cipher.ElGamal.Generic
  (Message : )
  (ℤq      : )
  (G       : )
  (g       : G)
  (_^_     : G  ℤq  G)

  -- Required for encryption
  (_♦_     : G  Message  Message)

  -- Required for decryption
  (_/_     : Message  G  Message)
where

PubKey     = G
SecKey     = ℤq
CipherText = G × Message
Rₖ         = ℤq
Rₑ         = ℤq

PubKeyGen : Rₖ  PubKey
PubKeyGen x = g ^ x

KeyGen : Rₖ  PubKey × SecKey
KeyGen x = (g ^ x , x)

Enc : PubKey  Message  Rₑ  CipherText
Enc  m y =  , ζ where
   = g  ^ y
  δ  =  ^ y
  ζ  = δ   m

Dec : SecKey  CipherText  Message
Dec x ( , ζ) = ζ / ( ^ x)

module FunctionalCorrectness
    (/-♦    :  {x y}  (x  y) / x  y)
    (comm-^ :  {α x y}  (α ^ x)^ y  (α ^ y)^ x)
    where

    functional-correctness :  x y m  Dec x (Enc (g ^ x) m y)  m
    functional-correctness x y m = ap Ctx comm-^  /-♦
      where Ctx = λ z  (z  m) / ((g ^ y)^ x)