m

aws · Feb 12, 2025 · 55f5bf6 · 55f5bf6
1 parent 89e51e3
commit 55f5bf6
Showing 1 changed file with 57 additions and 56 deletions.
diff --git a/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy
@@ -455,68 +455,69 @@ module AwsKmsKeyring {
           && AlgorithmSuites.GetEncryptKeyLength(input.materials.algorithmSuite) as nat == |res.value.materials.plaintextDataKey.value|
           && var LastDecrypt := Last(client.History.Decrypt);
           && LastDecrypt.output.Success?
-          && exists edk
-               // , returnedEncryptionAlgorithm
-               | edk in input.encryptedDataKeys
-               ::
-                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                 //= type=implication
-                 //# - Its provider ID MUST exactly match the value “aws-kms”.
-                 && var maybeWrappedMaterial :=
-                   EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
-                 && maybeWrappedMaterial.Success?
-                 && edk.keyProviderId == PROVIDER_ID
-                 && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                    //= type=implication
-                    //# When calling [AWS KMS Decrypt]
-                    //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
-                    //# the keyring MUST call with a request constructed
-                    //# as follows:
-                 && KMS.DecryptRequest(
-                      //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                      //= type=implication
-                      //# - `KeyId` MUST be the configured AWS KMS key identifier.
-                      KeyId := Some(awsKmsKey),
+          && (
+               exists edk
+                 // , returnedEncryptionAlgorithm
+                 | edk in input.encryptedDataKeys
+                 ::
+                   //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                   //= type=implication
+                   //# - Its provider ID MUST exactly match the value “aws-kms”.
+                   && var maybeWrappedMaterial :=
+                     EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
+                   && maybeWrappedMaterial.Success?
+                   && edk.keyProviderId == PROVIDER_ID
+                   && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
                       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
                       //= type=implication
-                      //# - `CiphertextBlob` MUST be the [encrypted data key ciphertext]
-                      //# (../structures.md#ciphertext).
-                      CiphertextBlob := maybeWrappedMaterial.value,
+                      //# When calling [AWS KMS Decrypt]
+                      //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
+                      //# the keyring MUST call with a request constructed
+                      //# as follows:
+                   && KMS.DecryptRequest(
+                        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                        //= type=implication
+                        //# - `KeyId` MUST be the configured AWS KMS key identifier.
+                        KeyId := Some(awsKmsKey),
+                        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                        //= type=implication
+                        //# - `CiphertextBlob` MUST be the [encrypted data key ciphertext]
+                        //# (../structures.md#ciphertext).
+                        CiphertextBlob := maybeWrappedMaterial.value,
+                        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                        //= type=implication
+                        //# - `EncryptionContext` MUST be the [encryption context]
+                        //# (../structures.md#encryption-context) included in the input
+                        //# [decryption materials](../structures.md#decryption-materials).
+                        EncryptionContext := Some(maybeStringifiedEncCtx.value),
+                        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                        //= type=implication
+                        //# - `GrantTokens` MUST be this keyring's [grant tokens]
+                        //# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token).
+                        GrantTokens := Some(grantTokens),
+                        EncryptionAlgorithm := None
+                      )
                       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
                       //= type=implication
-                      //# - `EncryptionContext` MUST be the [encryption context]
-                      //# (../structures.md#encryption-context) included in the input
-                      //# [decryption materials](../structures.md#decryption-materials).
-                      EncryptionContext := Some(maybeStringifiedEncCtx.value),
+                      //# To attempt to decrypt a particular [encrypted data key]
+                      //# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS
+                      //# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
+                      //# with the configured AWS KMS client.
+                      == LastDecrypt.input
                       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
                       //= type=implication
-                      //# - `GrantTokens` MUST be this keyring's [grant tokens]
-                      //# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token).
-                      GrantTokens := Some(grantTokens),
-                      EncryptionAlgorithm := None
-                    )
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                    //= type=implication
-                    //# To attempt to decrypt a particular [encrypted data key]
-                    //# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS
-                    //# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
-                    //# with the configured AWS KMS client.
-                    == LastDecrypt.input
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                    //= type=implication
-                    //# - The `KeyId` field in the response MUST equal the configured AWS
-                    //# KMS key identifier.
-                 && LastDecrypt.output.value.KeyId == Some(awsKmsKey)
-
-                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                 //= type=implication
-                 //# - MUST immediately return the modified [decryption materials]
-                 //# (../structures.md#decryption-materials).
-                 && (
-                      input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING?
-                      ==>
-                        LastDecrypt.output.value.Plaintext == res.value.materials.plaintextDataKey)
+                      //# - The `KeyId` field in the response MUST equal the configured AWS
+                      //# KMS key identifier.
+                   && LastDecrypt.output.value.KeyId == Some(awsKmsKey)
+             )
+             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+             //= type=implication
+             //# - MUST immediately return the modified [decryption materials]
+             //# (../structures.md#decryption-materials).
+          && (
+               input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING?
+               ==>
+                 LastDecrypt.output.value.Plaintext == res.value.materials.plaintextDataKey)
     {
 
       var materials := input.materials;