aes-gcm: clarify documentation, properties #46

- improves some documentation
- moves parameterization of several properties into the aes-gcm module,
  instead of doing it on the fly in the batch file

Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry

@@ -10,9 +10,21 @@ module Primitive::Symmetric::Cipher::Authenticated::AES_GCM where
 import `Primitive::Symmetric::Cipher::Authenticated::GCM
 import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
 
-aesGcmIsSymmetric : [128] -> [96] -> [256] -> [0] -> Bool
+// 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
 
+// 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
+
+// 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 AES_GCM_test_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         pt = []

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

@@ -1,6 +1,7 @@
 /*
 Galois Counter Mode in Cryptol
 Copyright (c) 2017-2018, Galois, Inc.
+Author: Sean Weaver, Marcella Hastings
 
 This implementation follows NIST special publication 800-38D:
 [NISTSP800-38D] Morris Dworkin. Recommendation for Block Cipher Modes

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

@@ -9,18 +9,20 @@
 
 // The following checks do not really provide any significant formal
 // verification because they check so little of the sample space.
+// They each take a long time to `:prove` and would likely require
+// manual modification to prove in a reasonable amount of time.
 
 // These properties can be checked manually; one of the APIs calls the other.
-// They take more than an hour to prove.
-:check decryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}
-:check encryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}
+// They take more than an hour to `:prove`.
+:check aesGcmDecryptionApisAreEquivalent
+:check aesGcmEncryptionApisAreEquivalent
 
 // This property is independent of the type parameters but we have to specify
 // them anyway.
-// It takes more than 25 minutes to prove.
+// It takes more than 25 minutes to `:prove`.
 :check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}
 
 // Make sure that decryption is the inverse of encryption
-// This property takes more than 20 minutes to prove
+// This property takes more than 20 minutes to `:prove`.
 // It's also spot-checked in the test vectors
 :check aesGcmIsSymmetric