{-# OPTIONS --without-K --copatterns #-}
-- Assuming the message space is only one bit the attack can be made even simpler.

open import Function
open import Type using (★)
open import Data.Product
open import Data.Two
open import Relation.Binary.PropositionalEquality.NP
open import Control.Strategy

import Game.IND-CCA2

module Attack.Reencryption.OneBitMessage
  (PubKey SecKey CipherText Rₑ Rₖ : ★)

  (KeyGen : Rₖ → PubKey × SecKey)
  (Enc    : PubKey → {-Message-}𝟚 → Rₑ → CipherText)
  (Dec    : SecKey → CipherText → {-Message-}𝟚)
  (Reenc  : PubKey → CipherText → Rₑ → CipherText)
  (Reenc-correct : ∀ rₖ m r₀ r₁ →
                      case KeyGen rₖ of λ
                      { (pk , sk) →
                        Dec sk (Reenc pk (Enc pk m r₀) r₁) ≡ m
                      })
  where

module IND-CCA2 = Game.IND-CCA2 PubKey SecKey 𝟚 CipherText Rₑ Rₖ Rₑ KeyGen Enc Dec
open IND-CCA2

module _ (rₐ : Rₑ) (pk : PubKey) where
    CPA-adversary : CPAAdversary (DecRound 𝟚)
    get-m CPA-adversary   = 0₂ , 1₂
    put-c CPA-adversary c = ask (Reenc pk c rₐ) done

adversary : IND-CCA2.Adversary
adversary rₐ pk = done (CPA-adversary rₐ pk)

adversary-always-win : ∀ b r → IND-CCA2.EXP b adversary r ≡ b
adversary-always-win b (rₐ , rₖ , rₑ) rewrite η-[0:1:] id b = Reenc-correct rₖ b rₑ rₐ