{-# OPTIONS --without-K #-}
open import Type
open import Data.Two
open import Data.Product

-- Decisional Diffie-Hellman security game
module Game.DDH
  (ℤq G : ★)
  (g    : G)
  (_^_  : G → ℤq → G)
  (Rₐ   : ★)
  where

-- The type of DDH adversaries:
Adv : ★
Adv = Rₐ → G → G → G → 𝟚

-- The randomness supply needed for DDH games
R : ★
R = Rₐ × ℤq × ℤq × ℤq

-- Decisional Diffie-Hellman game:
--   * input: adversary and randomness supply
--   * output b: adversary claims we are in game ⅁ b
Game : ★
Game = Adv → R → 𝟚

-- The adversary is given correlated inputs
⅁₀ : Game
⅁₀ d (r , x , y , _) = d r (g ^ x) (g ^ y) ((g ^ x) ^ y)

-- The adversary is given independent inputs
⅁₁ : Game
⅁₁ d (r , x , y , z) = d r (g ^ x) (g ^ y) (g ^ z)

-- Package ⅁₀ and ⅁₁
⅁ : 𝟚 → Game
⅁ = proj (⅁₀ , ⅁₁)