spec/crypto/curve25519/x25519.bend

bend-collections-laws-crypto@1.0.0.0 · 151 lines · 22 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/src/crypto/curve25519/x25519.bend as X
5
6# X25519, RFC 7748 section 5, over the natural numbers: a transcription of
7# the RFC's decodeScalar25519, decodeUCoordinate, encodeUCoordinate and the
8# Montgomery ladder pseudo-code, every operation mod p (FS.fadd, FS.fsub,
9# FS.fmul, FS.finv). HACL*'s Spec.Curve25519 is the same transcription.
10# `one` is the symbolic 1 of field.bend.
11#
12#   clause          statement
13#   X25519.value    the implementation equals this specification on every
14#                   pair of 32-byte strings (bytes below 256)
15#   X25519.checked  the checked entry point: Some of it on valid input,
16#                   None otherwise
17
18# decodeScalar25519's clamping: k[0] &= 248; k[31] &= 127; k[31] |= 64
19def clamp_last(xs: List<&2, U32>) -> List<&2, U32>:
20  match xs:
21    case Nil{}:
22      Nil{}
23    case Con{x, xt}:
24      match xt:
25        case Nil{}:
26          Con{U32.or(U32.and(x, 127), 64), Nil{}}
27        case Con{y, yt}:
28          Con{x, clamp_last(Con{y, yt})}
29
30def clamp(bs: List<&2, U32>) -> List<&2, U32>:
31  match bs:
32    case Nil{}:
33      Nil{}
34    case Con{b, bt}:
35      clamp_last(Con{U32.and(b, 248), bt})
36
37def decode_scalar(bs: List<&2, U32>) -> Nat:
38  FS.value(clamp(bs))
39
40# decodeUCoordinate: the last byte's top bit masked (bits = 255)
41def mask_last(xs: List<&2, U32>) -> List<&2, U32>:
42  match xs:
43    case Nil{}:
44      Nil{}
45    case Con{x, xt}:
46      match xt:
47        case Nil{}:
48          Con{U32.and(x, 127), Nil{}}
49        case Con{y, yt}:
50          Con{x, mask_last(Con{y, yt})}
51
52def decode_u(bs: List<&2, U32>) -> Nat:
53  FS.value(mask_last(bs))
54
55# encodeUCoordinate: u mod p as 32 little-endian bytes
56def le_bytes(n: Nat, +x: Nat) -> List<&2, U32>:
57  match n:
58    case 0n:
59      Nil{}
60    case 1n+m:
61      Con{U32.from_nat(Nat.mod(x, 256n)), le_bytes(m, Nat.div(x, 256n))}
62
63def encode_u(+p: Nat, u: Nat) -> List<&2, U32>:
64  le_bytes(32n, Nat.mod(u, p))
65
66# k_t = (k >> t) & 1
67def kbit(+k: Nat, t: Nat) -> Nat:
68  C.bit(C.high(t, k))
69
70# swap ^= k_t, on bits
71def bxor(a: Nat, b: Nat) -> Nat:
72  match a:
73    case 0n:
74      b
75    case 1n+q:
76      Nat.sub(1n, b)
77
78# cswap(swap, a, b), RFC 7748: (a, b) when swap is 0, (b, a) when it is 1;
79# cs_fst and cs_snd are its two components
80def cs_fst(swap: Nat, a: Nat, b: Nat) -> Nat:
81  match swap:
82    case 0n:
83      a
84    case 1n+q:
85      b
86
87def cs_snd(swap: Nat, a: Nat, b: Nat) -> Nat:
88  match swap:
89    case 0n:
90      b
91    case 1n+q:
92      a
93
94type LSt is Data:
95  LSt{x2: Nat, z2: Nat, x3: Nat, z3: Nat, swap: Nat}
96
97# a24 = 121665
98def a24(+one: Nat) -> Nat:
99  FS.digits(one, [65n, 219n, 1n])
100
101def step(+one: Nat, +p: Nat, +x1: Nat, +x2: Nat, +z2: Nat, +x3: Nat, +z3: Nat, kt: Nat) -> LSt:
102  +a = FS.fadd(p, x2, z2)
103  +aa = FS.fmul(p, a, a)
104  +b = FS.fsub(p, x2, z2)
105  +bb = FS.fmul(p, b, b)
106  +e = FS.fsub(p, aa, bb)
107  +c = FS.fadd(p, x3, z3)
108  +d = FS.fsub(p, x3, z3)
109  +da = FS.fmul(p, d, a)
110  +cb = FS.fmul(p, c, b)
111  +s = FS.fadd(p, da, cb)
112  +t = FS.fsub(p, da, cb)
113  LSt{FS.fmul(p, aa, bb), FS.fmul(p, e, FS.fadd(p, aa, FS.fmul(p, e, a24(one)))), FS.fmul(p, s, s), FS.fmul(p, x1, FS.fmul(p, t, t)), kt}
114
115def rung(+one: Nat, +p: Nat, +x1: Nat, st: LSt, +kt: Nat) -> LSt:
116  match st:
117    case LSt{+x2, +z2, +x3, +z3, swap}:
118      +sw = bxor(swap, kt)
119      step(one, p, x1, cs_fst(sw, x2, x3), cs_fst(sw, z2, z3), cs_snd(sw, x2, x3), cs_snd(sw, z2, z3), kt)
120
121# for t = n - 1 down to 0
122def ladder(+one: Nat, +p: Nat, n: Nat, +k: Nat, +x1: Nat, st: LSt) -> LSt:
123  match n:
124    case 0n:
125      st
126    case 1n+ +t:
127      ladder(one, p, t, k, x1, rung(one, p, x1, st, kbit(k, t)))
128
129def finish(+p: Nat, st: LSt) -> List<&2, U32>:
130  match st:
131    case LSt{x2, z2, x3, z3, +swap}:
132      encode_u(p, FS.fmul(p, cs_fst(swap, x2, x3), FS.finv(p, cs_fst(swap, z2, z3))))
133
134# RFC 7748's `bits` (255 for X25519) as 8 * len(k) - 1 of the 32-byte scalar
135def bits(k: List<&2, U32>) -> Nat:
136  Nat.sub(Nat.mul(8n, C.length(U32, k)), 1n)
137
138def x25519_p(+one: Nat, +p: Nat, +k: List<&2, U32>, u: List<&2, U32>) -> List<&2, U32>:
139  +x1 = Nat.mod(decode_u(u), p)
140  finish(p, ladder(one, p, bits(k), decode_scalar(k), x1, LSt{1n, 0n, x1, 1n, 0n}))
141
142def x25519(+one: Nat, k: List<&2, U32>, u: List<&2, U32>) -> List<&2, U32>:
143  x25519_p(one, FS.prime(one), k, u)
144
145# ---- clauses ----
146
147def X25519.value(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +u: List<&2, U32>, +hk: {FS.tight(k) == True{} : Bool}, +hu: {FS.tight(u) == True{} : Bool}) -> Type:
148  {X.x25519_raw(k, u) == x25519(one, k, u) : List<&2, U32>}
149
150def X25519.checked(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +u: List<&2, U32>) -> Type:
151  {X.x25519(k, u) == Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(k), FS.tight(u)), Some{x25519(one, k, u)}, None{}) : Maybe<&2, List<&2, U32>>}