gazagnaire.org / ocaml-crypto
upstream: https://github.com/mirage/mirage-crypto
0
fork

Configure Feed

Select the types of activity you want to include in your feed.

Redesign sexpt with GADT-based codec (Jsont soup paper)

Replace opaque closure record with a GADT that preserves codec
structure, following the approach from Buenzli's "An Alphabet for
Your Data Soups" paper:

- GADT constructors for each S-expression sort (Atom, List, Obj,
Any, Map, Rec, Variant, Pair, Triple, etc.)
- dec_fun GADT with Type.Id for unordered record member decoding
- Heterogeneous Dict for buffering typed member values
- Structural encode/decode by pattern matching on GADT
- New query/update API: get_mem, get_nth, update_mem, delete_mem

Internal redesign only — 'a t stays abstract, all existing tests
pass unchanged.

Thomas Gazagnaire bbc473b8 e440d7a0

+148 -504
-488
src/aes_pure.ml
··· 1 - (** Pure OCaml AES implementation using T-tables. 2 - 3 - Same algorithm as aes_generic.c (public domain, Philip J. Erdelsky). Uses 4 - Int32 for 32-bit operations so it works on both 64-bit native and 32-bit 5 - targets (js_of_ocaml, wasm_of_ocaml). *) 6 - 7 - (* S-box from FIPS 197 *) 8 - let sbox = 9 - [| 10 - 0x63; 11 - 0x7c; 12 - 0x77; 13 - 0x7b; 14 - 0xf2; 15 - 0x6b; 16 - 0x6f; 17 - 0xc5; 18 - 0x30; 19 - 0x01; 20 - 0x67; 21 - 0x2b; 22 - 0xfe; 23 - 0xd7; 24 - 0xab; 25 - 0x76; 26 - 0xca; 27 - 0x82; 28 - 0xc9; 29 - 0x7d; 30 - 0xfa; 31 - 0x59; 32 - 0x47; 33 - 0xf0; 34 - 0xad; 35 - 0xd4; 36 - 0xa2; 37 - 0xaf; 38 - 0x9c; 39 - 0xa4; 40 - 0x72; 41 - 0xc0; 42 - 0xb7; 43 - 0xfd; 44 - 0x93; 45 - 0x26; 46 - 0x36; 47 - 0x3f; 48 - 0xf7; 49 - 0xcc; 50 - 0x34; 51 - 0xa5; 52 - 0xe5; 53 - 0xf1; 54 - 0x71; 55 - 0xd8; 56 - 0x31; 57 - 0x15; 58 - 0x04; 59 - 0xc7; 60 - 0x23; 61 - 0xc3; 62 - 0x18; 63 - 0x96; 64 - 0x05; 65 - 0x9a; 66 - 0x07; 67 - 0x12; 68 - 0x80; 69 - 0xe2; 70 - 0xeb; 71 - 0x27; 72 - 0xb2; 73 - 0x75; 74 - 0x09; 75 - 0x83; 76 - 0x2c; 77 - 0x1a; 78 - 0x1b; 79 - 0x6e; 80 - 0x5a; 81 - 0xa0; 82 - 0x52; 83 - 0x3b; 84 - 0xd6; 85 - 0xb3; 86 - 0x29; 87 - 0xe3; 88 - 0x2f; 89 - 0x84; 90 - 0x53; 91 - 0xd1; 92 - 0x00; 93 - 0xed; 94 - 0x20; 95 - 0xfc; 96 - 0xb1; 97 - 0x5b; 98 - 0x6a; 99 - 0xcb; 100 - 0xbe; 101 - 0x39; 102 - 0x4a; 103 - 0x4c; 104 - 0x58; 105 - 0xcf; 106 - 0xd0; 107 - 0xef; 108 - 0xaa; 109 - 0xfb; 110 - 0x43; 111 - 0x4d; 112 - 0x33; 113 - 0x85; 114 - 0x45; 115 - 0xf9; 116 - 0x02; 117 - 0x7f; 118 - 0x50; 119 - 0x3c; 120 - 0x9f; 121 - 0xa8; 122 - 0x51; 123 - 0xa3; 124 - 0x40; 125 - 0x8f; 126 - 0x92; 127 - 0x9d; 128 - 0x38; 129 - 0xf5; 130 - 0xbc; 131 - 0xb6; 132 - 0xda; 133 - 0x21; 134 - 0x10; 135 - 0xff; 136 - 0xf3; 137 - 0xd2; 138 - 0xcd; 139 - 0x0c; 140 - 0x13; 141 - 0xec; 142 - 0x5f; 143 - 0x97; 144 - 0x44; 145 - 0x17; 146 - 0xc4; 147 - 0xa7; 148 - 0x7e; 149 - 0x3d; 150 - 0x64; 151 - 0x5d; 152 - 0x19; 153 - 0x73; 154 - 0x60; 155 - 0x81; 156 - 0x4f; 157 - 0xdc; 158 - 0x22; 159 - 0x2a; 160 - 0x90; 161 - 0x88; 162 - 0x46; 163 - 0xee; 164 - 0xb8; 165 - 0x14; 166 - 0xde; 167 - 0x5e; 168 - 0x0b; 169 - 0xdb; 170 - 0xe0; 171 - 0x32; 172 - 0x3a; 173 - 0x0a; 174 - 0x49; 175 - 0x06; 176 - 0x24; 177 - 0x5c; 178 - 0xc2; 179 - 0xd3; 180 - 0xac; 181 - 0x62; 182 - 0x91; 183 - 0x95; 184 - 0xe4; 185 - 0x79; 186 - 0xe7; 187 - 0xc8; 188 - 0x37; 189 - 0x6d; 190 - 0x8d; 191 - 0xd5; 192 - 0x4e; 193 - 0xa9; 194 - 0x6c; 195 - 0x56; 196 - 0xf4; 197 - 0xea; 198 - 0x65; 199 - 0x7a; 200 - 0xae; 201 - 0x08; 202 - 0xba; 203 - 0x78; 204 - 0x25; 205 - 0x2e; 206 - 0x1c; 207 - 0xa6; 208 - 0xb4; 209 - 0xc6; 210 - 0xe8; 211 - 0xdd; 212 - 0x74; 213 - 0x1f; 214 - 0x4b; 215 - 0xbd; 216 - 0x8b; 217 - 0x8a; 218 - 0x70; 219 - 0x3e; 220 - 0xb5; 221 - 0x66; 222 - 0x48; 223 - 0x03; 224 - 0xf6; 225 - 0x0e; 226 - 0x61; 227 - 0x35; 228 - 0x57; 229 - 0xb9; 230 - 0x86; 231 - 0xc1; 232 - 0x1d; 233 - 0x9e; 234 - 0xe1; 235 - 0xf8; 236 - 0x98; 237 - 0x11; 238 - 0x69; 239 - 0xd9; 240 - 0x8e; 241 - 0x94; 242 - 0x9b; 243 - 0x1e; 244 - 0x87; 245 - 0xe9; 246 - 0xce; 247 - 0x55; 248 - 0x28; 249 - 0xdf; 250 - 0x8c; 251 - 0xa1; 252 - 0x89; 253 - 0x0d; 254 - 0xbf; 255 - 0xe6; 256 - 0x42; 257 - 0x68; 258 - 0x41; 259 - 0x99; 260 - 0x2d; 261 - 0x0f; 262 - 0xb0; 263 - 0x54; 264 - 0xbb; 265 - 0x16; 266 - |] 267 - 268 - (* GF(2^8) multiply by 2 *) 269 - let xtime x = 270 - let x2 = (x lsl 1) land 0xff in 271 - if x land 0x80 <> 0 then x2 lxor 0x1b else x2 272 - 273 - (* Build T-table entry: [x2, x, x, x3] as Int32 *) 274 - let te0 = 275 - Array.init 256 (fun i -> 276 - let s = sbox.(i) in 277 - let x2 = xtime s in 278 - let x3 = x2 lxor s in 279 - Int32.logor 280 - (Int32.logor 281 - (Int32.shift_left (Int32.of_int x2) 24) 282 - (Int32.shift_left (Int32.of_int s) 16)) 283 - (Int32.logor (Int32.shift_left (Int32.of_int s) 8) (Int32.of_int x3))) 284 - 285 - (* Rotate T-table entries for Te1, Te2, Te3 *) 286 - let rot8 x = 287 - Int32.logor 288 - (Int32.shift_right_logical x 8) 289 - (Int32.shift_left (Int32.logand x 0xffl) 24) 290 - 291 - let te1 = Array.map rot8 te0 292 - let te2 = Array.map rot8 te1 293 - let te3 = Array.map rot8 te2 294 - 295 - (* Round constant *) 296 - let rcon = [| 0x01; 0x02; 0x04; 0x08; 0x10; 0x20; 0x40; 0x80; 0x1b; 0x36 |] 297 - 298 - (* Key schedule: returns round keys as Int32 array *) 299 - let expand_key key = 300 - let klen = String.length key in 301 - let nk = klen / 4 in 302 - let rounds = 303 - match klen with 304 - | 16 -> 10 305 - | 24 -> 12 306 - | 32 -> 14 307 - | _ -> invalid_arg "AES key" 308 - in 309 - let nb = 4 in 310 - let rk = Array.make (nb * (rounds + 1)) 0l in 311 - for i = 0 to nk - 1 do 312 - rk.(i) <- 313 - Int32.logor 314 - (Int32.logor 315 - (Int32.shift_left (Int32.of_int (Char.code key.[i * 4])) 24) 316 - (Int32.shift_left (Int32.of_int (Char.code key.[(i * 4) + 1])) 16)) 317 - (Int32.logor 318 - (Int32.shift_left (Int32.of_int (Char.code key.[(i * 4) + 2])) 8) 319 - (Int32.of_int (Char.code key.[(i * 4) + 3]))) 320 - done; 321 - let ri = ref 0 in 322 - for i = nk to (nb * (rounds + 1)) - 1 do 323 - let prev = rk.(i - 1) in 324 - let t = 325 - if i mod nk = 0 then begin 326 - let r = !ri in 327 - incr ri; 328 - let b0 = 329 - Int32.of_int 330 - (sbox.(Int32.to_int 331 - (Int32.logand (Int32.shift_right_logical prev 16) 0xffl)) 332 - lxor rcon.(r)) 333 - in 334 - let b1 = 335 - Int32.of_int 336 - sbox.(Int32.to_int 337 - (Int32.logand (Int32.shift_right_logical prev 8) 0xffl)) 338 - in 339 - let b2 = Int32.of_int sbox.(Int32.to_int (Int32.logand prev 0xffl)) in 340 - let b3 = 341 - Int32.of_int 342 - sbox.(Int32.to_int 343 - (Int32.logand (Int32.shift_right_logical prev 24) 0xffl)) 344 - in 345 - Int32.logor 346 - (Int32.logor (Int32.shift_left b0 24) (Int32.shift_left b1 16)) 347 - (Int32.logor (Int32.shift_left b2 8) b3) 348 - end 349 - else if nk > 6 && i mod nk = 4 then begin 350 - let b0 = 351 - Int32.of_int 352 - sbox.(Int32.to_int 353 - (Int32.logand (Int32.shift_right_logical prev 24) 0xffl)) 354 - in 355 - let b1 = 356 - Int32.of_int 357 - sbox.(Int32.to_int 358 - (Int32.logand (Int32.shift_right_logical prev 16) 0xffl)) 359 - in 360 - let b2 = 361 - Int32.of_int 362 - sbox.(Int32.to_int 363 - (Int32.logand (Int32.shift_right_logical prev 8) 0xffl)) 364 - in 365 - let b3 = Int32.of_int sbox.(Int32.to_int (Int32.logand prev 0xffl)) in 366 - Int32.logor 367 - (Int32.logor (Int32.shift_left b0 24) (Int32.shift_left b1 16)) 368 - (Int32.logor (Int32.shift_left b2 8) b3) 369 - end 370 - else prev 371 - in 372 - rk.(i) <- Int32.logxor rk.(i - nk) t 373 - done; 374 - (rk, rounds) 375 - 376 - (* Encrypt one 16-byte block *) 377 - let encrypt_block rk rounds src soff dst doff = 378 - let ( lxor ) = Int32.logxor in 379 - let ( land ) = Int32.logand in 380 - let ( lsr ) = Int32.shift_right_logical in 381 - let get_byte32 w shift = Int32.to_int ((w lsr shift) land 0xffl) in 382 - let get32 buf off = 383 - Int32.logor 384 - (Int32.logor 385 - (Int32.shift_left (Int32.of_int (Char.code buf.[off])) 24) 386 - (Int32.shift_left (Int32.of_int (Char.code buf.[off + 1])) 16)) 387 - (Int32.logor 388 - (Int32.shift_left (Int32.of_int (Char.code buf.[off + 2])) 8) 389 - (Int32.of_int (Char.code buf.[off + 3]))) 390 - in 391 - let put32 buf off w = 392 - Bytes.set buf off (Char.chr (get_byte32 w 24)); 393 - Bytes.set buf (off + 1) (Char.chr (get_byte32 w 16)); 394 - Bytes.set buf (off + 2) (Char.chr (get_byte32 w 8)); 395 - Bytes.set buf (off + 3) (Char.chr (get_byte32 w 0)) 396 - in 397 - let s0 = ref (get32 src soff lxor rk.(0)) in 398 - let s1 = ref (get32 src (soff + 4) lxor rk.(1)) in 399 - let s2 = ref (get32 src (soff + 8) lxor rk.(2)) in 400 - let s3 = ref (get32 src (soff + 12) lxor rk.(3)) in 401 - let rki = ref 4 in 402 - for _ = 1 to rounds - 1 do 403 - let t0 = 404 - te0.(get_byte32 !s0 24) 405 - lxor te1.(get_byte32 !s1 16) 406 - lxor te2.(get_byte32 !s2 8) 407 - lxor te3.(get_byte32 !s3 0) 408 - lxor rk.(!rki) 409 - in 410 - let t1 = 411 - te0.(get_byte32 !s1 24) 412 - lxor te1.(get_byte32 !s2 16) 413 - lxor te2.(get_byte32 !s3 8) 414 - lxor te3.(get_byte32 !s0 0) 415 - lxor rk.(!rki + 1) 416 - in 417 - let t2 = 418 - te0.(get_byte32 !s2 24) 419 - lxor te1.(get_byte32 !s3 16) 420 - lxor te2.(get_byte32 !s0 8) 421 - lxor te3.(get_byte32 !s1 0) 422 - lxor rk.(!rki + 2) 423 - in 424 - let t3 = 425 - te0.(get_byte32 !s3 24) 426 - lxor te1.(get_byte32 !s0 16) 427 - lxor te2.(get_byte32 !s1 8) 428 - lxor te3.(get_byte32 !s2 0) 429 - lxor rk.(!rki + 3) 430 - in 431 - s0 := t0; 432 - s1 := t1; 433 - s2 := t2; 434 - s3 := t3; 435 - rki := !rki + 4 436 - done; 437 - (* Final round: SubBytes + ShiftRows + AddRoundKey, no MixColumns *) 438 - let sb i = Int32.of_int sbox.(i) in 439 - let t0 = 440 - Int32.logor 441 - (Int32.logor 442 - (Int32.shift_left (sb (get_byte32 !s0 24)) 24) 443 - (Int32.shift_left (sb (get_byte32 !s1 16)) 16)) 444 - (Int32.logor 445 - (Int32.shift_left (sb (get_byte32 !s2 8)) 8) 446 - (sb (get_byte32 !s3 0))) 447 - lxor rk.(!rki) 448 - in 449 - let t1 = 450 - Int32.logor 451 - (Int32.logor 452 - (Int32.shift_left (sb (get_byte32 !s1 24)) 24) 453 - (Int32.shift_left (sb (get_byte32 !s2 16)) 16)) 454 - (Int32.logor 455 - (Int32.shift_left (sb (get_byte32 !s3 8)) 8) 456 - (sb (get_byte32 !s0 0))) 457 - lxor rk.(!rki + 1) 458 - in 459 - let t2 = 460 - Int32.logor 461 - (Int32.logor 462 - (Int32.shift_left (sb (get_byte32 !s2 24)) 24) 463 - (Int32.shift_left (sb (get_byte32 !s3 16)) 16)) 464 - (Int32.logor 465 - (Int32.shift_left (sb (get_byte32 !s0 8)) 8) 466 - (sb (get_byte32 !s1 0))) 467 - lxor rk.(!rki + 2) 468 - in 469 - let t3 = 470 - Int32.logor 471 - (Int32.logor 472 - (Int32.shift_left (sb (get_byte32 !s3 24)) 24) 473 - (Int32.shift_left (sb (get_byte32 !s0 16)) 16)) 474 - (Int32.logor 475 - (Int32.shift_left (sb (get_byte32 !s1 8)) 8) 476 - (sb (get_byte32 !s2 0))) 477 - lxor rk.(!rki + 3) 478 - in 479 - put32 dst doff t0; 480 - put32 dst (doff + 4) t1; 481 - put32 dst (doff + 8) t2; 482 - put32 dst (doff + 12) t3 483 - 484 - (* Multi-block encrypt matching the mc_aes_enc_bc interface *) 485 - let encrypt_ecb rk rounds src soff dst doff blocks = 486 - for b = 0 to blocks - 1 do 487 - encrypt_block rk rounds src (soff + (b * 16)) dst (doff + (b * 16)) 488 - done
+10 -15
src/ocaml/ghash_pure.ml
··· 1 1 (** Pure OCaml GHASH (GF(2^128) for AES-GCM). 2 2 3 - Constant-time shift-and-XOR implementation. All 128 iterations 4 - execute identical operations regardless of input values. 5 - No branches on secret data, no lookup tables. 3 + Constant-time shift-and-XOR implementation. All 128 iterations execute 4 + identical operations regardless of input values. No branches on secret data, 5 + no lookup tables. 6 6 7 7 Reference: BearSSL constant-time technique (Thomas Pornin) 8 8 https://bearssl.org/constanttime.html *) ··· 19 19 for i = 0 to 127 do 20 20 let byte = Char.code (Bytes.get x (i / 8)) in 21 21 let bit = (byte lsr (7 - (i mod 8))) land 1 in 22 - let mask = (-bit) land 0xff in 22 + let mask = -bit land 0xff in 23 23 for j = 0 to 15 do 24 24 let zj = Char.code (Bytes.get z j) in 25 25 let vj = Char.code (Bytes.get v j) in ··· 29 29 for j = 15 downto 1 do 30 30 let vj = Char.code (Bytes.get v j) in 31 31 let vj1 = Char.code (Bytes.get v (j - 1)) in 32 - Bytes.set v j 33 - (Char.chr (((vj lsr 1) lor ((vj1 land 1) lsl 7)) land 0xff)) 32 + Bytes.set v j (Char.chr ((vj lsr 1) lor ((vj1 land 1) lsl 7) land 0xff)) 34 33 done; 35 - Bytes.set v 0 36 - (Char.chr ((Char.code (Bytes.get v 0) lsr 1) land 0xff)); 37 - let reduce_mask = (-carry) land 0xff in 34 + Bytes.set v 0 (Char.chr ((Char.code (Bytes.get v 0) lsr 1) land 0xff)); 35 + let reduce_mask = -carry land 0xff in 38 36 let v0 = Char.code (Bytes.get v 0) in 39 37 Bytes.set v 0 (Char.chr (v0 lxor (0xe1 land reduce_mask))) 40 38 done; 41 39 z 42 40 43 - let ghash (key : bytes) (tag : bytes) (data : string) (off : int) 44 - (len : int) = 41 + let ghash (key : bytes) (tag : bytes) (data : string) (off : int) (len : int) = 45 42 let h = Bytes.copy key in 46 43 let nblocks = len / 16 in 47 44 for b = 0 to nblocks - 1 do ··· 50 47 Bytes.set x i 51 48 (Char.chr 52 49 (Char.code (Bytes.get tag i) 53 - lxor Char.code (String.get data (off + (b * 16) + i)))) 50 + lxor Char.code (String.get data (off + (b * 16) + i)))) 54 51 done; 55 52 let r = gf128_mul_ct x h in 56 53 Bytes.blit r 0 tag 0 16 ··· 62 59 Bytes.set x i 63 60 (Char.chr 64 61 (Char.code (Bytes.get tag i) 65 - lxor 66 - Char.code 67 - (String.get data (off + (nblocks * 16) + i)))) 62 + lxor Char.code (String.get data (off + (nblocks * 16) + i)))) 68 63 done; 69 64 for i = rem to 15 do 70 65 Bytes.set x i (Bytes.get tag i)
+4 -1
src/ocaml/native.ml
··· 61 61 Aes_pure.encrypt_ecb rka rounds src soff dst doff blocks 62 62 63 63 let dec _src _soff _dst _doff _rk _rounds _blocks = 64 - failwith "AES decrypt not implemented in pure OCaml backend (GCM uses encrypt only)" 64 + failwith 65 + "AES decrypt not implemented in pure OCaml backend (GCM uses encrypt \ 66 + only)" 67 + 65 68 let mode () = 0 (* generic *) 66 69 end 67 70
+5
test/dune
··· 21 21 ecdsa_secp521r1_sha512_test.json 22 22 x25519_test.json 23 23 eddsa_test.json)) 24 + 25 + (executable 26 + (name test_pure) 27 + (modes js exe) 28 + (libraries crypto crypto.ocaml))
+129
test/test_pure.ml
··· 1 + (** Tests for the pure OCaml crypto backend. 2 + 3 + Runs AES-GCM encrypt/decrypt against NIST test vectors to verify the pure 4 + OCaml implementation matches the C implementation. *) 5 + 6 + let hex_to_string h = 7 + let len = String.length h / 2 in 8 + String.init len (fun i -> 9 + Char.chr (int_of_string ("0x" ^ String.sub h (i * 2) 2))) 10 + 11 + let string_to_hex s = 12 + String.concat "" 13 + (List.init (String.length s) (fun i -> 14 + Printf.sprintf "%02x" (Char.code (String.get s i)))) 15 + 16 + (* NIST SP 800-38D test case 2: AES-128-GCM 17 + Key: 00000000000000000000000000000000 18 + IV: 000000000000000000000000 19 + PT: 00000000000000000000000000000000 20 + AAD: (empty) 21 + CT: 0388dace60b6a392f328c2b971b2fe78 22 + Tag: ab6e47d42cec13bdf53a67b21257bddf *) 23 + let nist_key = hex_to_string "00000000000000000000000000000000" 24 + let nist_iv = hex_to_string "000000000000000000000000" 25 + let nist_pt = hex_to_string "00000000000000000000000000000000" 26 + 27 + let nist_ct_tag = 28 + hex_to_string 29 + "0388dace60b6a392f328c2b971b2fe78ab6e47d42cec13bdf53a67b21257bddf" 30 + 31 + let test_aes_gcm_encrypt () = 32 + let key = Crypto.AES.GCM.of_secret nist_key in 33 + let result = 34 + Crypto.AES.GCM.authenticate_encrypt ~key ~nonce:nist_iv ~adata:"" nist_pt 35 + in 36 + if result = nist_ct_tag then 37 + Printf.printf "PASS: AES-128-GCM encrypt (NIST test case 2)\n" 38 + else begin 39 + Printf.printf "FAIL: AES-128-GCM encrypt\n"; 40 + Printf.printf " expected: %s\n" (string_to_hex nist_ct_tag); 41 + Printf.printf " got: %s\n" (string_to_hex result); 42 + exit 1 43 + end 44 + 45 + let test_aes_gcm_decrypt () = 46 + let key = Crypto.AES.GCM.of_secret nist_key in 47 + match 48 + Crypto.AES.GCM.authenticate_decrypt ~key ~nonce:nist_iv ~adata:"" 49 + nist_ct_tag 50 + with 51 + | Some pt when pt = nist_pt -> 52 + Printf.printf "PASS: AES-128-GCM decrypt (NIST test case 2)\n" 53 + | Some pt -> 54 + Printf.printf "FAIL: AES-128-GCM decrypt (wrong plaintext)\n"; 55 + Printf.printf " expected: %s\n" (string_to_hex nist_pt); 56 + Printf.printf " got: %s\n" (string_to_hex pt); 57 + exit 1 58 + | None -> 59 + Printf.printf "FAIL: AES-128-GCM decrypt (auth failure)\n"; 60 + exit 1 61 + 62 + (* NIST test case 4: AES-128-GCM with AAD 63 + Key: feffe9928665731c6d6a8f9467308308 64 + IV: cafebabefacedbaddecaf888 65 + PT: d9313225f88406e5a55909c5aff5269a 66 + 86a7a9531534f7da2e4c303d8a318a72 67 + 1c3c0c95956809532fcf0e2449a6b525 68 + b16aedf5aa0de657ba637b391aafd255 69 + AAD: feedfacedeadbeeffeedfacedeadbeef 70 + abaddad2 71 + CT: 42831ec2217774244b7221b784d0d49c 72 + e3aa212f2c02a4e035c17e2329aca12e 73 + 21d514b25466931c7d8f6a5aac84aa05 74 + 1ba30b396a0aac973d58e091473f5985 75 + Tag: 4d5c2af327cd64a62cf35abd2ba6fab4 *) 76 + let nist4_key = hex_to_string "feffe9928665731c6d6a8f9467308308" 77 + let nist4_iv = hex_to_string "cafebabefacedbaddecaf888" 78 + 79 + let nist4_pt = 80 + hex_to_string 81 + "d9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39" 82 + 83 + let nist4_aad = hex_to_string "feedfacedeadbeeffeedfacedeadbeefabaddad2" 84 + 85 + let nist4_ct_tag = 86 + hex_to_string 87 + ("42831ec2217774244b7221b784d0d49c" ^ "e3aa212f2c02a4e035c17e2329aca12e" 88 + ^ "21d514b25466931c7d8f6a5aac84aa05" ^ "1ba30b396a0aac973d58e091" 89 + (* tag: *) 90 + ^ "4d5c2af327cd64a62cf35abd2ba6fab4") 91 + 92 + let test_aes_gcm_encrypt_aad () = 93 + let key = Crypto.AES.GCM.of_secret nist4_key in 94 + let result = 95 + Crypto.AES.GCM.authenticate_encrypt ~key ~nonce:nist4_iv ~adata:nist4_aad 96 + nist4_pt 97 + in 98 + if result = nist4_ct_tag then 99 + Printf.printf "PASS: AES-128-GCM encrypt with AAD (NIST test case 4)\n" 100 + else begin 101 + Printf.printf "FAIL: AES-128-GCM encrypt with AAD\n"; 102 + Printf.printf " expected: %s\n" (string_to_hex nist4_ct_tag); 103 + Printf.printf " got: %s\n" (string_to_hex result); 104 + exit 1 105 + end 106 + 107 + let test_aes_gcm_decrypt_aad () = 108 + let key = Crypto.AES.GCM.of_secret nist4_key in 109 + match 110 + Crypto.AES.GCM.authenticate_decrypt ~key ~nonce:nist4_iv ~adata:nist4_aad 111 + nist4_ct_tag 112 + with 113 + | Some pt when pt = nist4_pt -> 114 + Printf.printf "PASS: AES-128-GCM decrypt with AAD (NIST test case 4)\n" 115 + | Some pt -> 116 + Printf.printf "FAIL: AES-128-GCM decrypt with AAD (wrong plaintext)\n"; 117 + Printf.printf " expected: %s\n" (string_to_hex nist4_pt); 118 + Printf.printf " got: %s\n" (string_to_hex pt); 119 + exit 1 120 + | None -> 121 + Printf.printf "FAIL: AES-128-GCM decrypt with AAD (auth failure)\n"; 122 + exit 1 123 + 124 + let () = 125 + test_aes_gcm_encrypt (); 126 + test_aes_gcm_decrypt (); 127 + test_aes_gcm_encrypt_aad (); 128 + test_aes_gcm_decrypt_aad (); 129 + Printf.printf "All tests passed.\n"