sml-aead

A single, algorithm-agnostic AEAD (authenticated encryption with associated data) facade in pure Standard ML, over the cipher primitives that already exist in the sjqtentacles ecosystem:

• ChaCha20-Poly1305 (RFC 8439) — via vendored sml-chacha20
• AES-128-GCM / AES-256-GCM (NIST GCM) — via vendored sml-aes

Instead of programming against three different structures, callers (and downstream protocol work such as a future sml-tls/sml-ssh) target one alg-keyed seal/open' interface. This repo implements no new cryptography — it is a thin dispatch layer plus a consolidated home for the canonical RFC 8439 / NIST GCM test vectors. The standalone Poly1305 one-time MAC is also re-exported.

No FFI, no external dependencies, and deterministic — byte-identical under both MLton and Poly/ML.

Status

• 50 assertions, green on MLton and Poly/ML (byte-identical output).
• Vendors sml-chacha20 + sml-aes (Layout B), so the repo builds standalone.
• Validated against the official vectors:
  • RFC 8439 §2.5.2 — Poly1305 one-time MAC.
  • RFC 8439 §2.8.2 — the canonical ChaCha20-Poly1305 AEAD "sunscreen" example (ciphertext and tag, byte-exact).
  • AES-GCM — McGrew & Viega Appendix B test cases 4 (AES-128) and 16 (AES-256), the de-facto NIST GCM known-answer vectors (ciphertext and tag, byte-exact).
• Tamper detection: a flipped tag byte, ciphertext byte, wrong AAD, or wrong nonce all make open' return NONE.

Building this facade surfaced and fixed a GHASH bug in sml-aes (its AES-GCM produced correct ciphertext but a non-interoperable authentication tag); the upstream fix plus NIST known-answer vectors landed in sml-aes first, and the byte-identical fixed tree is vendored here.

Install

With smlpkg:

smlpkg add github.com/sjqtentacles/sml-aead
smlpkg sync

Include the MLB from your own (it pulls in the vendored sml-chacha20 + sml-aes):

local
  $(SML_LIB)/basis/basis.mlb
  lib/github.com/sjqtentacles/sml-aead/... (via smlpkg)
in
  ...
end

This brings structure Aead (and the vendored primitive structures) into scope.

Quick start

(* keys, nonces, aad, plaintext and ciphertext are all raw byte strings:
   one char per byte, 0-255 *)

(* 32-byte key, 12-byte nonce for ChaCha20-Poly1305 *)
val sealed = Aead.seal Aead.ChaCha20Poly1305
  { key = key32, nonce = nonce12, aad = "header", plaintext = "secret" }
(* sealed = ciphertext || 16-byte tag *)

val recovered = Aead.open' Aead.ChaCha20Poly1305
  { key = key32, nonce = nonce12, aad = "header", ciphertext = sealed }
(* SOME "secret", or NONE if anything was tampered with *)

(* AES-256-GCM: 32-byte key, 12-byte IV *)
val sealed' = Aead.seal Aead.AesGcm256
  { key = key32, nonce = iv12, aad = "", plaintext = "secret" }

(* standalone Poly1305 one-time MAC *)
val tagHex = Aead.Poly1305.macHex oneTimeKey32 "message"

Demo

make example runs examples/demo.sml, sealing one message under all three algorithms with fixed keys/nonces:

sml-aead demo
=============
plaintext : attack at dawn
aad       : hdr:v1

ChaCha20-Poly1305:
  sealed  : 3fbe31666572e6086fe65702aec51e96d0c044d64b4e8c7b5adf1ab69cdf
  opened  : true
AES-128-GCM:
  sealed  : a55a77ce6c24968e63fd3994b0499fdab3ff07e908165aa3a63689380b45
  opened  : true
AES-256-GCM:
  sealed  : 1c8aec772aa21ad2be556c7c7817dd8320f4fdcc354535b6df9615f13af7
  opened  : true

Poly1305 MAC of "attack at dawn" under a fixed key:
  daf8f71535db4152c9b148bda19abcfa

API

datatype alg = ChaCha20Poly1305   (* 256-bit key, 96-bit nonce *)
             | AesGcm128          (* 128-bit key, 96-bit nonce *)
             | AesGcm256          (* 256-bit key, 96-bit nonce *)

exception Aead of string          (* wrong key/nonce length *)

val tagLen   : int                (* = 16 *)
val keyLen   : alg -> int
val nonceLen : alg -> int

val seal  : alg -> {key:string, nonce:string, aad:string, plaintext:string}
                -> string         (* ciphertext || tag *)
val open' : alg -> {key:string, nonce:string, aad:string, ciphertext:string}
                -> string option  (* SOME plaintext, or NONE if auth fails *)

structure Poly1305 :
  sig
    val mac    : string -> string -> string   (* raw 16-byte tag *)
    val macHex : string -> string -> string   (* 32-char hex tag *)
  end

Function	Behavior
keyLen alg / nonceLen alg	required key / nonce length in bytes (nonceLen is always 12)
seal alg {key, nonce, aad, plaintext}	encrypt + authenticate; returns ciphertext with the 16-byte tag appended; raises Aead on a wrong key/nonce length
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
Poly1305.mac key msg	RFC 8439 §2.5 one-time authenticator with a 32-byte key

Conventions

• Bytes as string. Keys, nonces, AAD, plaintext and ciphertext are raw byte strings (one char per byte, 0–255), matching the rest of the sjqtentacles crypto/codec family. They are never hex.
• Tag appended. seal returns ciphertext || tag (16-byte tag), exactly as the underlying RFC 8439 / NIST GCM constructions specify, and open' expects that same layout.
• Nonce reuse is catastrophic. As with any AEAD, never reuse a (key, nonce) pair; the caller is responsible for unique nonces.
• No new crypto. The ciphers live in sml-chacha20 / sml-aes; this repo only unifies and vector-tests them.

Build & test

make test        # MLton
make test-poly   # Poly/ML
make all-tests   # both
make example     # build + run examples/demo.sml
make clean

License

MIT — see LICENSE.