{-# OPTIONS --without-K #-}
open import Type
open import Data.Product
open import Data.Two
module Game.IND-CPA
(PubKey : ★)
(SecKey : ★)
(Message : ★)
(CipherText : ★)
(Rₑ Rₖ Rₐ Rₓ : ★)
(KeyGen : Rₖ → PubKey × SecKey)
(Enc : PubKey → Message → Rₑ → CipherText)
where
record Adversary : ★ where
field
m : Rₐ → PubKey → 𝟚 → Message
b′ : Rₐ → PubKey → CipherText → 𝟚
R : ★
R = (Rₐ × Rₖ × Rₑ × Rₓ)
Experiment : ★
Experiment = Adversary → R → 𝟚
EXP : 𝟚 → Experiment
EXP b A (rₐ , rₖ , rₑ , _rₓ) = res
where
module A = Adversary A
pk = proj₁ (KeyGen rₖ)
mb = A.m rₐ pk b
c = Enc pk mb rₑ
res = A.b′ rₐ pk c
EXP₀ EXP₁ : Experiment
EXP₀ = EXP 0₂
EXP₁ = EXP 1₂
game : Adversary → (𝟚 × R) → 𝟚
game A (b , r) = b == EXP b A r
open import Relation.Binary.PropositionalEquality
module _
(Dist : ★)
(|Pr[_≡1]-Pr[_≡1]| : (f g : R → 𝟚) → Dist)
(dist-comm : ∀ f g → |Pr[ f ≡1]-Pr[ g ≡1]| ≡ |Pr[ g ≡1]-Pr[ f ≡1]|)
where
Advantage : Adversary → Dist
Advantage A = |Pr[ EXP₀ A ≡1]-Pr[ EXP₁ A ≡1]|
Advantage-unordered : ∀ A b → Advantage A ≡ |Pr[ EXP b A ≡1]-Pr[ EXP (not b) A ≡1]|
Advantage-unordered A 1₂ = dist-comm _ _
Advantage-unordered A 0₂ = refl