spec/crypto/secp256k1/ecdsa.bend

bend-collections-laws-crypto@1.0.0.0 · 333 lines · 59 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as HM
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/main.bend as KS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
6
7# ECDSA over secp256k1, transcribed from SEC 1 v2 section 4.1 (signing
8# 4.1.3, verification 4.1.4, public key recovery 4.1.6) with the nonce of
9# RFC 6979 section 3.2 (HMAC_DRBG over HMAC-SHA256, spec/crypto/hmac.bend,
10# with qlen = hlen = 256, so bits2int is OS2IP and int2octets is I2OSP(32)),
11# the low-S rule of BIP 62 / libsecp256k1 (s > n / 2 is replaced by n - s,
12# flipping the recovery id's parity) and Ethereum's address and ECRECOVER
13# precompile. Over the natural numbers; nothing of the implementation is
14# used. Messages are 32-byte hashes. Every function takes `one` (with
15# one == 1 in every clause, see field.bend) to write p, n and G.
16#
17# Signatures are r || s || v (32 + 32 + 1 bytes, v the recovery id 0..3).
18
19def p(+one: Nat) -> Nat:
20  FS.prime(one)
21
22def n(+one: Nat) -> Nat:
23  FS.order(one)
24
25def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
26  List.append(&2, U32, xs, ys)
27
28def fill(k: Nat, +b: U32) -> List<&2, U32>:
29  List.replicate(U32, k, b)
30
31def i2osp32(+x: Nat) -> List<&2, U32>:
32  CV.i2osp(32n, x)
33
34# 1 <= x < n
35def scalar_ok(+one: Nat, +x: Nat) -> Bool:
36  Bool.and(Bool.not(Nat.is_eq(x, 0n)), Nat.is_lt(x, n(one)))
37
38# e = bits2int(H) mod n (SEC 1 4.1.3 step 5; RFC 6979 2.3.2)
39def hash_scalar(+one: Nat, +h: List<&2, U32>) -> Nat:
40  Nat.mod(CV.os2ip(h), n(one))
41
42# ---- RFC 6979 section 3.2 ----
43
44type Drbg is Data:
45  Drbg{k: List<&2, U32>, v: List<&2, U32>}
46
47# HMAC-SHA256 (the key is looked at first; the value is HM.hmac's)
48def hmac(key: List<&2, U32>, msg: List<&2, U32>) -> List<&2, U32>:
49  match key:
50    case Nil{}: HM.hmac(Nil{}, msg)
51    case k <> t: HM.hmac(k <> t, msg)
52
53def update_v(+k: List<&2, U32>, +v: List<&2, U32>) -> Drbg:
54  Drbg{k, hmac(k, v)}
55
56# K = HMAC_K(V || tag || seed), V = HMAC_K(V)
57def update(+k: List<&2, U32>, +v: List<&2, U32>, +tag: U32, +seed: List<&2, U32>) -> Drbg:
58  update_v(hmac(k, cat(v, tag <> seed)), v)
59
60def update2(d: Drbg, +seed: List<&2, U32>) -> Drbg:
61  match d:
62    case Drbg{k, v}: update(k, v, 1, seed)
63
64# steps b-g, with seed = int2octets(x) || bits2octets(h1)
65def drbg_init(+seed: List<&2, U32>) -> Drbg:
66  update2(update(fill(32n, 0), fill(32n, 1), 0, seed), seed)
67
68# ---- signing (SEC 1 4.1.3) ----
69
70type Attempt is Data:
71  Retry{}
72  Sig{sig: List<&2, U32>}
73
74# 0 or 1 when b is
75def flip(b: Bool, +par: Nat) -> Nat:
76  match b:
77    case True{}: Nat.sub(1n, par)
78    case False{}: par
79
80def low(high: Bool, +m: Nat, +s: Nat) -> Nat:
81  match high:
82    case True{}: FS.mneg(m, s)
83    case False{}: s
84
85def ge2(b: Bool) -> Nat:
86  match b:
87    case True{}: 0n
88    case False{}: 2n
89
90def finish_if(bad: Bool, +sig: List<&2, U32>) -> Attempt:
91  match bad:
92    case True{}: Retry{}
93    case False{}: Sig{sig}
94
95# R = (x, y) = [k] G, r = x mod n, s = k^-1 (e + r d) mod n; r = 0 or
96# s = 0 means another k. s > n / 2 (n is odd: n < 2 s) becomes n - s. The
97# recovery id is (y mod 2) + 2 (x >= n), with its low bit flipped when s was
98# replaced.
99def finish(+one: Nat, +e: Nat, +d: Nat, +k: Nat, a: CV.SAffine) -> Attempt:
100  match a:
101    case CV.SAffine{+x, +y}:
102      +m = n(one)
103      +r = Nat.mod(x, m)
104      +s = FS.mmul(m, FS.minv(m, k), FS.madd(m, e, FS.mmul(m, r, d)))
105      +high = Nat.is_lt(m, Nat.double(s))
106      finish_if(Bool.or(Nat.is_eq(r, 0n), Nat.is_eq(s, 0n)), cat(i2osp32(r), cat(i2osp32(low(high, m, s)), [U32.from_nat(Nat.add(ge2(Nat.is_lt(x, m)), flip(high, Nat.mod(y, 2n))))])))
107
108def attempt_ok(+one: Nat, +e: Nat, +d: Nat, +k: Nat, ok: Bool) -> Attempt:
109  match ok:
110    case True{}: finish(one, e, d, k, CV.to_affine(p(one), CV.pmul(p(one), k, CV.g(one))))
111    case False{}: Retry{}
112
113# step h.3: k = bits2int(T) with T = V, used when 1 <= k < n
114def attempt(+one: Nat, +e: Nat, +d: Nat, +v: List<&2, U32>) -> Attempt:
115  +k = CV.os2ip(v)
116  attempt_ok(one, e, d, k, scalar_ok(one, k))
117
118# step h, with the retry of step h.3 (K = HMAC_K(V || 0x00),
119# V = HMAC_K(V)) before the next V = HMAC_K(V); at most `fuel` candidates
120def sign_loop(fuel: Nat, +one: Nat, +e: Nat, +d: Nat, +k: List<&2, U32>, +v: List<&2, U32>, att: Attempt) -> Maybe<&2, List<&2, U32>>:
121  match fuel att:
122    case 0n Retry{}: None{}
123    case 0n Sig{sig}: Some{sig}
124    case 1n+f Retry{}:
125      +k2 = hmac(k, cat(v, [0]))
126      +v3 = hmac(k2, hmac(k2, v))
127      sign_loop(f, one, e, d, k2, v3, attempt(one, e, d, v3))
128    case 1n+f Sig{sig}: Some{sig}
129
130def sign_drbg(+one: Nat, +e: Nat, +d: Nat, g: Drbg) -> Maybe<&2, List<&2, U32>>:
131  match g:
132    case Drbg{+k, +v}:
133      +v1 = hmac(k, v)
134      sign_loop(16n, one, e, d, k, v1, attempt(one, e, d, v1))
135
136def sign_d(+one: Nat, +h: List<&2, U32>, +d: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
137  match ok:
138    case True{}:
139      +e = hash_scalar(one, h)
140      sign_drbg(one, e, d, drbg_init(cat(i2osp32(d), i2osp32(e))))
141    case False{}: None{}
142
143# sign(sk, H): d = OS2IP(sk) must be a 32-byte key with 1 <= d < n, H 32 bytes
144def sign(+one: Nat, +sk: List<&2, U32>, +h: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
145  sign_d(one, h, CV.os2ip(sk), Bool.and(CV.length_is(32n, h), Bool.and(CV.length_is(32n, sk), scalar_ok(one, CV.os2ip(sk)))))
146
147# ---- public keys ----
148
149def pk_of(+one: Nat, compressed: Bool, +q: CV.SPoint) -> List<&2, U32>:
150  match compressed:
151    case True{}: CV.encode_compressed(p(one), q)
152    case False{}: CV.encode_uncompressed(p(one), q)
153
154def public_d(+one: Nat, compressed: Bool, +d: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
155  match ok:
156    case True{}: Some{pk_of(one, compressed, CV.pmul(p(one), d, CV.g(one)))}
157    case False{}: None{}
158
159# the SEC 1 encoding of Q = [d] G
160def public_key(+one: Nat, +sk: List<&2, U32>, compressed: Bool) -> Maybe<&2, List<&2, U32>>:
161  public_d(one, compressed, CV.os2ip(sk), Bool.and(CV.length_is(32n, sk), scalar_ok(one, CV.os2ip(sk))))
162
163# ---- verification (SEC 1 4.1.4) ----
164
165# u1 = e s^-1, u2 = r s^-1, R = [u1] G + [u2] Q; valid when R is not the
166# point at infinity and x(R) mod n = r
167def verify_rs(+one: Nat, +q: CV.SPoint, +e: Nat, +r: Nat, +s: Nat) -> Bool:
168  +m = n(one)
169  +w = FS.minv(m, s)
170  +rr = CV.padd(p(one), CV.pmul(p(one), FS.mmul(m, e, w), CV.g(one)), CV.pmul(p(one), FS.mmul(m, r, w), q))
171  Bool.and(Bool.not(CV.is_inf(rr)), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(p(one), rr)), m), r))
172
173def verify_ok(+one: Nat, +q: CV.SPoint, +e: Nat, +r: Nat, +s: Nat, ok: Bool) -> Bool:
174  match ok:
175    case True{}: verify_rs(one, q, e, r, s)
176    case False{}: False{}
177
178# r and s in [1, n - 1]; strict verification also rejects s > n / 2
179def verify_q(+one: Nat, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, mq: Maybe<&2, CV.SPoint>) -> Bool:
180  match mq:
181    case None{}: False{}
182    case Some{+q}:
183      +r = CV.os2ip(CV.first(32n, sig))
184      +s = CV.os2ip(CV.after(32n, sig))
185      verify_ok(one, q, hash_scalar(one, h), r, s, Bool.and(Bool.and(scalar_ok(one, r), scalar_ok(one, s)), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(n(one), Nat.double(s))))))
186
187def verify_len(+one: Nat, +pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, ok: Bool) -> Bool:
188  match ok:
189    case True{}: verify_q(one, h, sig, strict, CV.decode(p(one), pk))
190    case False{}: False{}
191
192# verify(Q, H, r || s): Q a SEC 1 public key, H 32 bytes, r || s 64 bytes
193def verify(+one: Nat, +pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool) -> Bool:
194  verify_len(one, pk, h, sig, strict, Bool.and(CV.length_is(32n, h), CV.length_is(64n, sig)))
195
196# ---- public key recovery (SEC 1 4.1.6) ----
197
198def recover_q_if(+one: Nat, +q: CV.SPoint, inf: Bool) -> Maybe<&2, List<&2, U32>>:
199  match inf:
200    case True{}: None{}
201    case False{}: Some{CV.encode_uncompressed(p(one), q)}
202
203def recover_q(+one: Nat, +q: CV.SPoint) -> Maybe<&2, List<&2, U32>>:
204  recover_q_if(one, q, CV.is_inf(q))
205
206# Q = r^-1 (s R - e G) = [-e r^-1] G + [s r^-1] R
207def recover_r(+one: Nat, +e: Nat, +r: Nat, +s: Nat, mr: Maybe<&2, CV.SPoint>) -> Maybe<&2, List<&2, U32>>:
208  match mr:
209    case None{}: None{}
210    case Some{+pr}:
211      +m = n(one)
212      +ri = FS.minv(m, r)
213      recover_q(one, CV.padd(p(one), CV.pmul(p(one), FS.mmul(m, FS.mneg(m, e), ri), CV.g(one)), CV.pmul(p(one), FS.mmul(m, s, ri), pr)))
214
215# R: the point of x-coordinate x = r + j n (j = id / 2, x < p) whose y has
216# parity id mod 2
217def recover_x_if(+one: Nat, +e: Nat, +r: Nat, +s: Nat, +id: Nat, +x: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
218  match ok:
219    case True{}: recover_r(one, e, r, s, CV.decompress(p(one), x, Nat.mod(id, 2n)))
220    case False{}: None{}
221
222def recover_x(+one: Nat, +e: Nat, +r: Nat, +s: Nat, +id: Nat) -> Maybe<&2, List<&2, U32>>:
223  +x = Nat.add(r, Nat.mul(Nat.div(id, 2n), n(one)))
224  recover_x_if(one, e, r, s, id, x, Nat.is_lt(x, p(one)))
225
226def recover_ok(+one: Nat, +e: Nat, +r: Nat, +s: Nat, +id: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
227  match ok:
228    case True{}: recover_x(one, e, r, s, id)
229    case False{}: None{}
230
231def recover_len(+one: Nat, +h: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
232  match ok:
233    case True{}:
234      +r = CV.os2ip(CV.first(32n, sig))
235      +s = CV.os2ip(CV.first(32n, CV.after(32n, sig)))
236      +id = U32.to_nat(CV.head(CV.after(64n, sig)))
237      recover_ok(one, hash_scalar(one, h), r, s, id, Bool.and(Bool.and(scalar_ok(one, r), scalar_ok(one, s)), Nat.is_lt(id, 4n)))
238    case False{}: None{}
239
240# the 65-byte uncompressed key recovered from H (32 bytes) and
241# r || s || id (65 bytes, id in 0..3)
242def recover(+one: Nat, +h: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
243  recover_len(one, h, sig, Bool.and(CV.length_is(32n, h), CV.length_is(65n, sig)))
244
245# ---- Ethereum ----
246
247# Keccak-256 (spec/crypto/keccak/main.bend) of bytes packed into
248# little-endian U32 words, as its interface takes them
249def word(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
250  U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n)))
251
252def words(k: Nat, +bs: List<&2, U32>) -> List<&2, U32>:
253  match k:
254    case 0n: Nil{}
255    case 1n+j: word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> words(j, CV.after(4n, bs))
256
257def pack(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> Array<U32>:
258  match ws:
259    case Nil{}: a
260    case w <> t: pack(t, U32.inc(i), Array.set(U32, a, i, w))
261
262def unpack(ws: List<&1, U32>) -> List<&2, U32>:
263  match ws:
264    case Nil{}: Nil{}
265    case +w <> t: U32.and(w, 255) <> U32.and(U32.shrn(w, 8n), 255) <> U32.and(U32.shrn(w, 16n), 255) <> U32.shrn(w, 24n) <> unpack(t)
266
267def digest_bytes(m: Maybe<&1, Array<U32>>) -> List<&2, U32>:
268  match m:
269    case None{}: Nil{}
270    case Some{a}: unpack(Array.to_list(~U32, a))
271
272# The hash of addresses: Keccak-256 (spec/crypto/keccak/main.bend, 24
273# rounds), named by a value so that the proofs can keep it folded
274type Hash is Data:
275  Keccak256{}
276
277def hash(+h: Hash, a: Array<U32>, length: Nat) -> Maybe<&1, Array<U32>>:
278  match h:
279    case Keccak256{}: KS.keccak256_rounds(24n, a, length)
280
281def keccak64(+h: Hash, +bs: List<&2, U32>) -> List<&2, U32>:
282  digest_bytes(hash(h, pack(words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n))
283
284# address = the last 20 bytes of Keccak-256(x || y) of an uncompressed key
285def eth_if(ok: Bool, +dg: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
286  match ok:
287    case True{}: Some{CV.after(12n, dg)}
288    case False{}: None{}
289
290def eth_go(+h: Hash, +pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
291  eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), keccak64(h, CV.after(1n, pk)))
292
293# (the key is looked at first, so that the proof checker keeps an unknown
294# address folded)
295def eth_with(+h: Hash, pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
296  match pk:
297    case Nil{}: eth_go(h, Nil{})
298    case b <> t: eth_go(h, b <> t)
299
300def eth_address(+pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
301  eth_with(Keccak256{}, pk)
302
303def word_of(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
304  match m:
305    case None{}: None{}
306    case Some{a}: Some{cat(fill(12n, 0), a)}
307
308def addr_word(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
309  match m:
310    case None{}: None{}
311    case Some{pk}: word_of(eth_address(pk))
312
313def all_zero(bs: List<&2, U32>) -> Bool:
314  match bs:
315    case Nil{}: True{}
316    case b <> t: Bool.and(U32.is_eq(b, 0), all_zero(t))
317
318def ecrecover_v(+one: Nat, +h: List<&2, U32>, +rs: List<&2, U32>, +v: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>:
319  match ok:
320    case True{}: addr_word(recover(one, h, cat(rs, [U32.sub(v, 27)])))
321    case False{}: None{}
322
323def ecrecover_in(+one: Nat, +x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
324  +vw = CV.first(32n, CV.after(32n, x))
325  +v = CV.head(CV.after(31n, vw))
326  ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), v, Bool.and(all_zero(CV.first(31n, vw)), Bool.or(U32.is_eq(v, 27), U32.is_eq(v, 28))))
327
328# ECRECOVER (precompile 0x01): the input zero-padded or cut to 128 bytes is
329# H || v || r || s, v a 32-byte big-endian word that must be 27 or 28;
330# the output is the address word (12 zero bytes, then the address) of the
331# key recovered with id v - 27, or nothing
332def ecrecover(+one: Nat, input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
333  ecrecover_in(one, CV.first(128n, cat(input, fill(128n, 0))))