spec/crypto/ed25519.bend

bend-collections-laws-crypto@1.0.0.0 · 327 lines · 42 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as SX
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as SHA
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
8
9# Ed25519, RFC 8032 section 5.1, over the natural numbers: a transcription
10# of the RFC's encoding (5.1.2), decoding (5.1.3), point addition and
11# doubling in extended coordinates (5.1.4), key generation (5.1.5),
12# signing (5.1.6) and verification (5.1.7, the cofactorless equation
13# [S]B == R + [k]A', with S < L required), every field operation mod p
14# (FS.fadd, ...), every scalar mod L, the hash FIPS 180-4 SHA-512
15# (spec/crypto/sha512.bend). Scalar multiplication is double-and-add over
16# the scalar's bits, most significant first (HACL*'s Spec.Ed25519 fixes an
17# algorithm in the same way). `one` is the symbolic 1 of
18# spec/crypto/curve25519/field.bend: every constant above 2^13 is written
19# with it (L, 121665, 121666).
20#
21#   clause             statement
22#   Scalar.reduce      ESC.reduce(bs) has the value value(bs) mod L
23#   Scalar.mul_add     ESC.mul_add(k, s, r) has the value (r + k s) mod L
24#   Ed25519.public     the implementation's public key is public_key(seed)
25#   Ed25519.sign       the implementation's signature is sign(seed, msg)
26#   Ed25519.verify     the implementation's verdict is verify(pk, msg, sig)
27
28# ---- scalars ----
29
30# L = 2^252 + 27742317777372353535851937790883648493, little-endian bytes
31def ell_bytes() -> List<&2, U32>:
32  [237, 211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222, 20,
33   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16]
34
35def ell(+one: Nat) -> Nat:
36  FS.uvalue(one, ell_bytes())
37
38# ---- the curve ----
39
40type EPt is Data:
41  EPt{x: Nat, y: Nat, z: Nat, t: Nat}
42
43# d = -121665 / 121666
44def dconst(+one: Nat, +p: Nat) -> Nat:
45  FS.fmul(p, FS.fsub(p, 0n, FS.digits(one, [65n, 219n, 1n])), FS.finv(p, FS.digits(one, [66n, 219n, 1n])))
46
47# 2^((p - 1) / 4), a square root of -1
48def sqm1(+p: Nat) -> Nat:
49  FS.fpow(p, 2n, Nat.div(Nat.sub(p, 1n), 4n))
50
51def identity() -> EPt:
52  EPt{0n, 1n, 1n, 0n}
53
54# 5.1.4: A = (Y1-X1)(Y2-X2), B = (Y1+X1)(Y2+X2), C = T1 2d T2, D = Z1 2 Z2,
55# E = B-A, F = D-C, G = D+C, H = B+A, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG
56def add(+p: Nat, +d: Nat, a: EPt, b: EPt) -> EPt:
57  match a b:
58    case EPt{+x1, +y1, +z1, +t1} EPt{+x2, +y2, +z2, +t2}:
59      +ea = FS.fmul(p, FS.fsub(p, y1, x1), FS.fsub(p, y2, x2))
60      +eb = FS.fmul(p, FS.fadd(p, y1, x1), FS.fadd(p, y2, x2))
61      +ec = FS.fmul(p, FS.fmul(p, t1, FS.fadd(p, d, d)), t2)
62      +ed = FS.fmul(p, FS.fadd(p, z1, z1), z2)
63      +ee = FS.fsub(p, eb, ea)
64      +ef = FS.fsub(p, ed, ec)
65      +eg = FS.fadd(p, ed, ec)
66      +eh = FS.fadd(p, eb, ea)
67      EPt{FS.fmul(p, ee, ef), FS.fmul(p, eg, eh), FS.fmul(p, ef, eg), FS.fmul(p, ee, eh)}
68
69# 5.1.4: A = X1^2, B = Y1^2, C = 2 Z1^2, H = A+B, E = H-(X1+Y1)^2, G = A-B,
70# F = C+G, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG
71def double(+p: Nat, a: EPt) -> EPt:
72  match a:
73    case EPt{+x1, +y1, +z1, t1}:
74      +ea = FS.fmul(p, x1, x1)
75      +eb = FS.fmul(p, y1, y1)
76      +zz = FS.fmul(p, z1, z1)
77      +ec = FS.fadd(p, zz, zz)
78      +eh = FS.fadd(p, ea, eb)
79      +xy = FS.fadd(p, x1, y1)
80      +ee = FS.fsub(p, eh, FS.fmul(p, xy, xy))
81      +eg = FS.fsub(p, ea, eb)
82      +ef = FS.fadd(p, ec, eg)
83      EPt{FS.fmul(p, ee, ef), FS.fmul(p, eg, eh), FS.fmul(p, ef, eg), FS.fmul(p, ee, eh)}
84
85def pick(b: Nat, q: EPt, r: EPt) -> EPt:
86  match b:
87    case 0n:
88      q
89    case 1n+c:
90      r
91
92# bits t = n - 1 .. 0 of k: q = 2 q, plus a on a one bit
93def smul(+p: Nat, +d: Nat, n: Nat, +k: Nat, +a: EPt, q: EPt) -> EPt:
94  match n:
95    case 0n:
96      q
97    case 1n+ +t:
98      +q2 = double(p, q)
99      smul(p, d, t, k, a, pick(SX.kbit(k, t), q2, add(p, d, q2, a)))
100
101# [k] a for a scalar below 2^256: 256 bits, written 2^8 one (one == 1), so
102# the proof checker never unrolls the loop
103def mul(+one: Nat, +p: Nat, +d: Nat, +k: Nat, +a: EPt) -> EPt:
104  smul(p, d, C.shift(8n, one), k, a, identity())
105
106# ---- encoding, 5.1.2 ----
107
108# the most significant bit of the final octet set to b
109def set_msb(xs: List<&2, U32>, +b: U32) -> List<&2, U32>:
110  match xs:
111    case Nil{}:
112      Nil{}
113    case Con{x, xt}:
114      match xt:
115        case Nil{}:
116          Con{U32.or(x, U32.shln(b, 7n)), Nil{}}
117        case Con{y, yt}:
118          Con{x, set_msb(Con{y, yt}, b)}
119
120# n = 32 bytes
121def encode_n(n: Nat, +p: Nat, a: EPt) -> List<&2, U32>:
122  match a:
123    case EPt{+x, +y, +z, t}:
124      +zi = FS.finv(p, z)
125      set_msb(SX.le_bytes(n, FS.fmul(p, y, zi)), U32.from_nat(Nat.mod(FS.fmul(p, x, zi), 2n)))
126
127# 32 bytes, written 2^5 one (one == 1): the byte count stays symbolic, so the
128# checker never expands an encoding (and the SHA-512 over it) into bytes
129def encode(+one: Nat, +p: Nat, a: EPt) -> List<&2, U32>:
130  encode_n(C.shift(5n, one), p, a)
131
132# ---- decoding, 5.1.3 ----
133
134def dec_fin(+p: Nat, +x: Nat, +y: Nat, +x0: Nat, fail: Bool) -> Maybe<&2, EPt>:
135  match fail:
136    case True{}:
137      None{}
138    case False{}:
139      +x2 = SX.cs_fst(SX.bxor(Nat.mod(x, 2n), x0), x, FS.fsub(p, 0n, x))
140      Some{EPt{x2, y, 1n, FS.fmul(p, x2, y)}}
141
142def dec_root(+p: Nat, +x: Nat, +y: Nat, +x0: Nat, is_u: Bool, is_nu: Bool) -> Maybe<&2, EPt>:
143  match is_u:
144    case True{}:
145      dec_fin(p, x, y, x0, Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(x0, 1n)))
146    case False{}:
147      match is_nu:
148        case True{}:
149          +x1 = FS.fmul(p, x, sqm1(p))
150          dec_fin(p, x1, y, x0, Bool.and(Nat.is_eq(x1, 0n), Nat.is_eq(x0, 1n)))
151        case False{}:
152          None{}
153
154# u = y^2 - 1, v = d y^2 + 1, x = u v^3 (u v^7)^((p-5)/8); x or x sqrt(-1)
155# when v x^2 is u or -u; fail when x = 0 and x_0 = 1; x = p - x (here as
156# -x mod p) when x mod 2 != x_0
157def dec_y(+p: Nat, +d: Nat, +y: Nat, +x0: Nat, bad: Bool) -> Maybe<&2, EPt>:
158  match bad:
159    case True{}:
160      None{}
161    case False{}:
162      +yy = FS.fmul(p, y, y)
163      +u = FS.fsub(p, yy, 1n)
164      +v = FS.fadd(p, FS.fmul(p, d, yy), 1n)
165      +v3 = FS.fmul(p, FS.fmul(p, v, v), v)
166      +v7 = FS.fmul(p, FS.fmul(p, v3, v3), v)
167      +x = FS.fmul(p, FS.fmul(p, u, v3), FS.fpow(p, FS.fmul(p, u, v7), Nat.div(Nat.sub(p, 5n), 8n)))
168      +vxx = FS.fmul(p, v, FS.fmul(p, x, x))
169      dec_root(p, x, y, x0, Nat.is_eq(vxx, u), Nat.is_eq(vxx, FS.fsub(p, 0n, u)))
170
171# bit 255 is x_0; the rest is y, rejected when y >= p
172def decode(+p: Nat, +d: Nat, +bs: List<&2, U32>) -> Maybe<&2, EPt>:
173  +y = FS.value(SX.mask_last(bs))
174  dec_y(p, d, y, SX.kbit(FS.value(bs), 255n), Bool.not(Nat.is_lt(y, p)))
175
176# ---- the base point: y = 4/5, x even ----
177
178def base_of(m: Maybe<&2, EPt>) -> EPt:
179  match m:
180    case None{}:
181      identity()
182    case Some{a}:
183      a
184
185def base(+p: Nat, +d: Nat) -> EPt:
186  base_of(decode(p, d, SX.le_bytes(32n, FS.fmul(p, 4n, FS.finv(p, 5n)))))
187
188# the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1
189def equal(+p: Nat, a: EPt, b: EPt) -> Bool:
190  match a b:
191    case EPt{+x1, +y1, +z1, t1} EPt{+x2, +y2, +z2, t2}:
192      Bool.and(Nat.is_eq(FS.fmul(p, x1, z2), FS.fmul(p, x2, z1)), Nat.is_eq(FS.fmul(p, y1, z2), FS.fmul(p, y2, z1)))
193
194# ---- bytes ----
195
196def first(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
197  match n:
198    case 0n:
199      Nil{}
200    case 1n+m:
201      match xs:
202        case Nil{}:
203          Nil{}
204        case Con{x, xt}:
205          Con{x, first(m, xt)}
206
207def rest(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
208  match n:
209    case 0n:
210      xs
211    case 1n+m:
212      match xs:
213        case Nil{}:
214          Nil{}
215        case Con{x, xt}:
216          rest(m, xt)
217
218def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
219  match xs:
220    case Nil{}:
221      ys
222    case Con{x, xt}:
223      Con{x, cat(xt, ys)}
224
225# k = SHA-512(R || A || M) mod L; a function of R first, so a comparison of
226# two such terms compares R, A and M once instead of walking the digest
227def hram(+one: Nat, rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> Nat:
228  match rb:
229    case Nil{}:
230      Nat.mod(FS.value(SHA.sha512_bytes(cat(Nil{}, cat(a, msg)))), ell(one))
231    case Con{x, xt}:
232      Nat.mod(FS.value(SHA.sha512_bytes(cat(Con{x, xt}, cat(a, msg)))), ell(one))
233
234# ---- 5.1.5 key generation ----
235
236def secret(+h: List<&2, U32>) -> Nat:
237  FS.value(SX.clamp(first(32n, h)))
238
239def public_body(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>) -> List<&2, U32>:
240  encode(one, p, mul(one, p, d, secret(h), base(p, d)))
241
242# the same, a function of d first (d = dconst(one, p) is symbolic, so the
243# checker keeps it a call instead of expanding it on every comparison)
244def public_of(+one: Nat, +p: Nat, d: Nat, +h: List<&2, U32>) -> List<&2, U32>:
245  match d:
246    case 0n:
247      public_body(one, p, 0n, h)
248    case 1n+ +e:
249      public_body(one, p, 1n+e, h)
250
251# at p = prime(one); a function of p first, so the checker keeps it a call
252# (p is symbolic) instead of expanding it whenever it compares two of them
253def public_key_at(+one: Nat, p: Nat, +seed: List<&2, U32>) -> List<&2, U32>:
254  match p:
255    case 0n:
256      public_of(one, 0n, dconst(one, 0n), SHA.sha512_bytes(seed))
257    case 1n+ +q:
258      public_of(one, 1n+q, dconst(one, 1n+q), SHA.sha512_bytes(seed))
259
260def public_key(+one: Nat, +seed: List<&2, U32>) -> List<&2, U32>:
261  public_key_at(one, FS.prime(one), seed)
262
263# ---- 5.1.6 signing ----
264
265def sign_body(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
266  +el = ell(one)
267  +a = public_of(one, p, d, h)
268  +r = Nat.mod(FS.value(SHA.sha512_bytes(cat(rest(32n, h), msg))), el)
269  +rb = encode(one, p, mul(one, p, d, r, base(p, d)))
270  +k = hram(one, rb, a, msg)
271  cat(rb, SX.le_bytes(C.shift(5n, one), Nat.mod(Nat.add(r, Nat.mul(k, secret(h))), el)))
272
273def sign_with(+one: Nat, +p: Nat, d: Nat, +h: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
274  match d:
275    case 0n:
276      sign_body(one, p, 0n, h, msg)
277    case 1n+ +e:
278      sign_body(one, p, 1n+e, h, msg)
279
280def sign_at(+one: Nat, p: Nat, +seed: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
281  match p:
282    case 0n:
283      sign_with(one, 0n, dconst(one, 0n), SHA.sha512_bytes(seed), msg)
284    case 1n+ +q:
285      sign_with(one, 1n+q, dconst(one, 1n+q), SHA.sha512_bytes(seed), msg)
286
287def sign(+one: Nat, +seed: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
288  sign_at(one, FS.prime(one), seed, msg)
289
290# ---- 5.1.7 verification (cofactorless) ----
291
292def check(+one: Nat, +p: Nat, +d: Nat, +s: Nat, +rb: List<&2, U32>, +pk: List<&2, U32>, +msg: List<&2, U32>, ra: Maybe<&2, EPt>, aa: Maybe<&2, EPt>) -> Bool:
293  match ra aa:
294    case Some{r} Some{+a}:
295      +k = hram(one, rb, pk, msg)
296      equal(p, mul(one, p, d, s, base(p, d)), add(p, d, r, mul(one, p, d, k, a)))
297    case _ _:
298      False{}
299
300def verify_with(+one: Nat, +p: Nat, +d: Nat, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +s: Nat, s_ok: Bool) -> Bool:
301  match s_ok:
302    case True{}:
303      check(one, p, d, s, rb, pk, msg, decode(p, d, rb), decode(p, d, pk))
304    case False{}:
305      False{}
306
307def verify(+one: Nat, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
308  +p = FS.prime(one)
309  +s = FS.value(rest(32n, sig))
310  verify_with(one, p, dconst(one, p), pk, msg, first(32n, sig), s, Nat.is_lt(s, ell(one)))
311
312# ---- clauses ----
313
314def Scalar.reduce(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {FS.bytes_ok(64n, bs) == True{} : Bool}) -> Type:
315  {FS.value(ESC.reduce(bs)) == Nat.mod(FS.value(bs), ell(one)) : Nat}
316
317def Scalar.mul_add(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +s: List<&2, U32>, +r: List<&2, U32>, +hk: {FS.tight(k) == True{} : Bool}, +hs: {FS.tight(s) == True{} : Bool}, +hr: {FS.tight(r) == True{} : Bool}, +hsl: {Nat.is_lt(FS.value(s), ell(one)) == True{} : Bool}, +hrl: {Nat.is_lt(FS.value(r), ell(one)) == True{} : Bool}) -> Type:
318  {FS.value(ESC.mul_add(k, s, r)) == Nat.mod(Nat.add(FS.value(r), Nat.mul(FS.value(k), FS.value(s))), ell(one)) : Nat}
319
320def Ed25519.public(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
321  {E.public_key(seed) == public_key(one, seed) : List<&2, U32>}
322
323def Ed25519.sign(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
324  {E.sign_raw(seed, msg) == sign(one, seed, msg) : List<&2, U32>}
325
326def Ed25519.verify(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +hp: {FS.tight(pk) == True{} : Bool}, +hg: {FS.bytes_ok(64n, sig) == True{} : Bool}) -> Type:
327  {E.verify_raw(pk, msg, sig) == verify(one, pk, msg, sig) : Bool}