Skip to content

Add NIST SP 800-38D GCM specification with KATs#389

Draft
sgmenda wants to merge 8 commits into
awslabs:mainfrom
sgmenda:gcm-spec
Draft

Add NIST SP 800-38D GCM specification with KATs#389
sgmenda wants to merge 8 commits into
awslabs:mainfrom
sgmenda:gcm-spec

Conversation

@sgmenda
Copy link
Copy Markdown
Contributor

@sgmenda sgmenda commented Apr 8, 2026

Depends on #370 (AES specs), #381 (word_pmul), and #382 (ghash).

To simplify the future merge, we only copied over the specific files we need: common/misc.ml from #381 and common/ghash.ml from #382. This contains merge conflicts to these two files.

This PR adds a high-level AES-GCM specification, following NIST SP 800-38D. It will be the correctness target for forthcoming AES-GCM assembly proofs.

New files

common/gcm.ml — GCM definitions and KATs:

  • inc32 — increment rightmost 32 bits of a 128-bit block (Section 6.2)
  • gctr — counter-mode encryption (Algorithm 3)
  • gf128_mul — GF(2^128) multiplication (Algorithm 1)
  • ghash — GHASH universal hash (Algorithm 2)
  • gcm_ae — authenticated encryption (Algorithm 4)
  • gcm_ad — authenticated decryption (Algorithm 5)

Simplified to 96-bit IVs, full 128-bit blocks, 128-bit tags, and pre-expanded key schedules.

KATs validated against test vectors from the GCM revised spec (McGrew & Viega, Appendix B):

Test case Plaintext AAD What it exercises
TC1 empty empty Bare GHASH + tag
TC2 1 zero block empty GCTR with plaintext
TC3 4 blocks empty Full pipeline, non-trivial key/IV

TC1 is proved end-to-end (prove()). TC2 and TC3 are deconstructed KATs where each step (AES, GCTR, GHASH, tag) is proved as an individual theorem.

sgmenda added 6 commits March 12, 2026 23:13
@sgmenda
Add FIPS 197 AES cipher specification with KATs
84ada38 
Add HOL Light definitions for AES-128 and AES-256 following NIST FIPS 197
exactly, independent from the hardware-oriented model in common/aes.ml.
Uses NIST ordering (SubBytes before ShiftRows) throughout.

New files:
- common/fips197.ml: key expansion, cipher steps, full cipher, and KATs
- {arm,x86}/proofs/fips197.ml: loaders for standard build-proof.sh validation

Definitions: aes128_kexp_round, aes256_kexp_round, aes256_kexp_last,
fips197_sub_bytes, fips197_shift_rows, fips197_mix_columns,
fips197_add_round_key, fips197_round, fips197_final_round,
aes128_cipher, aes256_cipher.

KATs: FIPS 197 Appendices A.1, A.3, B; NIST AES_Core256; AESAVS GFSbox.

To validate: cd x86 && make proofs/fips197.correct
         or: cd arm && make proofs/fips197.correct
@sgmenda
Merge branch 'main' into fips197
41d016f
@sgmenda
whitespace
a8a5585
@sgmenda
Add S-box/FFmul precomputation tables and fast AES conversions
a233309 
Precompute all 768 lookup table entries (256 each for S-box, FFmul02,
FFmul03) as proven theorems at load time (~48s). This eliminates the
word_subword bottleneck on 2048-bit constants, reducing AES-128
evaluation from ~40s to ~7s per call.

Add FIPS197_ENCRYPT_FAST_CONV and supporting fast conversion chain.
Uncomment all KATs (key expansion, SubBytes, ShiftRows, MixColumns,
AddRoundKey, full AES-128 and AES-256 cipher) using fast conversions.
Remove fips197_add_round_key (just word_xor, unused).
@sgmenda
Pick common/misc.ml from awslabs#381 (word_pmul)
6154292 
Cherry-pick common/misc.ml from s2n-bignum#381 to get word_pmul and
WORD_PMUL_CONV, needed by ghash_reduce in common/ghash.ml.

This file should be identical to the version in awslabs#381 and will be a
no-op when awslabs#381 merges.
@sgmenda
Pick common/ghash.ml from awslabs#382 (GHASH polynomial reduction)
1ba8858 
Cherry-pick common/ghash.ml from s2n-bignum#382 to get ghash_reduce1,
ghash_reduce, and their correctness proofs. Needed by gf128_mul in
common/gcm.ml.

This file should be identical to the version in awslabs#382 and will be a
no-op when awslabs#382 merges.
@sgmenda sgmenda self-assigned this Apr 8, 2026
@sgmenda sgmenda marked this pull request as draft April 8, 2026 19:51
@sgmenda
Add GCM spec (SP 800-38D) with KATs
9aa96c4 
common/gcm.ml: High-level GCM spec close to NIST SP 800-38D:
- gf128_mul (via word_pmul + ghash_reduce), ghash, inc32, gctr,
  gcm_ae (Algorithm 4), gcm_ad (Algorithm 5).
- Simplified to 96-bit IV, full 128-bit blocks, 128-bit tag.
- KATs: inc32, GCTR, gf128_mul, GHASH, plus GCM-AE/AD for TC1-TC3
  from the GCM revised spec (McGrew & Viega, Appendix B).
sgmenda
sgmenda commented Apr 20, 2026
View reviewed changes
Comment thread common/gcm.ml
Comment on lines +197 to +272
(* ========================================================================= *)
(* GHASH: NIST SP 800-38D Algorithm 2. *)
(* *)
(* GHASH(H, X_1 || ... || X_m) iterates gf128_mul: *)
(* Y_0 = 0, Y_i = gf128_mul(Y_{i-1} XOR X_i, H). *)
(* Takes an initial accumulator Y (normally word 0) for generality. *)
(* ========================================================================= *)

let ghash = define
`ghash (H:128 word) (Y:128 word) ([] : (128 word) list) = Y /\
ghash H Y (CONS x rest) = ghash H (gf128_mul (word_xor Y x) H) rest`;;

(* Conversion for evaluating ghash on concrete values *)
let GHASH_STEP_CONV =
ONCE_REWRITE_CONV [ghash] THENC
DEPTH_CONV WORD_RED_CONV THENC
ONCE_DEPTH_CONV GF128_MUL_CONV;;

let rec GHASH_CONV tm =
(GHASH_STEP_CONV THENC TRY_CONV GHASH_CONV) tm;;

prove(`ghash (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E) (word 0)
[word 0 : 128 word] = word 0`,
CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);;

prove(`ghash (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E) (word 0)
[word 0x0388DACE60B6A392F328C2B971B2FE78 : 128 word] =
word 0x5E2EC746917062882C85B0685353DEB7`,
CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);;

prove(`ghash (word 0xB83B533708BF535D0AA6E52980D53B78) (word 0)
[ word 0x42831EC2217774244B7221B784D0D49C
; word 0xE3AA212F2C02A4E035C17E2329ACA12E : 128 word] =
word 0xB714C9048389AFD9F9BC5C1D4378E052`,
CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);;

(* ========================================================================= *)
(* GCM-AE: NIST SP 800-38D Algorithm 4 (authenticated encryption). *)
(* *)
(* Simplified to 96-bit IV, full 128-bit blocks, and 128-bit tag. *)
(* Key schedule is pre-expanded. Returns (ciphertext, tag). *)
(* ========================================================================= *)

let gcm_ae = new_definition
`gcm_ae (ks:(128 word) list) (iv:96 word)
(P:(128 word) list) (A:(128 word) list) =
let H = aes128_cipher (word 0) ks in
let J0 : 128 word = word_join iv (word 1 : 32 word) in
let C = gctr ks (inc32 J0) P in
let len_block : 128 word =
word_join (word (128 * LENGTH A) : 64 word)
(word (128 * LENGTH C) : 64 word) in
let S = ghash H (word 0) (APPEND A (APPEND C [len_block])) in
let tag = word_xor S (aes128_cipher J0 ks) in
(C, tag)`;;

(* ========================================================================= *)
(* GCM-AD: NIST SP 800-38D Algorithm 5 (authenticated decryption). *)
(* *)
(* Returns SOME plaintext if tag verifies, NONE otherwise. *)
(* ========================================================================= *)

let gcm_ad = new_definition
`gcm_ad (ks:(128 word) list) (iv:96 word)
(C:(128 word) list) (A:(128 word) list) (tag:128 word) =
let H = aes128_cipher (word 0) ks in
let J0 : 128 word = word_join iv (word 1 : 32 word) in
let P = gctr ks (inc32 J0) C in
let len_block : 128 word =
word_join (word (128 * LENGTH A) : 64 word)
(word (128 * LENGTH C) : 64 word) in
let S = ghash H (word 0) (APPEND A (APPEND C [len_block])) in
let tag' = word_xor S (aes128_cipher J0 ks) in
if tag' = tag then SOME P else NONE`;;


Copy link
Copy Markdown
Contributor Author

@sgmenda sgmenda Apr 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@nebeid the the current KATs

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@sgmenda sgmenda

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@sgmenda