AES_256_GCM.cry

module Primitive::Symmetric::Cipher::Authenticated::AES_256_GCM where

import Primitive::Symmetric::Cipher::Block::AES256 as AES256

aes_hw_encrypt : [16][8] -> [32][8] -> [16][8]
aes_hw_encrypt in key = split (AES256::encrypt (join key) (join in))


gcm_pmult_pmod : [128] -> [128] -> [128]
gcm_pmult_pmod X Y = reverse (pmod (pmult (reverse X) (reverse Y)) <| x^^128 + x^^7 + x^^2 + x + 1|>)

gcm_polyval_mul : {n} (fin n) => [2 * (1 + n)] -> [2 * (1 + n)] -> [4 * (1 + n)]
gcm_polyval_mul X Y = (0 : [1]) # pmult X Y

gcm_polyval_red : [256] -> [128]
gcm_polyval_red X = reverse (pmod (reverse X) <| x^^128 + x^^7 + x^^2 + x + 1|>)

gcm_polyval : [128] -> [128] -> [128]
gcm_polyval X Y = gcm_polyval_red (gcm_polyval_mul X Y)

gcm_init_H : [128] -> [128]
gcm_init_H Xi = pmod (Xi # (0 : [1]))  <| 1 + x^^121 + x^^126 + x^^127 + x^^128 |>


type AES_GCM_Ctx =
  { key : [32][8]
  , iv : [12][8]
  , Xi : [16][8]
  , len : [64]
  }


get_H : AES_GCM_Ctx -> [2][64]
get_H ctx = split (join (aes_hw_encrypt zero ctx.key))

EKi : AES_GCM_Ctx -> [32] -> [16][8]
EKi ctx i = aes_hw_encrypt (ctx.iv # (split (i + 1))) ctx.key

EKij : AES_GCM_Ctx -> [32] -> [4] -> [8]
EKij ctx i j = (EKi ctx i) @ j


cipher_update : {n} (fin n) => [32] -> AES_GCM_Ctx -> [n][8] -> AES_GCM_Ctx
cipher_update enc ctx in = ctx'
  where
    enc_bytes = if enc ! 0
      then ctr32_encrypt ctx in
      else in
    ctx' = foldl cipher_update_byte ctx enc_bytes

ctr32_encrypt : {n} (fin n) => AES_GCM_Ctx -> [n][8] -> [n][8]
ctr32_encrypt ctx in = out
  where
    out = [ byte ^ (EKij ctx ((take`{32} (drop`{28} i)) + 1) (drop`{60} i)) | byte <- in | i <- [ctx.len ...] ]

cipher_update_byte : AES_GCM_Ctx -> [8] -> AES_GCM_Ctx
cipher_update_byte ctx byte = ctx'
  where
    H = join (get_H ctx)
    n = ctx.len % 16
    Xi' = update ctx.Xi n ((ctx.Xi @ n) ^ byte)
    len' = ctx.len + 1
    Xi'' = if (len' % 16) == 0
      then split (gcm_pmult_pmod H (join Xi'))
      else Xi'
    ctx' =
      { key = ctx.key
      , iv = ctx.iv
      , Xi = Xi''
      , len = len'
      }

cipher_final : AES_GCM_Ctx -> [16][8]
cipher_final ctx = (split (gcm_pmult_pmod H Xi'')) ^ (EKi ctx 0)
  where
    H = join (get_H ctx)
    Xi' = if (ctx.len % 16) != 0
      then gcm_pmult_pmod H (join ctx.Xi)
      else join ctx.Xi
    Xi'' = Xi' ^ (0 # (ctx.len * 8))