Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplify AES module structure #79

Merged
merged 9 commits into from
Jun 27, 2024
+360 −449
Merged

Simplify AES module structure #79

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
53d6e68
aes: add concrete instantiations of AES #77
marsella Jun 24, 2024
6b1af4b
aes: use explicit params in cbc, cfb, ctr mode #77
marsella Jun 24, 2024
8c14010
aes: use explicit AES in gcm and gcm-siv mode #77
marsella Jun 24, 2024
302d249
aes: remove aes_parameterized version #77
marsella Jun 24, 2024
9e1b9a0
aes: add concrete instantiation for AES-192 #77
marsella Jun 24, 2024
c46fa18
aes: add basic test vector for 128, 192 #77
marsella Jun 24, 2024
0244aa4
aes: replace duplicate AES.cry with AES256 #77
marsella Jun 24, 2024
6430913
aes: update KeySize definition, accessibility #77
marsella Jun 26, 2024
d736d81
aes: add migration guide for aes API changes #77
marsella Jun 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Primitive/Keyless/Generator/DRBG.cry
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@

module Primitive::Keyless::Generator::DRBG where

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

type keylen = AESKeySize // bits
type keylen = AES256::KeySize // bits
type blocklen = 128 // bits
type seedlen = 384 // bits, 384 bits fixed by table 3 for AES-256
type reseed_limit = 2 ^^ 35 // max number of bytes to generate before reseeding
Expand All @@ -19,7 +19,7 @@ type seedsize = 48
type cipher_ctx = { key : [keylen] }

block_encrypt : [keylen] -> [blocklen] -> [blocklen]
block_encrypt key data = aesEncrypt(data, key)
block_encrypt key data = AES256::encrypt key data

type s2n_drbg =
{ bytes_used : [64]
Expand Down
5 changes: 2 additions & 3 deletions Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
module Primitive::Symmetric::Cipher::Authenticated::AES_256_GCM where

import Primitive::Symmetric::Cipher::Block::AES

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

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


gcm_pmult_pmod : [128] -> [128] -> [128]
Expand Down
51 changes: 30 additions & 21 deletions Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

// Cryptol AES GCM test vectors
// Cryptol instatiation of AES128-GCM and AES256-GCM, and test vectors for each.
// Copyright (c) 2010-2024, Galois Inc.
// www.cryptol.net
// Author: Ajay Kumar Eeralla
Expand All @@ -8,43 +8,52 @@

module Primitive::Symmetric::Cipher::Authenticated::AES_GCM where
import `Primitive::Symmetric::Cipher::Authenticated::GCM
import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
import Primitive::Symmetric::Cipher::Block::AES128 as AES128
import Primitive::Symmetric::Cipher::Block::AES256 as AES256

AES128_GCM_encrypt = GCM_AE `{K=128} {E=AES128::encrypt}
AES128_GCM_decrypt = GCM_AD `{K=128} {E=AES128::encrypt}

AES256_GCM_encrypt = GCM_AE `{K=256} {E=AES256::encrypt}
AES256_GCM_decrypt = GCM_AD `{K=256} {E=AES256::encrypt}
Comment on lines +14 to +18
Copy link
Contributor Author

@marsella marsella Jun 24, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

question: I am trying to partially initialize the functor here -- set the K and E parameters and leave the others (T, AAD, IV) up to the caller. This compiled the way I expected, but below on L40 & L41, I wasn't able to specify those other parameters when I called it; I had to give explicit types to the parameters themselves. E.g. I thought I could do

AES128_GCM_encrypt `{ IV=96 } zero zero [] []

but I couldn't get the bracket notation to compile. Instead, I had to specify the type of the IV where I declared it:

iv = zero: [96]
AES128_GCM_encrypt zero iv [] []

Why is that the case? And does this still do what I want it to do (instantiate AES-GCM for a fixed key size and arbitrary IV, plaintext, and tag length)?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this has something to do with the fact that the wrapper API here isn't actually a functor. I guess the bracket notation only operates directly on a functor, and if I wanted to be able to explicitly specify these types I'd have to make AES_GCM be a functor as well with the additional parameters defined. Maybe this can be done in #80 if we think it's useful.


// GCM's symmetry property must hold for AES.
// The other type parameter sizes are chosen arbitrarily.
aesGcmIsSymmetric: [128] -> [96] -> [256] -> [0] -> Bool
property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES::encrypt } key iv pt aad
property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES128::encrypt } key iv pt aad

// GCM's decryption API equivalence must hold for AES.
// The other type parameter sizes are chosen arbitrarily.
aesGcmDecryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES::encrypt} key iv ct [] tag
property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES128::encrypt} key iv ct [] tag

// GCM's encryption API equivalence must hold for AES.
// The other type parameter sizes are chosen arbitrarily.
aesGcmEncryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES::encrypt} key iv pt []
property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES128::encrypt} key iv pt []

property AES_GCM_test_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
where
pt = []
(ct, tag) = GCM_AE `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero pt []
dec = GCM_AD `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero ct [] tag
expected_ct = []
expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a
key = zero : [128]
iv = zero : [96]
(ct, tag) = AES128_GCM_encrypt key iv pt []
dec = AES128_GCM_decrypt key iv ct [] tag
expected_ct = [] : [0]
expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a : [128]
valid_dec = dec.valid && (dec.pt == pt)

property AES_GCM_test_vector_1 =
ct == expected_ct /\ tag == expected_tag /\ valid_dec
where
key = zero
iv = zero
iv = zero : [96]
pt = zero
aad = []
expected_ct = 0x0388dace60b6a392f328c2b971b2fe78
expected_ct = 0x0388dace60b6a392f328c2b971b2fe78 : [128]
expected_tag = 0xab6e47d42cec13bdf53a67b21257bddf : [128]
(ct, tag) = GCM_AE `{K=128, IV=96} {E=AES::encrypt} key iv pt aad
dec = GCM_AD `{K=128, IV=96} {E=AES::encrypt} key iv ct aad tag
(ct, tag) = AES128_GCM_encrypt key iv pt aad
dec = AES128_GCM_decrypt key iv ct aad tag
valid_dec = dec.valid && (dec.pt == pt)

property AES_GCM_test_vector_2 =
Expand All @@ -56,8 +65,8 @@ property AES_GCM_test_vector_2 =
aad = []
expected_ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985
expected_tag = 0x4d5c2af327cd64a62cf35abd2ba6fab4 : [128]
(ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
(ct, tag) = AES128_GCM_encrypt key iv pt aad
dec = AES128_GCM_decrypt key iv ct aad tag
valid_dec = dec.valid && (dec.pt == pt)

property AES_GCM_test_vector_3 =
Expand All @@ -69,8 +78,8 @@ property AES_GCM_test_vector_3 =
aad = 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2
expected_ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091
expected_tag = 0x5bc94fbc3221a5db94fae95ae7121a47
(ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
(ct, tag) = AES128_GCM_encrypt key iv pt aad
dec = AES128_GCM_decrypt key iv ct aad tag
valid_dec = dec.valid && (dec.pt == pt)

// A test case from aesgcmtest.c
Expand All @@ -83,8 +92,8 @@ property AES_GCM_test_vector_4 =
aad = 0x4d23c3cec334b49bdb370c437fec78de : [128]
expected_ct = 0xf7264413a84c0e7cd536867eb9f21736
expected_tag = 0x67ba0510262ae487d737ee6298f77e0c
(ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
(ct, tag) = AES256_GCM_encrypt key iv pt aad
dec = AES256_GCM_decrypt key iv ct aad tag
valid_dec = dec.valid && (dec.pt == pt)

property AES_GCM_invalid_test_vector =
Expand All @@ -97,5 +106,5 @@ property AES_GCM_invalid_test_vector =
expected_ct = 0xf7264413a84c0e7cd536867eb9f21736
expected_tag = 0x67ba0510262ae487d737ee6298f77e0c
invalid_tag = 0x67ba0510262ae487d737ee6298f77888
(ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
dec = GCM_AD {E=AES::encrypt} key iv ct aad invalid_tag
(ct, tag) = AES256_GCM_encrypt key iv pt aad
dec = AES256_GCM_decrypt key iv ct aad invalid_tag
30 changes: 18 additions & 12 deletions Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,26 +14,33 @@

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

import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES

parameter
/** 0: use AES128, 1: use AES256 */
type Mode : #
type constraint (1 >= Mode)
// 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
type KS = AES::EncKey (2 * Mode)
import Primitive::Symmetric::Cipher::Block::AES_specification as AES where
type KeySize' = KeySize
type KS = AES::EncryptionKey


/** 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
*/
* 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]
Expand Down Expand Up @@ -73,7 +80,7 @@ gcm_siv_plus (K1,K2) N AAD MSG = (unblockify Cs,TAG)
T = polyvalFrom K1 (A # M # [msg_len # aad_len]) 0
A = blockify AAD
M = blockify MSG
aad_len = `AAD : [64]
aad_len = `AAD: [64]
msg_len = `n : [64]

_ # tUpper # tLower = TAG
Expand Down Expand Up @@ -115,4 +122,3 @@ unblockify xs = take (join [ byteSwap b | b <- xs ])
// This function changes back and forth.
byteSwap : {n} (fin n) => [8 * n] -> [8 * n]
byteSwap xs = join (reverse (split`{each=8} xs))

6 changes: 3 additions & 3 deletions Primitive/Symmetric/Cipher/Authenticated/SIV_rfc5297.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
```
module Primitive::Symmetric::Cipher::Authenticated::SIV_rfc5297 where

import Primitive::Symmetric::Cipher::Block::AES
import Primitive::Symmetric::Cipher::Block::AES128 as AES128

type Key = [AESKeySize]
type Key = [AES128::KeySize]
```

Network Working Group D. Harkins
Expand Down Expand Up @@ -307,7 +307,7 @@ bitand a b = a && b

```
E : (Key,[128]) -> [128]
E(K,X) = aesEncrypt (X,K)
E(K,X) = AES128::encrypt K X

// 1. Apply the subkey generation process in Sec. 6.1 to K to produce K1 and K2.
// 2. If Mlen = 0, let n = 1; else, let n = ⎡Mlen/b⎤.
Expand Down
2 changes: 1 addition & 1 deletion Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
// This property is independent of the type parameters but we have to specify
// them anyway.
// It takes more than 25 minutes to `:prove`.
:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}
:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES128::encrypt}

// Make sure that decryption is the inverse of encryption
// This property takes more than 20 minutes to `:prove`.
Expand Down
Loading