Digital signature schemes

Signing randomness lives in StateM State; verify_sign quantifies over every state, so a randomized signer must verify for every nonce. Key generation is a pure function of a seed. Signatures are fixed-size and sign is total, which excludes stateful schemes such as XMSS.

structure Cryptlib.Primitives.Sign.Sign.Signature : Type 1

• State : Type
• PublicKey : Type
• PrivateKey : Type
• Sig : Type
• seedSize : Nat
• publicKeySize : Nat
• privateKeySize : Nat
• sigSize : Nat
• encodePublicKey : self.PublicKey → Vector UInt8 self.publicKeySize
• decodePublicKey : Vector UInt8 self.publicKeySize → Option self.PublicKey
• encodePrivateKey : self.PrivateKey → Vector UInt8 self.privateKeySize
• decodePrivateKey : Vector UInt8 self.privateKeySize → Option self.PrivateKey
• encodeSig : self.Sig → Vector UInt8 self.sigSize
• decodeSig : Vector UInt8 self.sigSize → Option self.Sig
• privateKeyFromSeed : Vector UInt8 self.seedSize → self.PrivateKey

  Key generation from a caller-supplied seed.

• pub : self.PrivateKey → self.PublicKey
• sign : self.PrivateKey → ByteArray → StateM self.State self.Sig

  Stateful only to carry signing randomness.

• verify : self.PublicKey → ByteArray → self.Sig → Bool
• decode_encode_pub (pk : self.PublicKey) : self.decodePublicKey (self.encodePublicKey pk) = some pk
• decode_encode_priv (sk : self.PrivateKey) : self.decodePrivateKey (self.encodePrivateKey sk) = some sk
• decode_encode_sig (s : self.Sig) : self.decodeSig (self.encodeSig s) = some s
• verify_sign (sk : self.PrivateKey) (m : ByteArray) (s : self.State) : self.verify (self.pub sk) m (self.sign sk m s).fst = true

  Correctness, for every private key and every signing state.

@[instance_reducible]

instance Cryptlib.Primitives.Sign.Sign.instInhabitedSignature : Inhabited Signature

The trivial scheme: one key, one signature, everything verifies. Insecure.

Equations

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