{-# OPTIONS --without-K #-}
module Crypto.Schemes where

open import Type
open import Data.Product
open import Relation.Binary.PropositionalEquality

record PublicKeyEncryption : ★₁ where
  constructor mk
  field
    PubKey SecKey Message CipherText Rₖ Rₑ : 
    KeyGen : Rₖ  PubKey × SecKey
    Enc : PubKey  Message  Rₑ  CipherText
    Dec : SecKey  CipherText  Message

  FunctionallyCorrect : 
  FunctionallyCorrect =
     rₖ rₑ m  let (pk , sk) = KeyGen rₖ in
                 Dec sk (Enc pk m rₑ)  m