Converting signature keys into NIKE keys

Both directions return Option, since the conversion may be partial. Conversion does not commute with Blindable.blindPriv, so convert_derive covers root keys only.

structure Cryptlib.Primitives.Sign.Convert.KeyConvert (S : Sign.Signature) (N : NIKE.NIKE.NIKE) : Type

A conversion from a signature scheme's keys into a NIKE's keys.

• toNikePub : S.PublicKey → Option N.PublicKey
• toNikePriv : S.PrivateKey → Option N.PrivateKey
• convert_derive (sk : S.PrivateKey) (nsk : N.PrivateKey) (npk : N.PublicKey) : self.toNikePriv sk = some nsk → self.toNikePub (S.pub sk) = some npk → N.derivePublicKey nsk = npk

  Converting then deriving agrees with deriving then converting.

theorem Cryptlib.Primitives.Sign.Convert.converted_pub_safe {S : Sign.Signature} {N : NIKE.NIKE.NIKE} (C : KeyConvert S N) (sk : S.PrivateKey) (nsk : N.PrivateKey) (npk : N.PublicKey) (h₁ : C.toNikePriv sk = some nsk) (h₂ : C.toNikePub (S.pub sk) = some npk) : N.Safe npk

A converted public key whose private key also converts is Safe.

def Cryptlib.Primitives.Sign.Convert.stub (S : Sign.Signature) (N : NIKE.NIKE.NIKE) : KeyConvert S N

The stub conversion: nothing converts. Vacuously lawful.

Equations

• Cryptlib.Primitives.Sign.Convert.stub S N = { toNikePub := fun (x : S.PublicKey) => none, toNikePriv := fun (x : S.PrivateKey) => none, convert_derive := ⋯ }