src/crypto/ed25519/ed25519.bend

bend-collections-laws-crypto@1.0.0.0 · 73 lines · 11 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as SC
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT
7
8# Ed25519 (RFC 8032 section 5.1): key generation (5.1.5), signing (5.1.6)
9# and cofactorless verification (5.1.7: [S]B == R + [k]A', S < L checked)
10# on byte strings (U32 values below 256); SHA-512 is ../hash.bend's (proved
11# equal to FIPS 180-4).
12
13def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
14  match xs:
15    case Nil{}:
16      ys
17    case Con{x, xt}:
18      Con{x, cat(xt, ys)}
19
20# k = SHA-512(R || A || M) mod L
21def hram(rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
22  match rb:
23    case Nil{}:
24      SC.reduce(H.sha512(cat(Nil{}, cat(a, msg))))
25    case Con{x, xt}:
26      SC.reduce(H.sha512(cat(Con{x, xt}, cat(a, msg))))
27
28# the secret scalar s (pruned lower half of SHA-512(seed)) and the prefix
29def secret(+h: List<&2, U32>) -> List<&2, U32>:
30  X.clamp(F.take(32n, h))
31
32def prefix(+h: List<&2, U32>) -> List<&2, U32>:
33  F.drop(32n, h)
34
35# xs: an input (the seed or the public key), which keeps the proof checker
36# from computing the curve constants (see PT.lit)
37def public_of(+c: PT.Cs, +xs: List<&2, U32>, +h: List<&2, U32>) -> List<&2, U32>:
38  PT.encode(PT.mul(c, secret(h), PT.base(c, xs)))
39
40# A = [s]B, encoded
41def public_key(+seed: List<&2, U32>) -> List<&2, U32>:
42  public_of(PT.consts(seed), seed, H.sha512(seed))
43
44def sign_with(+c: PT.Cs, +xs: List<&2, U32>, +h: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
45  +b = PT.base(c, xs)
46  +a = public_of(c, xs, h)
47  +r = SC.reduce(H.sha512(cat(prefix(h), msg)))
48  +rb = PT.encode(PT.mul(c, r, b))
49  +k = hram(rb, a, msg)
50  cat(rb, SC.mul_add(k, SC.reduce(secret(h)), r))
51
52def sign_raw(+seed: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
53  sign_with(PT.consts(seed), seed, H.sha512(seed), msg)
54
55def check(+c: PT.Cs, +sb: List<&2, U32>, +rb: List<&2, U32>, +pk: List<&2, U32>, +msg: List<&2, U32>, ra: Maybe<&2, PT.Pt>, aa: Maybe<&2, PT.Pt>) -> Bool:
56  match ra aa:
57    case Some{r} Some{+a}:
58      +k = hram(rb, pk, msg)
59      +b = PT.base(c, pk)
60      PT.equal(PT.mul(c, sb, b), PT.add(c, r, PT.mul(c, k, a)))
61    case _ _:
62      False{}
63
64def verify_with(+c: PT.Cs, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +sb: List<&2, U32>, s_ok: Bool) -> Bool:
65  match s_ok:
66    case True{}:
67      check(c, sb, rb, pk, msg, PT.decode(c, rb), PT.decode(c, pk))
68    case False{}:
69      False{}
70
71def verify_raw(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
72  +sb = F.drop(32n, sig)
73  verify_with(PT.consts(pk), pk, msg, F.take(32n, sig), sb, SC.lt_l(sb))