varification stability

aws · Oct 26, 2024 · 0c46bb3 · 0c46bb3
1 parent 0f60d17
commit 0c46bb3
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 57 deletions.
diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/...ptographicMaterialProviders/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/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/...alProviders/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<ActionInvoke<Types.EncryptedDataKey, Result<Materials.SealedDecryptionMaterials, Types.Error>>>
     ) returns (res: Result<Materials.SealedDecryptionMaterials, Types.Error>)