AES_GCM_SIV.cry

/* This module implements that AES-GCM-SIV mode of operations
   as described in:

   "AES-GCM-SIV: Specification and Analysis"
   by Shay Gueron, Adam Langley, and Yehuda Lindell

   See also:
   https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06

   @copyright Galois Inc.
   @author Nichole Schimanski <nls@galois.com>
   @author Marcella Hastings <marcella@galois.com>
   www.cryptol.net

*/

module Primitive::Symmetric::Cipher::Authenticated::AES_GCM_SIV where

parameter
  // This constraint enforces the standard key sizes of 128 and
  // 256-bits recommended in the draft RFC.
  type KeySize : #
  type constraint (fin KeySize, KeySize % 128 == 0, KeySize / 128 >= 1, KeySize / 128 <= 2)

  type AAD : #
  type constraint ( (36 + 8) >= width AAD )


/** This bit of algebra is here to satisfy the constraint solver.
 * `K` should be the same as `KeySize`, but the type inference doesn't work
 * if you set it directly equal.
 * `Mode` is 0 for AES-128 and 1 for AES-256.
 */
type Mode = KeySize / 128 - 1
type K  = 128 + 128 * Mode
import Primitive::Symmetric::Cipher::Block::AES_specification as AES where
  type KeySize' = KeySize
type KS = AES::ExpandedKey


/** Note the weird byte-swapping business (also in `blockify` and `unblockify`)
 * It is not quite clear in what format we want the inputs/outputs, but we
 * do the swapping so that inputs/ouputs match the test vectors at
 * https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06
 */
aes_gcm_siv :
  {n} ((36 + 8) >= width n) =>
      { key   : [K]
      , nonce : [96]
      , aad   : [AAD]
      , msg   : [n]
      } -> [n + 128]
aes_gcm_siv input = c # byteSwap t
  where
  (c,t) = gcm_siv_plus (derive_key k' n') n' input.aad input.msg
  k'    = byteSwap input.key
  n'    = byteSwap input.nonce

aes : KS -> [128] -> [128]
aes ks v = byteSwap (AES::encryptWithSchedule ks (byteSwap v))

expandKey : [K] -> KS
expandKey k = AES::keyExpansion (byteSwap k)

/** See Figure 2 in Section 4 */
derive_key : [K] -> [96] -> ([128], KS)
derive_key K N = (mkKey parts1, expandKey (mkKey parts2))
  where
  parts1 # parts2 = [ drop (aes (expandKey K) (N # i)) | i <- take [ 0 ... ]  ]

  mkKey : {n} (fin n) => [n][64] -> [64 * n]
  mkKey xs = join (reverse xs)


/** See Figure 1 in Section 3 */
gcm_siv_plus :
  {n} (64 >= width n) => ([128], KS) -> [96] -> [AAD] -> [n] -> ([n],[128])
gcm_siv_plus (K1,K2) N AAD MSG = (unblockify Cs,TAG)
  where

  TAG     = aes K2 (0b0 # drop (T ^ (0 # N)))
  T       = polyvalFrom K1 (A # M # [msg_len # aad_len]) 0
  A       = blockify AAD
  M       = blockify MSG
  aad_len = `AAD: [64]
  msg_len = `n   : [64]

  _ # tUpper # tLower = TAG

  Cs = counter_mode K2 (0b1 # tUpper, tLower) M

counter_mode : {n} KS -> ([96],[32]) -> [n][128] -> [n][128]
counter_mode K2 (tUpper,tLower) M =
            [ aes K2 (tUpper # lower32 i) ^ m | m <- M | i <- [ 0 ... ] ]
  where
  lower32 i = tLower + i


/** See Section 2.2 */
polyvalFrom : {n} (fin n) => [128] -> [n][128] -> [128] -> [128]
polyvalFrom H Xs start = psums ! 0
  where psums = [start] # [ dot (s ^ x) H | s <- psums | x <- Xs ]

dot : [128] -> [128] -> [128]
dot x y = mult x (mult y x_neg_128)
  where x_neg_128 = <| 1 + x^^114 + x^^121 + x^^124 + x^^127 |>
        // This is x^(-128)


mult : [128] -> [128] -> [128]
mult x y = pmod (pmult x y) irred
  where
  irred = <| 1 + x^^121 + x^^126 + x^^127 + x^^128 |>

// -----------------------------------------------------------------------------

blockify : {n} (fin n) => [n] -> [n /^ 128][128]
blockify x = [ byteSwap b | b <- split (x # zero) ]

unblockify : {n} (fin n) => [n /^ 128][128] -> [n]
unblockify xs = take (join [ byteSwap b | b <- xs ])

// The spec uses byte-oriented little-endian representations.
// This function changes back and forth.
byteSwap : {n} (fin n) => [8 * n] -> [8 * n]
byteSwap xs = join (reverse (split`{each=8} xs))