diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy index ef4d1fa88..13dc2d3a4 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy @@ -587,7 +587,8 @@ module {:options "/functionSyntax:4" } LocalCMC { assert MutableMapIsInjective(cache) by { // Since the map values are themselves heap objects, we need to check that they too are unchanged - assert forall k <- cache.Keys() :: old(allocated(cache.Select(k))) && unchanged(cache.Select(k)); + assert forall k <- cache.Keys() :: old(allocated(cache.Select(k))); + assert forall k <- cache.Keys() :: unchanged(cache.Select(k)); assert MutableMapIsInjective(old@CAN_REMOVE(cache)); assert MutableMapContains(old@CAN_REMOVE(cache), cache); diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy index 1f8aaa4e8..2621e9603 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy @@ -455,67 +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) // For intermedite key wrapping, KMS::Decrypt.Plaintext is the intermediate key { @@ -708,7 +710,7 @@ module AwsKmsKeyring { true } - method Invoke( + method {:vcs_split_on_every_assert} Invoke( edk: Types.EncryptedDataKey, ghost attemptsState: seq>> ) returns (res: Result)