MEE_CBC.cry

/*
  Copyright (c) 2018, Galois Inc.
  www.cryptol.net
 */


module Primitive::Symmetric::Cipher::Authenticated::MEE_CBC where


// Fixing block size for simplicity.
type blkBytes = 16
// Using blocks of bytes for greatest compatibility with both EasyCrypt
// and other external descriptions of these algorithms
type Blk = [blkBytes][8]
// Fixing encryption key size for simplicity.
type EKey = [blkBytes][8]

// Fixing tag size for simplicity.
type tagBytes = 32
type Tag = [tagBytes][8]

// Fixing signing key size for simplicity.
type skeyBytes = 64
type SKey = [skeyBytes][8]

cbc_enc : {n} (fin n) => (EKey -> Blk -> Blk) -> EKey -> Blk -> [n]Blk -> [n]Blk
cbc_enc enc k iv ps = cs
 where cs = [ enc k (p ^ c') | p <- ps | c' <- [iv] # cs ]

cbc_dec : {n} (fin n) => (EKey -> Blk -> Blk) -> EKey -> Blk -> [n]Blk -> [n]Blk
cbc_dec dec k iv cs = [ (dec k c) ^ c' | c <- cs | c' <- [iv] # cs ]

pad : {n, p, b}
      (fin n, 8 >= width p, p == blkBytes*b - n, blkBytes*b >= n) =>
      [n][8] -> Tag -> [b+2]Blk
pad msg tag = split `{each=blkBytes} (msg # tag # padding)
  where
    padding = (repeat `p) : [p][8]

unpad : {n, p, b}
        (fin n, 8 >= width p, p == blkBytes*b - n, blkBytes*b >= n) =>
        [b+2]Blk -> ([n][8], Tag, Bit)
unpad ct = (m, t, good)
  where
    padded = join ct
    m = take `{n} padded
    t = take `{tagBytes} (drop `{n} padded)
    p = drop `{n + tagBytes} padded
    good = p == ((repeat `p) : [p][8]) /* /\ 1 <= p /\ p <= 16 */

property unpad_pad_good_1000_256 msg tag =
  unpad (pad `{n=1000,p=104} msg tag) == (msg, tag, True)

mee_enc : {n, p, b}
          (fin n, p == blkBytes*b - n, 8 >= width p, b >= 1, 16*b >= n) =>
          (Blk -> Blk -> Blk)
       -> (SKey -> [n][8] -> Tag)
       -> EKey -> SKey -> Blk -> [n][8] -> [b+2]Blk
mee_enc enc sign ekey skey iv msg =
  cbc_enc enc ekey iv (pad msg (sign skey msg))

mee_dec : {n, p, b}
          (fin n, p == blkBytes*b - n, 8 >= width (32 + p), b >= 1, 16*b >= n)
       => (EKey -> Blk -> Blk)
       -> (SKey -> [n][8] -> Tag)
       -> EKey -> SKey -> Blk -> [b+2]Blk -> ([n][8], Bit)
mee_dec dec sign ekey skey iv ct = (m, good /\ sign skey m == t)
  where
    (m, t, good) = unpad (cbc_dec dec ekey iv ct)

property mee_enc_dec_good_1000 enc dec sign ekey skey iv msg =
  mee_dec `{n=1000,p=104} dec sign ekey skey iv ct == (msg, True)
    where ct = mee_enc `{n=1000,p=104} enc sign ekey skey iv msg