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
Merged

Simplify AES module structure #79

Show file tree
Hide file tree
Changes from 7 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::AesKeySize // 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
8 changes: 3 additions & 5 deletions Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry
View file
Open in desktop
Copy link
Contributor Author

Choose a reason for hiding this comment

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

note: I constrained AES-GCM-SIV to just use AES256, which is effectively what it was doing before (due to the type constraint below). I think a nicer option would be to write GCM-SIV in terms of a Cipher parameter and instantiate it with AES128 and 256.

I also don't think this works right now; I tried dropping a test vector in but it didn't work in either the before or after version and I chose not to spend much time debugging right now. There are some weird constraints here (for example, the RFC allows the associated data to be 0-64 bytes long; here it's restricted to a minimum of 44 bytes?). I think all of this is better suited to a separate issue, which I'm happy to write up. This work does not make anything worse, at least.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

On second look, I misread the comparison in L22. This previously supported both AES versions, but now it only supports one. I'll take another pass and try to fix it.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Fixed the supporting-multiple-keys issue in 6430913.

For the test vectors not working issue, I made a note in #82.

Original file line number Diff line number Diff line change
Expand Up @@ -14,17 +14,16 @@

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

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

parameter
/** 0: use AES128, 1: use AES256 */
type Mode : #
type constraint (1 >= Mode)
type constraint (1 == Mode)

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


type K = 128 + 128 * Mode
type KS = AES::EncKey (2 * Mode)

Expand Down Expand Up @@ -73,7 +72,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 +114,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::AesKeySize]
```

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