{-# OPTIONS --without-K --copatterns #-}
{-
Any cipher which does supports reencryption (exponential ElGamal, Pailler...) are vulnerable to a CCA2 attack.
-}
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
  (PubKey    : )
  (SecKey    : )
  (Message   : )
  (CipherText : )

  -- randomness supply for, encryption, key-generation
  (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
                      })

  (_==_    : (x y : Message)  𝟚)
  (m₀ m₁   : Message)
  (m₁==m₁  : m₁ == m₁  1₂)
  (¬m₀==m₁ : m₀ == m₁  0₂)
  where

m : 𝟚  Message
m = [0: m₀
     1: m₁ ]

m-diff :  b  m b == m₁  b
m-diff 1₂ = m₁==m₁
m-diff 0₂ = ¬m₀==m₁

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

adversary : IND-CCA2.Adversary
adversary rₐ pk = done CPApart
  where CPApart : CPAAdversary _
        get-m CPApart   = m₀ , m₁
        put-c CPApart c = ask (Reenc pk c rₐ) λ m′  done (m′ == m₁)

adversary-always-win :  b r  IND-CCA2.EXP b adversary r  b
adversary-always-win b (rₐ , rₖ , rₑ) = ap (flip _==_ m₁) (Reenc-correct rₖ (m b) rₑ rₐ)  m-diff b