Skip to content

Commit 14e9ec0

Browse files
committed
feat(moonapi): EdDSA (Ed25519) JWT verification.
Completes the jose signature set — HS256, RS256, ES256, and now EdDSA. ed25519.mbt transcribes Edwards25519 on core BigInt and the module's own SHA-512: point decompression by the p ≡ 5 (mod 8) square root, the complete twisted-Edwards addition law, scalar multiplication, and the RFC 8032 §5.1.7 check [S]B = R + [k]A. jwt_verify_eddsa (RFC 8037) wraps it and refuses an alg downgrade. Verified against the RFC 8032 §7.1 test vectors (TEST 1 and TEST 3) and a real EdDSA JWT; a self-consistency test recomputes p and d independently of their hardcoded hex, which caught a transcription typo during development. Passes on wasm, wasm-gc, js, and native. Signed-off-by: 林晨 (Leo Cheng) <chengkelfan@qq.com>
1 parent 2731c57 commit 14e9ec0

3 files changed

Lines changed: 329 additions & 0 deletions

File tree

ed25519.mbt

Lines changed: 209 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,209 @@
1+
///|
2+
/// Edwards25519 curve parameters as big integers (RFC 8032). `p = 2^255 - 19` is
3+
/// the field prime, `d` the curve coefficient, `l` the group order, `sqrt_m1` a
4+
/// square root of -1 (for point decompression, since `p ≡ 5 (mod 8)`), and
5+
/// `(bx, by)` the base point. Core's `BigInt` supplies the arithmetic; the values
6+
/// were computed from the definition, not transcribed.
7+
let ed_p : BigInt = BigInt::from_string(
8+
"7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFED",
9+
radix=16,
10+
)
11+
12+
///|
13+
let ed_d : BigInt = BigInt::from_string(
14+
"52036CEE2B6FFE738CC740797779E89800700A4D4141D8AB75EB4DCA135978A3",
15+
radix=16,
16+
)
17+
18+
///|
19+
let ed_l : BigInt = BigInt::from_string(
20+
"1000000000000000000000000000000014DEF9DEA2F79CD65812631A5CF5D3ED",
21+
radix=16,
22+
)
23+
24+
///|
25+
let ed_sqrt_m1 : BigInt = BigInt::from_string(
26+
"2B8324804FC1DF0B2B4D00993DFBD7A72F431806AD2FE478C4EE1B274A0EA0B0",
27+
radix=16,
28+
)
29+
30+
///|
31+
let ed_bx : BigInt = BigInt::from_string(
32+
"216936D3CD6E53FEC0A4E231FDD6DC5C692CC7609525A7B2C9562D608F25D51A",
33+
radix=16,
34+
)
35+
36+
///|
37+
let ed_by : BigInt = BigInt::from_string(
38+
"6666666666666666666666666666666666666666666666666666666666666658",
39+
radix=16,
40+
)
41+
42+
///|
43+
/// 2^255, for masking off a compressed point's sign bit.
44+
let ed_2_255 : BigInt = BigInt::from_string(
45+
"8000000000000000000000000000000000000000000000000000000000000000",
46+
radix=16,
47+
)
48+
49+
///|
50+
/// A point on Edwards25519 in affine coordinates. The addition law is complete
51+
/// (identity `(0, 1)`, no special cases), so no infinity flag is needed.
52+
priv struct EdPoint {
53+
x : BigInt
54+
y : BigInt
55+
}
56+
57+
///|
58+
/// Reduce mod the field prime, normalised to `[0, p)`.
59+
fn edmod(a : BigInt) -> BigInt {
60+
let m = a % ed_p
61+
if m < (0 : BigInt) {
62+
m + ed_p
63+
} else {
64+
m
65+
}
66+
}
67+
68+
///|
69+
/// Reduce mod the group order, normalised to `[0, l)`.
70+
fn edmod_l(a : BigInt) -> BigInt {
71+
let m = a % ed_l
72+
if m < (0 : BigInt) {
73+
m + ed_l
74+
} else {
75+
m
76+
}
77+
}
78+
79+
///|
80+
/// Field inverse (Fermat: a^(p-2) mod p).
81+
fn edinv(a : BigInt) -> BigInt {
82+
edmod(a).pow(ed_p - 2, modulus=ed_p)
83+
}
84+
85+
///|
86+
/// Recover the `x` coordinate from `y` on Edwards25519: `x² = (y²-1)/(d·y²+1)`,
87+
/// with the `p ≡ 5 (mod 8)` square root and the even root chosen.
88+
fn ed_xrecover(y : BigInt) -> BigInt {
89+
let yy = edmod(y * y)
90+
let xx = edmod((yy - 1) * edinv(edmod(ed_d * yy + 1)))
91+
let mut x = xx.pow((ed_p + 3) / 8, modulus=ed_p)
92+
if edmod(x * x - xx) != (0 : BigInt) {
93+
x = edmod(x * ed_sqrt_m1)
94+
}
95+
if x % 2 != (0 : BigInt) {
96+
x = ed_p - x
97+
}
98+
x
99+
}
100+
101+
///|
102+
/// Edwards25519 point addition (complete twisted-Edwards law, a = -1).
103+
fn ed_add(pp : EdPoint, qq : EdPoint) -> EdPoint {
104+
let x1 = pp.x
105+
let y1 = pp.y
106+
let x2 = qq.x
107+
let y2 = qq.y
108+
let dxy = edmod(ed_d * x1 * x2 * y1 * y2)
109+
let x3 = edmod((x1 * y2 + x2 * y1) * edinv(edmod(1 + dxy)))
110+
let y3 = edmod((y1 * y2 + x1 * x2) * edinv(edmod(1 - dxy)))
111+
{ x: x3, y: y3 }
112+
}
113+
114+
///|
115+
/// Scalar multiplication `e · pt` by double-and-add.
116+
fn ed_mul(e : BigInt, pt : EdPoint) -> EdPoint {
117+
let mut result : EdPoint = { x: 0, y: 1 }
118+
let mut addend = pt
119+
let mut k = e
120+
while k > (0 : BigInt) {
121+
if k % 2 == (1 : BigInt) {
122+
result = ed_add(result, addend)
123+
}
124+
addend = ed_add(addend, addend)
125+
k = k / 2
126+
}
127+
result
128+
}
129+
130+
///|
131+
/// Interpret `b` as a little-endian unsigned integer (Ed25519's byte order).
132+
fn ed_le_int(b : BytesView) -> BigInt {
133+
let buf = Buffer()
134+
for i = b.length() - 1; i >= 0; i = i - 1 {
135+
buf.write_byte(b[i])
136+
}
137+
BigInt::from_octets(buf.to_bytes()[:])
138+
}
139+
140+
///|
141+
/// Decompress a 32-byte little-endian Edwards25519 point: `y` is the low 255
142+
/// bits, and the top bit selects the sign (parity) of `x`.
143+
fn ed_decode_point(s : BytesView) -> EdPoint {
144+
let y = ed_le_int(s) % ed_2_255
145+
let mut x = ed_xrecover(y)
146+
let sign = (s[31].to_int() >> 7) & 1
147+
let parity = if x % 2 == (1 : BigInt) { 1 } else { 0 }
148+
if parity != sign {
149+
x = ed_p - x
150+
}
151+
{ x, y }
152+
}
153+
154+
///|
155+
/// Ed25519 signature verification (RFC 8032 §5.1.7). `sig` is the 64-byte
156+
/// `R || S`, `pub_key` the 32-byte compressed public point. Checks `[S]B = R +
157+
/// [k]A` with `k = SHA-512(R || A || M) mod l`.
158+
pub fn ed25519_verify(pub_key : Bytes, msg : Bytes, sig : Bytes) -> Bool {
159+
if pub_key.length() != 32 || sig.length() != 64 {
160+
return false
161+
}
162+
let a_pt = ed_decode_point(pub_key[:])
163+
let r_pt = ed_decode_point(sig[0:32])
164+
let s = ed_le_int(sig[32:64])
165+
if s >= ed_l {
166+
return false
167+
}
168+
let hbuf = Buffer()
169+
hbuf.write_bytes(sig[0:32])
170+
hbuf.write_bytes(pub_key[:])
171+
hbuf.write_bytes(msg[:])
172+
let k = edmod_l(ed_le_int(sha512(hbuf.to_bytes())[:]))
173+
let lhs = ed_mul(s, { x: ed_bx, y: ed_by })
174+
let rhs = ed_add(r_pt, ed_mul(k, a_pt))
175+
lhs.x == rhs.x && lhs.y == rhs.y
176+
}
177+
178+
///|
179+
/// An Ed25519 (EdDSA) public key: the 32-byte compressed point. The verification
180+
/// key for the JWT `EdDSA` algorithm (RFC 8037).
181+
pub(all) struct Ed25519PublicKey {
182+
key : Bytes
183+
}
184+
185+
///|
186+
/// Build an Ed25519 public key from its 32-byte hex encoding.
187+
pub fn Ed25519PublicKey::from_hex(hex : String) -> Ed25519PublicKey {
188+
let buf = Buffer()
189+
for i = 0; i < hex.length(); i = i + 2 {
190+
let hi = hex_nibble(hex[i].to_int())
191+
let lo = hex_nibble(hex[i + 1].to_int())
192+
buf.write_byte(((hi << 4) | lo).to_byte())
193+
}
194+
{ key: buf.to_bytes() }
195+
}
196+
197+
///|
198+
/// A single hex digit's value, from its character code.
199+
fn hex_nibble(v : Int) -> Int {
200+
if v >= 0x30 && v <= 0x39 {
201+
v - 0x30
202+
} else if v >= 0x61 && v <= 0x66 {
203+
v - 0x61 + 10
204+
} else if v >= 0x41 && v <= 0x46 {
205+
v - 0x41 + 10
206+
} else {
207+
0
208+
}
209+
}

ed25519_wbtest.mbt

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
///|
2+
/// Decode a hex string to bytes.
3+
fn hexb(h : String) -> Bytes {
4+
let buf = Buffer()
5+
for i = 0; i < h.length(); i = i + 2 {
6+
let hi = hex_nibble(h[i].to_int())
7+
let lo = hex_nibble(h[i + 1].to_int())
8+
buf.write_byte(((hi << 4) | lo).to_byte())
9+
}
10+
buf.to_bytes()
11+
}
12+
13+
///|
14+
test "Ed25519 curve constants are self-consistent" {
15+
// p = 2^255 - 19, and d = -121665 / 121666 mod p — cross-checked independently
16+
// of their hardcoded hex, so a transcription typo cannot slip through.
17+
assert_true(ed_p == ed_2_255 - 19)
18+
assert_true(ed_d == edmod((ed_p - 121665) * edinv(121666)))
19+
}
20+
21+
///|
22+
test "Ed25519 verifies the RFC 8032 test vectors" {
23+
// TEST 1: empty message.
24+
assert_true(
25+
ed25519_verify(
26+
hexb("d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a"),
27+
b"",
28+
hexb(
29+
"e5564300c360ac729086e2cc806e828a84877f1eb8e5d974d873e065224901555fb8821590a33bacc61e39701cf9b46bd25bf5f0595bbe24655141438e7a100b",
30+
),
31+
),
32+
)
33+
// TEST 3: message 0xaf82.
34+
assert_true(
35+
ed25519_verify(
36+
hexb("fc51cd8e6218a1a38da47ed00230f0580816ed13ba3303ac5deb911548908025"),
37+
b"\xaf\x82",
38+
hexb(
39+
"6291d657deec24024827e69c3abe01a30ce548a284743a445e3680d7db5ac3ac18ff9b538d16f290ae67f760984dc6594a7c15e9716ed28dc027beceea1ec40a",
40+
),
41+
),
42+
)
43+
// Tamper the message -> reject.
44+
assert_false(
45+
ed25519_verify(
46+
hexb("d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a"),
47+
b"x",
48+
hexb(
49+
"e5564300c360ac729086e2cc806e828a84877f1eb8e5d974d873e065224901555fb8821590a33bacc61e39701cf9b46bd25bf5f0595bbe24655141438e7a100b",
50+
),
51+
),
52+
)
53+
}
54+
55+
///|
56+
test "jwt_verify_eddsa accepts an Ed25519 token and refuses an alg downgrade" {
57+
let key = Ed25519PublicKey::from_hex(
58+
"d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a",
59+
)
60+
// A real EdDSA JWT signed with the matching Ed25519 key (payload {"sub":"42"}).
61+
let token = "eyJhbGciOiJFZERTQSIsInR5cCI6IkpXVCJ9.eyJzdWIiOiI0MiJ9.EitmEz7OHUvbI6btyx4HMZTnXX3mAHUohPlaegodtCruZXtWibfaE8DZTEI8Txubf5SgAiM6JxBSkmY1evpsBw"
62+
let claims = jwt_verify_eddsa(token, key, 0) catch {
63+
_ => fail("jwt_verify_eddsa unexpectedly raised")
64+
}
65+
assert_eq(claims.get("sub"), Some("42".to_json()))
66+
// An HS256 token is refused by the EdDSA verifier.
67+
let hs = jwt_sign(Map([("sub", "1".to_json())]), "secret")
68+
let refused = try {
69+
jwt_verify_eddsa(hs, key, 0) |> ignore
70+
false
71+
} catch {
72+
UnsupportedAlg(_) => true
73+
_ => false
74+
}
75+
assert_true(refused)
76+
}

jwt.mbt

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -314,6 +314,50 @@ pub fn jwt_sign_es256(
314314
header_seg + "." + payload_seg + "." + base64url_encode(sig)
315315
}
316316

317+
///|
318+
/// Read the header segment's `alg`, raising `UnsupportedAlg` for anything but
319+
/// `EdDSA` — the EdDSA counterpart of `check_alg`, refusing an `alg` downgrade.
320+
fn check_alg_eddsa(header_seg : String) -> Unit raise JwtError {
321+
let text = @utf8.decode_lossy(base64url_decode(header_seg)[:])
322+
let json = @json.parse(text) catch {
323+
_ => raise MalformedToken("header is not valid JSON")
324+
}
325+
match json {
326+
Object(m) =>
327+
match m.get("alg") {
328+
Some(String("EdDSA")) => ()
329+
Some(String(other)) => raise UnsupportedAlg(other)
330+
_ => raise UnsupportedAlg("missing alg")
331+
}
332+
_ => raise MalformedToken("header is not a JSON object")
333+
}
334+
}
335+
336+
///|
337+
/// Verify a compact EdDSA (Ed25519) JWT and return its claims (RFC 8037). Checks
338+
/// three segments; the header `alg` is `EdDSA`; the Ed25519 signature verifies
339+
/// against `key`; and the `exp` / `nbf` time claims. Raises the matching
340+
/// `JwtError`; a tampered payload or signature fails at `BadSignature`.
341+
pub fn jwt_verify_eddsa(
342+
token : String,
343+
key : Ed25519PublicKey,
344+
now_secs : Int64,
345+
) -> Map[String, Json] raise JwtError {
346+
let parts = split_char(token, '.')
347+
if parts.length() != 3 {
348+
raise MalformedToken("expected three segments")
349+
}
350+
let header_seg = parts[0]
351+
let payload_seg = parts[1]
352+
let sig_seg = parts[2]
353+
check_alg_eddsa(header_seg)
354+
let sig = base64url_decode(sig_seg)
355+
if !ed25519_verify(key.key, jwt_signing_input(header_seg, payload_seg), sig) {
356+
raise BadSignature
357+
}
358+
parse_and_check_claims(payload_seg, now_secs)
359+
}
360+
317361
///|
318362
/// Read a `NumericDate` claim as seconds. RFC 7519 says it's a JSON number, but
319363
/// tokens in the wild sometimes carry it as a numeric string, so both are

0 commit comments

Comments
 (0)