Asymmetric Encryption Schemes.

This file defines a type AsymmEncAlg spec σ M PK SK C to represent an protocol for asymmetric encryption using oracles in spec, with message space M, public/secret keys PK and SK, and ciphertext space C.

structure SignatureAlg (m : Type → Type v) (M PK SK S : Type) extends ExecutionMethod m : Type (max 1 v)

Signature algorithm with computations in the monad m, where M is the space of messages, PK/SK are the spaces of the public/private keys, and S is the type of the final signature.

• exec {α : Type} : m α → ProbComp α
• lift_probComp {α : Type} : ProbComp α → m α
• exec_lift_probComp {α : Type} (px : ProbComp α) : self.exec (self.lift_probComp px) = px
• keygen : m (PK × SK)
• sign (pk : PK) (sk : SK) (msg : M) : m S
• verify (pk : PK) (msg : M) (σ : S) : m Bool