Skip to content

Commit dc9d079

Browse files
sjqtentaclescursoragent
sjqtentacles
and
cursoragent
committed
sml-aead: unified AEAD facade over ChaCha20-Poly1305 and AES-GCM
A thin, algorithm-agnostic AEAD interface (seal/open' keyed by alg) over the existing vendored primitives -- ChaCha20-Poly1305 (sml-chacha20, RFC 8439) and AES-128/256-GCM (sml-aes, NIST GCM) -- plus a re-exported standalone Poly1305 one-time MAC. No new cryptography; the value is one interface and a consolidated byte-exact vector vault. Validated against RFC 8439 (Poly1305 2.5.2, ChaCha20-Poly1305 2.8.2) and the McGrew/NIST Appendix B GCM cases 4 and 16, with tamper-detection and key/nonce length validation. 50 assertions, byte-identical on MLton and Poly/ML. Layout B, CI Variant A. Co-authored-by: Cursor <cursoragent@cursor.com>
0 parents  commit dc9d079

24 files changed

Lines changed: 1534 additions & 0 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
name: CI
2+
on:
3+
push:
4+
branches: [ main ]
5+
pull_request:
6+
branches: [ main ]
7+
jobs:
8+
mlton:
9+
name: MLton (build + test)
10+
runs-on: ubuntu-latest
11+
steps:
12+
- uses: actions/checkout@v4
13+
- name: Install MLton
14+
run: sudo apt-get update && sudo apt-get install -y mlton
15+
- name: Run tests
16+
run: make test
17+
polyml:
18+
name: Poly/ML (test)
19+
runs-on: ubuntu-latest
20+
steps:
21+
- uses: actions/checkout@v4
22+
- name: Install Poly/ML
23+
run: sudo apt-get update && sudo apt-get install -y polyml libpolyml-dev
24+
- name: Run tests
25+
run: make test-poly

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# MLton build artifacts
2+
/bin/
3+
4+
# editor/OS noise
5+
.DS_Store

‎LICENSE‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MIT License
2+
3+
Copyright (c) 2026 sml-aead contributors
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
The above copyright notice and this permission notice shall be included in all
13+
copies or substantial portions of the Software.
14+
15+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+
SOFTWARE.

‎Makefile‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# sml-aead build
2+
#
3+
# make build the test binary with MLton (default)
4+
# make test build + run tests under MLton
5+
# make test-poly run tests under Poly/ML (use-and-run; no link step)
6+
# make all-tests run the suite under both compilers
7+
# make example build + run the demo
8+
# make clean remove build artifacts
9+
#
10+
# Layout B (dependent): own sources live in src/; sml-chacha20 (ChaCha20 /
11+
# Poly1305 / ChaCha20Poly1305) and sml-aes (AesBlock / AesGcm) are vendored
12+
# under lib/ and loaded first, then the Aead facade.
13+
14+
MLTON ?= mlton
15+
POLY ?= poly
16+
BIN := bin
17+
CHACHADIR := lib/github.com/sjqtentacles/sml-chacha20
18+
AESDIR := lib/github.com/sjqtentacles/sml-aes
19+
TEST_MLB := test/test.mlb
20+
SRCS := $(wildcard $(CHACHADIR)/* $(AESDIR)/* src/* test/*.sml) $(TEST_MLB)
21+
22+
.PHONY: all test poly test-poly all-tests example clean
23+
24+
all: $(BIN)/test-mlton
25+
26+
example: $(BIN)/demo
27+
./$(BIN)/demo
28+
29+
$(BIN)/demo: $(SRCS) examples/demo.sml examples/sources.mlb | $(BIN)
30+
$(MLTON) -output $@ examples/sources.mlb
31+
32+
$(BIN)/test-mlton: $(SRCS) | $(BIN)
33+
$(MLTON) -output $@ $(TEST_MLB)
34+
35+
test: $(BIN)/test-mlton
36+
$(BIN)/test-mlton
37+
38+
# Poly/ML has no native .mlb support; the suite runs at top level and exits on
39+
# its own. Load the vendored primitive sources (in dependency order), then the
40+
# aead facade, then the test driver.
41+
poly test-poly:
42+
printf 'use "$(CHACHADIR)/chacha20.sig";\nuse "$(CHACHADIR)/chacha20.sml";\nuse "$(AESDIR)/aes.sig";\nuse "$(AESDIR)/aes.sml";\nuse "src/aead.sig";\nuse "src/aead.sml";\nuse "test/harness.sml";\nuse "test/support.sml";\nuse "test/test_vectors.sml";\nuse "test/test_facade.sml";\nuse "test/entry.sml";\nuse "test/main.sml";\n' | $(POLY) -q --error-exit
43+
44+
all-tests: test test-poly
45+
46+
$(BIN):
47+
mkdir -p $(BIN)
48+
49+
clean:
50+
rm -f $(BIN)/test-mlton $(BIN)/demo

‎README.md‎

Lines changed: 167 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
# sml-aead
2+
3+
A single, algorithm-agnostic **AEAD** (authenticated encryption with associated
4+
data) facade in pure Standard ML, over the cipher primitives that already exist
5+
in the sjqtentacles ecosystem:
6+
7+
- **ChaCha20-Poly1305** ([RFC 8439](https://www.rfc-editor.org/rfc/rfc8439)) — via vendored [`sml-chacha20`](https://github.com/sjqtentacles/sml-chacha20)
8+
- **AES-128-GCM / AES-256-GCM** (NIST GCM) — via vendored [`sml-aes`](https://github.com/sjqtentacles/sml-aes)
9+
10+
Instead of programming against three different structures, callers (and
11+
downstream protocol work such as a future `sml-tls`/`sml-ssh`) target one
12+
`alg`-keyed `seal`/`open'` interface. This repo **implements no new
13+
cryptography** — it is a thin dispatch layer plus a consolidated home for the
14+
canonical RFC 8439 / NIST GCM test vectors. The standalone Poly1305 one-time
15+
MAC is also re-exported.
16+
17+
No FFI, no external dependencies, and **deterministic** — byte-identical under
18+
both [MLton](http://mlton.org/) and [Poly/ML](https://www.polyml.org/).
19+
20+
## Status
21+
22+
- 50 assertions, green on MLton and Poly/ML (byte-identical output).
23+
- Vendors `sml-chacha20` + `sml-aes` (Layout B), so the repo builds standalone.
24+
- Validated against the **official vectors**:
25+
- **RFC 8439 §2.5.2** — Poly1305 one-time MAC.
26+
- **RFC 8439 §2.8.2** — the canonical ChaCha20-Poly1305 AEAD "sunscreen"
27+
example (ciphertext **and** tag, byte-exact).
28+
- **AES-GCM** — McGrew & Viega Appendix B test cases 4 (AES-128) and 16
29+
(AES-256), the de-facto NIST GCM known-answer vectors (ciphertext **and**
30+
tag, byte-exact).
31+
- Tamper detection: a flipped tag byte, ciphertext byte, wrong AAD, or wrong
32+
nonce all make `open'` return `NONE`.
33+
34+
> Building this facade surfaced and fixed a GHASH bug in `sml-aes` (its AES-GCM
35+
> produced correct ciphertext but a non-interoperable authentication tag); the
36+
> upstream fix plus NIST known-answer vectors landed in `sml-aes` first, and the
37+
> byte-identical fixed tree is vendored here.
38+
39+
## Install
40+
41+
With [`smlpkg`](https://github.com/diku-dk/smlpkg):
42+
43+
```
44+
smlpkg add github.com/sjqtentacles/sml-aead
45+
smlpkg sync
46+
```
47+
48+
Include the MLB from your own (it pulls in the vendored `sml-chacha20` +
49+
`sml-aes`):
50+
51+
```
52+
local
53+
$(SML_LIB)/basis/basis.mlb
54+
lib/github.com/sjqtentacles/sml-aead/... (via smlpkg)
55+
in
56+
...
57+
end
58+
```
59+
60+
This brings `structure Aead` (and the vendored primitive structures) into scope.
61+
62+
## Quick start
63+
64+
```sml
65+
(* keys, nonces, aad, plaintext and ciphertext are all raw byte strings:
66+
one char per byte, 0-255 *)
67+
68+
(* 32-byte key, 12-byte nonce for ChaCha20-Poly1305 *)
69+
val sealed = Aead.seal Aead.ChaCha20Poly1305
70+
{ key = key32, nonce = nonce12, aad = "header", plaintext = "secret" }
71+
(* sealed = ciphertext || 16-byte tag *)
72+
73+
val recovered = Aead.open' Aead.ChaCha20Poly1305
74+
{ key = key32, nonce = nonce12, aad = "header", ciphertext = sealed }
75+
(* SOME "secret", or NONE if anything was tampered with *)
76+
77+
(* AES-256-GCM: 32-byte key, 12-byte IV *)
78+
val sealed' = Aead.seal Aead.AesGcm256
79+
{ key = key32, nonce = iv12, aad = "", plaintext = "secret" }
80+
81+
(* standalone Poly1305 one-time MAC *)
82+
val tagHex = Aead.Poly1305.macHex oneTimeKey32 "message"
83+
```
84+
85+
## Demo
86+
87+
`make example` runs [`examples/demo.sml`](examples/demo.sml), sealing one
88+
message under all three algorithms with fixed keys/nonces:
89+
90+
```
91+
sml-aead demo
92+
=============
93+
plaintext : attack at dawn
94+
aad : hdr:v1
95+
96+
ChaCha20-Poly1305:
97+
sealed : 3fbe31666572e6086fe65702aec51e96d0c044d64b4e8c7b5adf1ab69cdf
98+
opened : true
99+
AES-128-GCM:
100+
sealed : a55a77ce6c24968e63fd3994b0499fdab3ff07e908165aa3a63689380b45
101+
opened : true
102+
AES-256-GCM:
103+
sealed : 1c8aec772aa21ad2be556c7c7817dd8320f4fdcc354535b6df9615f13af7
104+
opened : true
105+
106+
Poly1305 MAC of "attack at dawn" under a fixed key:
107+
daf8f71535db4152c9b148bda19abcfa
108+
```
109+
110+
## API
111+
112+
```sml
113+
datatype alg = ChaCha20Poly1305 (* 256-bit key, 96-bit nonce *)
114+
| AesGcm128 (* 128-bit key, 96-bit nonce *)
115+
| AesGcm256 (* 256-bit key, 96-bit nonce *)
116+
117+
exception Aead of string (* wrong key/nonce length *)
118+
119+
val tagLen : int (* = 16 *)
120+
val keyLen : alg -> int
121+
val nonceLen : alg -> int
122+
123+
val seal : alg -> {key:string, nonce:string, aad:string, plaintext:string}
124+
-> string (* ciphertext || tag *)
125+
val open' : alg -> {key:string, nonce:string, aad:string, ciphertext:string}
126+
-> string option (* SOME plaintext, or NONE if auth fails *)
127+
128+
structure Poly1305 :
129+
sig
130+
val mac : string -> string -> string (* raw 16-byte tag *)
131+
val macHex : string -> string -> string (* 32-char hex tag *)
132+
end
133+
```
134+
135+
| Function | Behavior |
136+
| --- | --- |
137+
| `keyLen alg` / `nonceLen alg` | required key / nonce length in bytes (`nonceLen` is always 12) |
138+
| `seal alg {key, nonce, aad, plaintext}` | encrypt + authenticate; returns `ciphertext` with the 16-byte tag appended; raises `Aead` on a wrong key/nonce length |
139+
| `open' alg {key, nonce, aad, ciphertext}` | verify the tag in constant time and decrypt; `SOME plaintext` on success, `NONE` if authentication fails or the input is shorter than the tag |
140+
| `Poly1305.mac key msg` | RFC 8439 §2.5 one-time authenticator with a 32-byte `key` |
141+
142+
### Conventions
143+
144+
- **Bytes as `string`.** Keys, nonces, AAD, plaintext and ciphertext are raw
145+
byte strings (one char per byte, 0–255), matching the rest of the
146+
sjqtentacles crypto/codec family. They are never hex.
147+
- **Tag appended.** `seal` returns `ciphertext || tag` (16-byte tag), exactly as
148+
the underlying RFC 8439 / NIST GCM constructions specify, and `open'` expects
149+
that same layout.
150+
- **Nonce reuse is catastrophic.** As with any AEAD, never reuse a
151+
(key, nonce) pair; the caller is responsible for unique nonces.
152+
- **No new crypto.** The ciphers live in `sml-chacha20` / `sml-aes`; this repo
153+
only unifies and vector-tests them.
154+
155+
## Build & test
156+
157+
```
158+
make test # MLton
159+
make test-poly # Poly/ML
160+
make all-tests # both
161+
make example # build + run examples/demo.sml
162+
make clean
163+
```
164+
165+
## License
166+
167+
MIT — see [LICENSE](LICENSE).

‎examples/demo.sml‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
(* sml-aead demo: seal one message under all three AEAD algorithms through the
2+
unified facade, print the ciphertext||tag as hex, and confirm authenticated
3+
decryption round-trips. All inputs are fixed, so the output is fully
4+
deterministic and byte-identical across MLton and Poly/ML. *)
5+
6+
fun line s = print (s ^ "\n")
7+
8+
fun toHex s =
9+
String.concat (List.map (fn c =>
10+
let val v = Char.ord c
11+
fun d x = String.str (String.sub ("0123456789abcdef", x))
12+
in d (v div 16) ^ d (v mod 16) end) (String.explode s))
13+
14+
val () = line "sml-aead demo"
15+
val () = line "============="
16+
17+
val plaintext = "attack at dawn"
18+
val aad = "hdr:v1"
19+
20+
fun keyOf alg = String.implode (List.tabulate (Aead.keyLen alg, fn i => Char.chr (i mod 256)))
21+
fun nonceOf alg = String.implode (List.tabulate (Aead.nonceLen alg, fn i => Char.chr (16 + i)))
22+
23+
fun show (name, alg) =
24+
let
25+
val key = keyOf alg
26+
val nonce = nonceOf alg
27+
val sealed = Aead.seal alg {key=key, nonce=nonce, aad=aad, plaintext=plaintext}
28+
val opened = Aead.open' alg {key=key, nonce=nonce, aad=aad, ciphertext=sealed}
29+
val ok = opened = SOME plaintext
30+
in
31+
line (name ^ ":");
32+
line (" sealed : " ^ toHex sealed);
33+
line (" opened : " ^ Bool.toString ok)
34+
end
35+
36+
val () = line ("plaintext : " ^ plaintext)
37+
val () = line ("aad : " ^ aad)
38+
val () = line ""
39+
val () = List.app show
40+
[ ("ChaCha20-Poly1305", Aead.ChaCha20Poly1305)
41+
, ("AES-128-GCM", Aead.AesGcm128)
42+
, ("AES-256-GCM", Aead.AesGcm256) ]
43+
44+
val () = line ""
45+
val () = line ("Poly1305 MAC of \"" ^ plaintext ^ "\" under a fixed key:")
46+
val () = line (" " ^ Aead.Poly1305.macHex (keyOf Aead.ChaCha20Poly1305) plaintext)

‎examples/sources.mlb‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
$(SML_LIB)/basis/basis.mlb
2+
3+
../src/aead.mlb
4+
5+
demo.sml

‎lib/github.com/sjqtentacles/sml-aes/aes.sig‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
(* aes.sig — AES block cipher (FIPS 197) + modes of operation. *)
2+
3+
signature AES_BLOCK =
4+
sig
5+
type key
6+
val keySize : key -> int
7+
val expand128 : string -> key
8+
val expand192 : string -> key
9+
val expand256 : string -> key
10+
val encrypt : key -> string -> string
11+
val decrypt : key -> string -> string
12+
end
13+
14+
signature AES_MODE =
15+
sig
16+
val encrypt : string -> string -> string -> string
17+
val decrypt : string -> string -> string -> string
18+
end
19+
20+
signature AES_GCM =
21+
sig
22+
val seal : string -> string -> string -> string -> string
23+
val open' : string -> string -> string -> string -> string option
24+
end

0 commit comments

Comments
 (0)