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

def SignatureAlg.signingOracle {m : Type → Type v} [Monad m] {M PK SK S : Type} (sigAlg : SignatureAlg m M PK SK S) (pk : PK) (sk : SK) : QueryImpl (M →ₒ S) (WriterT (M →ₒ S).QueryLog m)

Equations

• One or more equations did not get rendered due to their size.

def SignatureAlg.PerfectlyComplete {m : Type → Type v} [Monad m] {M PK SK S : Type} (sigAlg : SignatureAlg m M PK SK S) : Prop

a SignatureAlg is perfectly complete if honest signatures are always verified.

Equations

• One or more equations did not get rendered due to their size.

structure SignatureAlg.unforgeableAdv {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} (_sigAlg : SignatureAlg (OracleComp spec) M PK SK S) : Type (max (max 1 u) u_1)

Adversary for testing the unforgeability of a signature scheme. We only define this if the monad for the protocol is OracleComp spec, as we need to be able to give the adversary access to a signing oracle.

• main (pk : PK) : OracleComp (spec ++ₒ (M →ₒ S)) (M × S)

def SignatureAlg.unforgeableExp {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} [DecidableEq M] [DecidableEq S] {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (adv : sigAlg.unforgeableAdv) : ProbComp Bool

Unforgeability expiriment for a signature algorithm runs the adversary and checks returns whether or not the adversary successfully forged a signature

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SignatureAlg.unforgeableAdv.advantage {ι : Type u} {spec : OracleSpec ι} {M PK SK S : Type} [DecidableEq M] [DecidableEq S] {sigAlg : SignatureAlg (OracleComp spec) M PK SK S} (adv : sigAlg.unforgeableAdv) : ENNReal

Advantage

Equations

• adv.advantage = [=true|SignatureAlg.unforgeableExp adv]