fix(Key Store): remove runtime length check on GenerateKey (#84)

* chore: Update CHANGELOG and bump version

Author: josecorella

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy

@@ -47,7 +47,6 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
     ensures res.Success? ==>
               && res.value.KeyId.Some?
               && res.value.CiphertextBlob.Some?
-              && |res.value.CiphertextBlob.value| == Structure.KMS_GEN_KEY_NO_PLAINTEXT_LENGTH_32
               && KMS.IsValid_CiphertextType(res.value.CiphertextBlob.value)
               && var kmsOperationOutput := Seq.Last(kmsClient.History.GenerateDataKeyWithoutPlaintext).output;
               && kmsOperationOutput.Success?
@@ -67,17 +66,15 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
 
     :- Need(
       && generateResponse.KeyId.Some?,
-      // && ParseAwsKmsIdentifier(generateResponse.KeyId.value).Success?,
       Types.KeyStoreException(
         message := "Invalid response from KMS GenerateDataKey:: Invalid Key Id")
     );
 
     :- Need(
       && generateResponse.CiphertextBlob.Some?
-      && |generateResponse.CiphertextBlob.value| == Structure.KMS_GEN_KEY_NO_PLAINTEXT_LENGTH_32
       && KMS.IsValid_CiphertextType(generateResponse.CiphertextBlob.value),
       Types.KeyStoreException(
-        message := "Invalid response from AWS KMS GeneratedDataKey: Invalid ciphertext")
+        message := "Invalid response from AWS KMS GenerateDataKey: Invalid ciphertext")
     );
 
     return Success(generateResponse);
@@ -161,7 +158,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
       && reEncryptResponse.CiphertextBlob.Some?
       && KMS.IsValid_CiphertextType(reEncryptResponse.CiphertextBlob.value),
       Types.KeyStoreException(
-        message := "Invalid response from AWS KMS GeneratedDataKey: Invalid ciphertext")
+        message := "Invalid response from AWS KMS ReEncrypt: Invalid ciphertext.")
     );
 
     return Success(reEncryptResponse);

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy

@@ -27,9 +27,6 @@ module {:options "/functionSyntax:4" } Structure {
   const BEACON_KEY_TYPE_VALUE := "beacon:ACTIVE"
   const ENCRYPTION_CONTEXT_PREFIX := "aws-crypto-ec:"
 
-  // A GenerateDataKeyWithoutPlaintext of request size 32 returns a ciphertext size of 184 bytes.
-  const KMS_GEN_KEY_NO_PLAINTEXT_LENGTH_32 := 184
-
   type BranchKeyContext = m: map<string, string> | BranchKeyContext?(m) witness *
   predicate BranchKeyContext?(m: map<string, string>) {
     //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context

AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts

@@ -10,7 +10,7 @@ plugins {
 }
 
 group = "software.amazon.cryptography"
-version = "1.0.0"
+version = "1.0.1"
 description = "AWS Cryptographic Material Providers Library"
 
 java {

CHANGELOG.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## 1.0.1 2023-07-26
+
+### Fix
+- Fixes a runtime check in `VersionKey` Key Store API that no longer checks for the CipherText length
+  on the output of a KMS ReEncrypt API call. 
+
 ## 1.0.0 2023-07-21
 
 ### Features

ComAmazonawsKms/src/Index.dfy

@@ -30,7 +30,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny"} Com.A
 
   function method DafnyUserAgentSuffix(runtime: string): string
   {
-    var version := "1.0.0";
+    var version := "1.0.1";
     "AwsCryptographicMPL/" + runtime + "/" + version
   }
 

README.md

@@ -72,14 +72,14 @@ You can get the latest release from Maven or Gradle:
 <dependency>
   <groupId>software.amazon.cryptography</groupId>
   <artifactId>aws-cryptographic-material-providers</artifactId>
-  <version>1.0.0</version>
+  <version>1.0.1</version>
 </dependency>
 ```
 
 #### Gradle:
 ```
 dependencies {
-    implementation("software.amazon.cryptography:aws-cryptographic-material-providers:1.0.0")
+    implementation("software.amazon.cryptography:aws-cryptographic-material-providers:1.0.1")
 }
 ```
 

TestVectorsAwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts

@@ -58,7 +58,7 @@ repositories {
 dependencies {
     implementation("org.dafny:DafnyRuntime:4.1.0")
     implementation("software.amazon.smithy.dafny:conversion:0.1")
-    implementation("software.amazon.cryptography:aws-cryptographic-material-providers:1.0.0")
+    implementation("software.amazon.cryptography:aws-cryptographic-material-providers:1.0.1")
     implementation(platform("software.amazon.awssdk:bom:2.19.1"))
     implementation("software.amazon.awssdk:dynamodb")
     implementation("software.amazon.awssdk:dynamodb-enhanced")