src/crypto/curve25519/x25519.bend

bend-collections@1.0.0.0 · 157 lines · 17 definitions

1import Base
2import bend-collections@1.0.0.0/src/crypto/curve25519/field.bend as F
3
4# X25519 (RFC 7748 section 5): the Montgomery ladder on Curve25519 over the
5# field of field.bend. Scalars and u-coordinates are 32-byte little-endian
6# lists (U32 values below 256); implementation == the RFC's pseudo-code
7# (spec/crypto/curve25519/x25519.bend) is proved for every input.
8#
9# The ladder runs the same operations for every scalar: the conditional
10# swap is arithmetic selection (field.bend `select`) driven by bit masks,
11# bit t of the scalar is read at a public position, and the loop count is
12# fixed (255). Bend has no timing model: this is branch-free by
13# construction, not proved constant-time.
14
15type St is Data:
16  St{x2: List<&2, U32>, z2: List<&2, U32>, x3: List<&2, U32>, z3: List<&2, U32>, swap: U32}
17
18# bit t of a little-endian byte string
19def kbit(bs: List<&2, U32>, t: Nat) -> U32:
20  match bs:
21    case Nil{}:
22      0
23    case Con{b, bt}:
24      match t:
25        case 0n:
26          U32.and(b, 1)
27        case 1n:
28          U32.and(U32.shrn(b, 1n), 1)
29        case 2n:
30          U32.and(U32.shrn(b, 2n), 1)
31        case 3n:
32          U32.and(U32.shrn(b, 3n), 1)
33        case 4n:
34          U32.and(U32.shrn(b, 4n), 1)
35        case 5n:
36          U32.and(U32.shrn(b, 5n), 1)
37        case 6n:
38          U32.and(U32.shrn(b, 6n), 1)
39        case 7n:
40          U32.and(U32.shrn(b, 7n), 1)
41        case 8n+q:
42          kbit(bt, q)
43
44# RFC 7748 decodeScalar25519's clamping: k[0] &= 248, k[31] &= 127, k[31] |= 64
45def clamp_top(xs: List<&2, U32>) -> List<&2, U32>:
46  match xs:
47    case Nil{}:
48      Nil{}
49    case Con{x, xt}:
50      match xt:
51        case Nil{}:
52          Con{U32.or(U32.and(x, 127), 64), Nil{}}
53        case Con{y, yt}:
54          Con{x, clamp_top(Con{y, yt})}
55
56def clamp(bs: List<&2, U32>) -> List<&2, U32>:
57  match bs:
58    case Nil{}:
59      Nil{}
60    case Con{b, bt}:
61      clamp_top(Con{U32.and(b, 248), bt})
62
63# a24 = 121665 as a field element
64def a24() -> List<&2, U32>:
65  [65, 219, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
66   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
67
68# one ladder step on the swapped pair (x2 : z2), (x3 : z3); c24 is a24
69def step(+c24: List<&2, U32>, +x1: List<&2, U32>, +x2: List<&2, U32>, +z2: List<&2, U32>, +x3: List<&2, U32>, +z3: List<&2, U32>, kt: U32) -> St:
70  +a = F.add(x2, z2)
71  +aa = F.sq(a)
72  +b = F.sub(x2, z2)
73  +bb = F.sq(b)
74  +e = F.sub(aa, bb)
75  +c = F.add(x3, z3)
76  +d = F.sub(x3, z3)
77  +da = F.mul(d, a)
78  +cb = F.mul(c, b)
79  St{F.mul(aa, bb), F.mul(e, F.add(aa, F.mul(e, c24))), F.sq(F.add(da, cb)), F.mul(x1, F.sq(F.sub(da, cb))), kt}
80
81# swap ^= k_t; cswap; the step; swap = k_t
82def rung(+c24: List<&2, U32>, +x1: List<&2, U32>, st: St, +kt: U32) -> St:
83  match st:
84    case St{+x2, +z2, +x3, +z3, swap}:
85      +sw = U32.xor(swap, kt)
86      step(c24, x1, F.select(sw, x2, x3), F.select(sw, z2, z3), F.select(sw, x3, x2), F.select(sw, z3, z2), kt)
87
88# the ladder's bit count, 8 len(k) - 1: 255 for a 32-byte scalar (RFC 7748
89# `bits`). Taken from the scalar, it keeps the proof checker from unfolding
90# the 255 steps for an unknown scalar.
91def len(xs: List<&2, U32>) -> Nat:
92  match xs:
93    case Nil{}:
94      0n
95    case Con{x, xt}:
96      1n+len(xt)
97
98# 8 len(xs), the bit count of a byte string
99def bitlen(xs: List<&2, U32>) -> Nat:
100  match xs:
101    case Nil{}:
102      0n
103    case Con{x, xt}:
104      Nat.add(8n, bitlen(xt))
105
106def nbits(+k: List<&2, U32>) -> Nat:
107  Nat.sub(Nat.mul(8n, len(k)), 1n)
108
109# bits t = n - 1 down to 0
110def ladder(n: Nat, +c24: List<&2, U32>, +k: List<&2, U32>, +x1: List<&2, U32>, st: St) -> St:
111  match n:
112    case 0n:
113      st
114    case 1n+ +t:
115      ladder(t, c24, k, x1, rung(c24, x1, st, kbit(k, t)))
116
117# the final cswap, then x2 * z2^(p - 2), encoded
118def finish(st: St) -> List<&2, U32>:
119  match st:
120    case St{+x2, +z2, +x3, +z3, +swap}:
121      F.to_bytes(F.mul(F.select(swap, x2, x3), F.inv(F.select(swap, z2, z3))))
122
123# X25519 on two 32-byte strings of bytes below 256
124def x25519_raw(+k: List<&2, U32>, u: List<&2, U32>) -> List<&2, U32>:
125  +x1 = F.of_bytes(u)
126  finish(ladder(nbits(k), a24(), clamp(k), x1, St{F.one(), F.zero(), x1, F.one(), 0}))
127
128# 32 values, each below 256
129def valid_bytes(n: Nat, xs: List<&2, U32>) -> Bool:
130  match n:
131    case 0n:
132      match xs:
133        case Nil{}:
134          True{}
135        case Con{x, xt}:
136          False{}
137    case 1n+m:
138      match xs:
139        case Nil{}:
140          False{}
141        case Con{x, xt}:
142          Bool.and(U32.is_lt(x, 256), valid_bytes(m, xt))
143
144def x25519_if(ok: Bool, k: List<&2, U32>, u: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
145  match ok:
146    case True{}:
147      Some{x25519_raw(k, u)}
148    case False{}:
149      None{}
150
151# X25519(k, u); None unless both are 32 bytes below 256
152def x25519(+k: List<&2, U32>, +u: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
153  x25519_if(Bool.and(valid_bytes(32n, k), valid_bytes(32n, u)), k, u)
154
155# the base point u = 9
156def base() -> List<&2, U32>:
157  F.small(9)