~/jendhub

spec/crypto/secp256k1/schnorr.bend

bend-collections-laws-crypto@1.0.0.0 · 168 lines · 32 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5
6# BIP-340 Schnorr signatures, transcribed from the BIP's "Default Signing"
7# and "Verification" sections (and its reference.py), over the natural
8# numbers and the FIPS 180-4 SHA-256 specification spec/crypto/sha.bend.
9# Nothing of the implementation is used. Every function takes `one`
10# (one == 1 in every clause, see field.bend) to write p, n and G.
11
12def p(+one: Nat) -> Nat:
13  FS.prime(one)
14
15def n(+one: Nat) -> Nat:
16  FS.order(one)
17
18def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
19  List.append(&2, U32, xs, ys)
20
21def bytes32(+x: Nat) -> List<&2, U32>:
22  CV.i2osp(32n, x)
23
24def tagged_h(+th: List<&2, U32>, x: List<&2, U32>) -> List<&2, U32>:
25  FIPS.sha256_bytes(cat(th, cat(th, x)))
26
27# hash_name(x) = SHA256(SHA256(name) || SHA256(name) || x), name in ASCII
28def tagged(tag: List<&2, U32>, x: List<&2, U32>) -> List<&2, U32>:
29  tagged_h(FIPS.sha256_bytes(tag), x)
30
31# "BIP0340/aux", "BIP0340/nonce", "BIP0340/challenge"
32def tag_aux() -> List<&2, U32>:
33  [66, 73, 80, 48, 51, 52, 48, 47, 97, 117, 120]
34
35def tag_nonce() -> List<&2, U32>:
36  [66, 73, 80, 48, 51, 52, 48, 47, 110, 111, 110, 99, 101]
37
38def tag_challenge() -> List<&2, U32>:
39  [66, 73, 80, 48, 51, 52, 48, 47, 99, 104, 97, 108, 108, 101, 110, 103, 101]
40
41def xor_bytes(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
42  match xs ys:
43    case x <> xt y <> yt: U32.xor(x, y) <> xor_bytes(xt, yt)
44    case _ _: Nil{}
45
46# n - x when y is odd (the key or nonce whose point has even y)
47def even_b(+m: Nat, b: Nat, +x: Nat) -> Nat:
48  match b:
49    case 0n: x
50    case 1n+k: FS.mneg(m, x)
51
52def even(+m: Nat, +y: Nat, +x: Nat) -> Nat:
53  even_b(m, Nat.mod(y, 2n), x)
54
55# ---- verification ----
56
57# lift_x(x): the point with x-coordinate x and even y, if x < p and
58# x^3 + 7 is a square
59def lift_if(+one: Nat, +x: Nat, ok: Bool) -> Maybe<&2, CV.SPoint>:
60  match ok:
61    case True{}: CV.decompress(p(one), x, 0n)
62    case False{}: None{}
63
64def lift_x(+one: Nat, +x: Nat) -> Maybe<&2, CV.SPoint>:
65  lift_if(one, x, Nat.is_lt(x, p(one)))
66
67# fail if is_infinite(R) or not has_even_y(R) or x(R) != r
68def check_r(+r: Nat, inf: Bool, a: CV.SAffine) -> Bool:
69  match a:
70    case CV.SAffine{x, y}: Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(y, 2n), 0n), Nat.is_eq(x, r)))
71
72# R = s G - e P with e = int(hash_challenge(r || pk || m)) mod n
73def verify_rs(+one: Nat, +r: Nat, +s: Nat, +e: Nat, +pp: CV.SPoint) -> Bool:
74  +rr = CV.padd(p(one), CV.pmul(p(one), s, CV.g(one)), CV.pmul(p(one), FS.mneg(n(one), e), pp))
75  check_r(r, CV.is_inf(rr), CV.to_affine(p(one), rr))
76
77def verify_ok(+one: Nat, +r: Nat, +s: Nat, +e: Nat, +pp: CV.SPoint, ok: Bool) -> Bool:
78  match ok:
79    case True{}: verify_rs(one, r, s, e, pp)
80    case False{}: False{}
81
82# fail if r >= p or s >= n
83def verify_p(+one: Nat, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, mp: Maybe<&2, CV.SPoint>) -> Bool:
84  match mp:
85    case None{}: False{}
86    case Some{+pp}:
87      +r = CV.os2ip(CV.first(32n, sig))
88      +s = CV.os2ip(CV.after(32n, sig))
89      +e = Nat.mod(CV.os2ip(tagged(tag_challenge(), cat(CV.first(32n, sig), cat(pk, m)))), n(one))
90      verify_ok(one, r, s, e, pp, Bool.and(Nat.is_lt(r, p(one)), Nat.is_lt(s, n(one))))
91
92def verify_len(+one: Nat, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Bool:
93  match ok:
94    case True{}: verify_p(one, pk, m, sig, lift_x(one, CV.os2ip(pk)))
95    case False{}: False{}
96
97# Verify(pk, m, sig): pk 32 bytes, sig 64 bytes, m any length
98def verify(+one: Nat, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
99  verify_len(one, pk, m, sig, Bool.and(CV.length_is(32n, pk), CV.length_is(64n, sig)))
100
101# ---- signing ----
102
103# d' = int(sk), 1 <= d' <= n - 1
104def secret_ok(+one: Nat, +sk: List<&2, U32>) -> Bool:
105  Bool.and(CV.length_is(32n, sk), Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), n(one))))
106
107def pub_of(a: CV.SAffine) -> List<&2, U32>:
108  match a:
109    case CV.SAffine{x, y}: bytes32(x)
110
111def pubkey_ok(+one: Nat, +sk: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
112  match ok:
113    case True{}: Some{pub_of(CV.to_affine(p(one), CV.pmul(p(one), CV.os2ip(sk), CV.g(one))))}
114    case False{}: None{}
115
116# PubKey(sk) = bytes(d' G)
117def pubkey(+one: Nat, +sk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
118  pubkey_ok(one, sk, secret_ok(one, sk))
119
120# sig = bytes(R) || bytes((k + e d) mod n); if Verify(bytes(P), m, sig)
121# fails, abort
122def sign_if(+sig: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
123  match ok:
124    case True{}: Some{sig}
125    case False{}: None{}
126
127def sign_fin(+one: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
128  sign_if(sig, verify(one, pb, m, sig))
129
130# R = k' G; k = k' if has_even_y(R), otherwise n - k';
131# e = int(hash_challenge(bytes(R) || bytes(P) || m)) mod n
132def sign_r(+one: Nat, +d: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: Nat, ra: CV.SAffine) -> Maybe<&2, List<&2, U32>>:
133  match ra:
134    case CV.SAffine{rx, +ry}:
135      +k = even(n(one), ry, k0)
136      +rb = bytes32(rx)
137      +e = Nat.mod(CV.os2ip(tagged(tag_challenge(), cat(rb, cat(pb, m)))), n(one))
138      sign_fin(one, pb, m, cat(rb, bytes32(FS.madd(n(one), k, FS.mmul(n(one), e, d)))))
139
140# k' = int(rand) mod n; fail if k' = 0
141def sign_kz(+one: Nat, +d: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: Nat, zero: Bool) -> Maybe<&2, List<&2, U32>>:
142  match zero:
143    case True{}: None{}
144    case False{}: sign_r(one, d, pb, m, k0, CV.to_affine(p(one), CV.pmul(p(one), k0, CV.g(one))))
145
146def sign_k(+one: Nat, +d: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: Nat) -> Maybe<&2, List<&2, U32>>:
147  sign_kz(one, d, pb, m, k0, Nat.is_eq(k0, 0n))
148
149# P = d' G; d = d' if has_even_y(P), otherwise n - d';
150# t = bytes(d) xor hash_aux(a); rand = hash_nonce(t || bytes(P) || m)
151def sign_p(+one: Nat, +d0: Nat, +m: List<&2, U32>, +aux: List<&2, U32>, pa: CV.SAffine) -> Maybe<&2, List<&2, U32>>:
152  match pa:
153    case CV.SAffine{px, +py}:
154      +d = even(n(one), py, d0)
155      +pb = bytes32(px)
156      +t = xor_bytes(bytes32(d), tagged(tag_aux(), aux))
157      sign_k(one, d, pb, m, Nat.mod(CV.os2ip(tagged(tag_nonce(), cat(t, cat(pb, m)))), n(one)))
158
159def sign_ok(+one: Nat, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
160  match ok:
161    case True{}:
162      +d0 = CV.os2ip(sk)
163      sign_p(one, d0, m, aux, CV.to_affine(p(one), CV.pmul(p(one), d0, CV.g(one))))
164    case False{}: None{}
165
166# Sign(sk, m, a): sk and a 32 bytes, m any length
167def sign(+one: Nat, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
168  sign_ok(one, sk, m, aux, Bool.and(CV.length_is(32n, aux), secret_ok(one, sk)))