m

aws · Jan 28, 2025 · 9e1c922 · 9e1c922
1 parent 6e88995
commit 9e1c922
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy b/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy
@@ -478,6 +478,8 @@ module AwsKmsMrkKeyring {
         Materials.DecryptionMaterialsWithoutPlaintextDataKey(materials),
         Types.AwsCryptographicMaterialProvidersException( message := "Keyring received decryption materials that already contain a plaintext data key."));
 
+      :- OkForDecrypt(awsKmsArn, awsKmsKey);
+
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
       //# The set of encrypted data keys MUST first be filtered to match this
       //# keyring’s configuration.

diff --git a/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy
@@ -223,6 +223,8 @@ module AwsKmsRsaKeyring {
         Types.AwsCryptographicMaterialProvidersException(
           message := "Keyring received decryption materials that already contain a plaintext data key."));
 
+      :- AwsKmsUtils.OkForDecrypt(awsKmsArn, awsKmsKey);
+
       :- Need(
         input.materials.algorithmSuite.signature.None?,
         Types.AwsCryptographicMaterialProvidersException(