aes: add explicit parameterizations of aes #77

this also refactors ctr mode

Primitive/Symmetric/Cipher/Block/AES.cry

@@ -151,6 +151,10 @@ stateToMsg st = join (join (transpose st))
 aesEncrypt : ([128], [AESKeySize]) -> [128]
 aesEncrypt (pt, key) = aesEncryptWithKeySchedule pt (ExpandKey key)
 
+// AES encryption with a specified KeySchedule
+//
+// In general, this should only be used when manually rewriting proof goals
+// for optimizing proofs of properties in SAW.
 aesEncryptWithKeySchedule : [128] -> KeySchedule -> [128]
 aesEncryptWithKeySchedule pt (kInit, ks, kFinal) = stateToMsg (AESFinalRound (kFinal, rounds ! 0))
   where

Primitive/Symmetric/Cipher/Block/AES128.cry

@@ -0,0 +1,4 @@
+module Primitive::Symmetric::Cipher::Block::AES128 =
+    Primitive::Symmetric::Cipher::Block::AES_specification where
+    // This produces a key size of 128
+    type m = 0

Primitive/Symmetric/Cipher/Block/AES256.cry

@@ -0,0 +1,4 @@
+module Primitive::Symmetric::Cipher::Block::AES256 =
+    Primitive::Symmetric::Cipher::Block::AES_specification where
+    // This produces a key size of 256
+    type m = 2

Primitive/Symmetric/Cipher/Block/AES_specification.cry

@@ -0,0 +1,50 @@
+/*
+   Copyright (c) 2018 Galois, Inc.
+   www.cryptol.net
+*/
+
+module Primitive::Symmetric::Cipher::Block::AES_specification where
+
+import `Primitive::Symmetric::Cipher::Block::AES::Algorithm as AES
+import `Primitive::Symmetric::Cipher::Block::AES::ExpandKey
+import Primitive::Symmetric::Cipher::Block::AES::TBox
+import Primitive::Symmetric::Cipher::Block::Cipher(Cipher)
+
+parameter
+   type m : #
+   type constraint (fin m, m <= 2)
+
+type AesKeySize = 64 * (m + 2)
+
+type EncKey n = AES::KeySchedule n
+type DecKey n = AES::KeySchedule n
+
+AES: Cipher AesKeySize 128
+AES = { encrypt key pt = encrypt key pt
+      , decrypt key ct = decrypt key ct
+      }
+
+encrypt : [AesKeySize] -> [128] -> [128]
+encrypt k = encryptWithSchedule (expandKeyEnc k)
+
+decrypt : [AesKeySize] -> [128] -> [128]
+decrypt k = decryptWithSchedule (expandKeyDec k)
+
+
+expandKeyEnc : [AesKeySize] -> EncKey m
+expandKeyEnc = expandKey`{Nk = AES::Nk m, Nr = AES::Nr m}
+
+encryptWithSchedule : EncKey m -> [128] -> [128]
+encryptWithSchedule = AES::encrypt params
+
+expandKeyDec : [AesKeySize] -> EncKey m
+expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk m, Nr = AES::Nr m} k)
+
+decryptWithSchedule : DecKey m -> [128] -> [128]
+decryptWithSchedule = AES::decrypt params
+
+
+params = { encRound = AESRound, decRound = AESInvRound }
+
+property test k pt = decrypt k (encrypt k pt) == pt
+

Primitive/Symmetric/Cipher/Block/Modes/AES256_CTR.cry

@@ -0,0 +1,32 @@
+// Cryptol AES CTR test vectors
+// Copyright (c) 2010-2018, Galois Inc.
+// www.cryptol.net
+// Author: Ajay Kumar Eeralla
+// Test vector from https://nvlpubs.nist.gov/nistpubs/Legacy/SP nistspecialpublication800-38a.pdf
+
+module Primitive::Symmetric::Cipher::Block::Modes::AES_CTR where
+import Primitive::Symmetric::Cipher::Block::Modes::CTR
+import Primitive::Symmetric::Cipher::Block::AES_parameterized
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+
+AES128_CTR_encrypt: {n} (fin n) => [AES128::AesKeySize] -> ic -> [n]block -> [n]block
+AES128_CTR_encrypt = ctrEnc AES128::encrypt
+
+AES128_CTR_decrypt: {n} (fin n) => [AES128::AesKeySize] -> ic -> [n]block -> [n]block
+AES128_CTR_decrypt = ctrDec AES128::decrypt
+
+
+// This `:prove`s quickly!
+property aes128_ctr_enc_test_vector_passes = (AES128_CTR_encrypt k ic plaintext) == ciphertext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    plaintext = [0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [0x874d6191b620e3261bef6864990db6ce, 0x9806f66b7970fdff8617187bb9fffdff, 0x5ae4df3edbd5d35e5b4f09020db03eab, 0x1e031dda2fbe03d1792170a0f3009cee]
+
+property aes128_ctr_dec_test_vector_passes = (AES128_CTR_decrypt k ic ciphertext) == plaintext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    ciphertext = [0x874d6191b620e3261bef6864990db6ce, 0x9806f66b7970fdff8617187bb9fffdff, 0x5ae4df3edbd5d35e5b4f09020db03eab, 0x1e031dda2fbe03d1792170a0f3009cee]
+    plaintext = [0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]

Primitive/Symmetric/Cipher/Block/Modes/CTR.cry

@@ -20,6 +20,7 @@ ctrDec enc k c cs = ps
     where ps = [(enc k c')^ct | ct <- cs | c' <- ctrs]
           ctrs = [c+i | i<- [0...]]
 
-
+// This will need to be parameterized with a specific encryption function before it can be proved
+property ctrEncCorrect enc k c ps = (ctrDec enc k c (ctrEnc enc k c ps)) == ps
 
 

Primitive/Symmetric/Cipher/Block/Tests/TestAES256.cry

@@ -0,0 +1,14 @@
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
+
+testmsgs = [0x6bc1bee22e409f96e93d7e117393172a
+           ,0xae2d8a571e03ac9c9eb76fac45af8e51
+           ,0x30c81c46a35ce411e5fbc1191a0a52ef
+           ,0xf69f2445df4f9b17ad2b417be66c3710]
+testkey256 = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
+testct256 = [0xf3eed1bdb5d2a03c064b5a7e3db181f8
+        ,0x591ccb10d410ed26dc5ba74a31362870
+        ,0xb6ed21b99ca6f4f9f153e7b1beafed1d
+        ,0x23304b7a39f9f3ff067d8d8f9e24ecc7]
+
+property testsPass = and [ AES256::encrypt testkey256 msg == ct
+                     | msg <- testmsgs | ct <- testct256 ]