ECDSA deterministic signature with public key recovery for secp256k1.

ECDSA signatures are specified in Standards for Efficient Cryptography 1 (SEC 1) in general, and their deterministic version is specified in the RFC 6979 standard. The public key recovery aspects are also described in SEC 1.

ECDSA, as specified in SEC 1, relies on a randomly generated ephemeral private key for each signature. RFC 6979 describes a procedure to generate a deterministic but unpredictable ephemeral private key (from the message and the signing key), which can be considered indistinguishable from a random one. The details of this are unimportant for the interface introduced here, but the point is that, since the ephemeral private key is deterministically generated, the constrained ACL2 function introduced here requires no additional inputs related to the random generation of the ephemeral private key.

ECDSA is parameterized over a hash function applied to the message prior to the creation of the signature. To avoid this explicit dependency in our ACL2 function, we have it take as input a hash of the message instead of the message: this sidesteps the choice of the hash function, providing the ability to sign messages that are hashed by external means.

According to RFC 6979, the same hash function is used as part of the procedure to deterministically generate the ephemeral private key. Mathematically speaking, one could well use a different hash function though. For now, our constrained ACL2 function is agnostic in regard to the RFC 6979 hash function, and can be in fact made executable via attachments that pick different hash functions.

An ECDSA signature consists of a pair

An ECDSA signature may involve the generation of successive
random or (random-looking) deterministic ephemeral private keys
until valid

If

To summarize, our constrained function takes as inputs a hash (a list of bytes), a private key, and two boolean flags, as formalized by the guard.

The function returns as outputs:
an error flag, constrained to be a boolean;
a public key recovery

We constrain this function to return results of the types described above unconditionally. We also constrain it to fix its arguments to the guard types.

See also:

- Deterministic ECDSA executable specification
- attaching Deterministic ECDSA executable specification to this interface

**Theorem: **

(defthm booleanp-of-mv-nth-0-secp256k1-sign-det-rec (booleanp (mv-nth 0 (secp256k1-sign-det-rec hash priv small-x? small-s?))))

**Theorem: **

(defthm natp-of-mv-nth-1-secp256k1-sign-det-rec (natp (mv-nth 1 (secp256k1-sign-det-rec hash priv small-x? small-s?))))

**Theorem: **

(defthm booleanp-of-mv-nth-2-secp256k1-sign-det-rec (booleanp (mv-nth 2 (secp256k1-sign-det-rec hash priv small-x? small-s?))))

**Theorem: **

(defthm secp256k1-fieldp-of-mv-nth-3-secp256k1-sign-det-rec (secp256k1-fieldp (mv-nth 3 (secp256k1-sign-det-rec hash priv small-x? small-s?))))

**Theorem: **

(defthm secp256k1-fieldp-of-mv-nth-4-secp256k1-sign-det-rec (secp256k1-fieldp (mv-nth 4 (secp256k1-sign-det-rec hash priv small-x? small-s?))))

**Theorem: **

(defthm secp256k1-sign-det-rec-fixes-input-hash (equal (secp256k1-sign-det-rec (byte-list-fix hash) priv small-x? small-s?) (secp256k1-sign-det-rec hash priv small-x? small-s?)))

**Theorem: **

(defthm secp256k1-sign-det-rec-fixes-input-priv (equal (secp256k1-sign-det-rec hash (secp256k1-priv-key-fix priv) small-x? small-s?) (secp256k1-sign-det-rec hash priv small-x? small-s?)))

**Theorem: **

(defthm secp256k1-sign-det-rec-fixes-input-small-x? (equal (secp256k1-sign-det-rec hash priv (bool-fix small-x?) small-s?) (secp256k1-sign-det-rec hash priv small-x? small-s?)))

**Theorem: **

(defthm secp256k1-sign-det-rec-fixes-input-small-s? (equal (secp256k1-sign-det-rec hash priv small-x? (bool-fix small-s?)) (secp256k1-sign-det-rec hash priv small-x? small-s?)))

**Theorem: **

(defthm byte-list-equiv-implies-equal-secp256k1-sign-det-rec-1 (implies (byte-list-equiv hash hash-equiv) (equal (secp256k1-sign-det-rec hash priv small-x? small-s?) (secp256k1-sign-det-rec hash-equiv priv small-x? small-s?))) :rule-classes (:congruence))

**Theorem: **

(defthm secp256k1-priv-key-equiv-implies-equal-secp256k1-sign-det-rec-2 (implies (secp256k1-priv-key-equiv priv priv-equiv) (equal (secp256k1-sign-det-rec hash priv small-x? small-s?) (secp256k1-sign-det-rec hash priv-equiv small-x? small-s?))) :rule-classes (:congruence))

**Theorem: **

(defthm iff-implies-equal-secp256k1-sign-det-rec-3 (implies (iff small-x? small-x?-equiv) (equal (secp256k1-sign-det-rec hash priv small-x? small-s?) (secp256k1-sign-det-rec hash priv small-x?-equiv small-s?))) :rule-classes (:congruence))

**Theorem: **

(defthm iff-implies-equal-secp256k1-sign-det-rec-4 (implies (iff small-s? small-s?-equiv) (equal (secp256k1-sign-det-rec hash priv small-x? small-s?) (secp256k1-sign-det-rec hash priv small-x? small-s?-equiv))) :rule-classes (:congruence))