Skip to content

Commit 4d7d498

Browse files
josecorellatexastony
josecorella
authored and
texastony
committed
chore: bring in latest main changes
1 parent f8782d7 commit 4d7d498

File tree

3 files changed

+66
-54
lines changed

3 files changed

+66
-54
lines changed

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy

Lines changed: 54 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -457,60 +457,60 @@ module AwsKmsKeyring {
457457
&& AlgorithmSuites.GetEncryptKeyLength(input.materials.algorithmSuite) as nat == |res.value.materials.plaintextDataKey.value|
458458
&& var LastDecrypt := Last(client.History.Decrypt);
459459
&& LastDecrypt.output.Success?
460-
&& (
461-
exists edk
462-
// , returnedEncryptionAlgorithm
463-
| edk in input.encryptedDataKeys
464-
::
465-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
466-
//= type=implication
467-
//# - Its provider ID MUST exactly match the value “aws-kms”.
468-
&& var maybeWrappedMaterial :=
469-
EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
470-
&& maybeWrappedMaterial.Success?
471-
&& edk.keyProviderId == PROVIDER_ID
472-
&& KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
473-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
474-
//= type=implication
475-
//# When calling [AWS KMS Decrypt]
476-
//# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
477-
//# the keyring MUST call with a request constructed
478-
//# as follows:
479-
&& KMS.DecryptRequest(
480-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
481-
//= type=implication
482-
//# - `KeyId` MUST be the configured AWS KMS key identifier.
483-
KeyId := Some(awsKmsKey),
484-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
485-
//= type=implication
486-
//# - `CiphertextBlob` MUST be the [encrypted data key ciphertext]
487-
//# (../structures.md#ciphertext).
488-
CiphertextBlob := maybeWrappedMaterial.value,
489-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
490-
//= type=implication
491-
//# - `EncryptionContext` MUST be the [encryption context]
492-
//# (../structures.md#encryption-context) included in the input
493-
//# [decryption materials](../structures.md#decryption-materials).
494-
EncryptionContext := Some(maybeStringifiedEncCtx.value),
495-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
496-
//= type=implication
497-
//# - `GrantTokens` MUST be this keyring's [grant tokens]
498-
//# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token).
499-
GrantTokens := Some(grantTokens),
500-
EncryptionAlgorithm := None
501-
)
502-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
503-
//= type=implication
504-
//# To attempt to decrypt a particular [encrypted data key]
505-
//# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS
506-
//# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
507-
//# with the configured AWS KMS client.
508-
== LastDecrypt.input
509-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
510-
//= type=implication
511-
//# - The `KeyId` field in the response MUST equal the configured AWS
512-
//# KMS key identifier.
513-
&& LastDecrypt.output.value.KeyId == Some(awsKmsKey)
460+
&& OkForDecrypt(awsKmsArn, awsKmsKey).Pass?
461+
&& (exists edk
462+
// , returnedEncryptionAlgorithm
463+
| edk in input.encryptedDataKeys
464+
::
465+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
466+
//= type=implication
467+
//# - Its provider ID MUST exactly match the value “aws-kms”.
468+
&& var maybeWrappedMaterial :=
469+
EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
470+
&& maybeWrappedMaterial.Success?
471+
&& edk.keyProviderId == PROVIDER_ID
472+
&& KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
473+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
474+
//= type=implication
475+
//# When calling [AWS KMS Decrypt]
476+
//# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
477+
//# the keyring MUST call with a request constructed
478+
//# as follows:
479+
&& KMS.DecryptRequest(
480+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
481+
//= type=implication
482+
//# - `KeyId` MUST be the configured AWS KMS key identifier.
483+
KeyId := Some(awsKmsKey),
484+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
485+
//= type=implication
486+
//# - `CiphertextBlob` MUST be the [encrypted data key ciphertext]
487+
//# (../structures.md#ciphertext).
488+
CiphertextBlob := maybeWrappedMaterial.value,
489+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
490+
//= type=implication
491+
//# - `EncryptionContext` MUST be the [encryption context]
492+
//# (../structures.md#encryption-context) included in the input
493+
//# [decryption materials](../structures.md#decryption-materials).
494+
EncryptionContext := Some(maybeStringifiedEncCtx.value),
495+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
496+
//= type=implication
497+
//# - `GrantTokens` MUST be this keyring's [grant tokens]
498+
//# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token).
499+
GrantTokens := Some(grantTokens),
500+
EncryptionAlgorithm := None
501+
)
502+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
503+
//= type=implication
504+
//# To attempt to decrypt a particular [encrypted data key]
505+
//# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS
506+
//# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
507+
//# with the configured AWS KMS client.
508+
== LastDecrypt.input
509+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
510+
//= type=implication
511+
//# - The `KeyId` field in the response MUST equal the configured AWS
512+
//# KMS key identifier.
513+
&& LastDecrypt.output.value.KeyId == Some(awsKmsKey)
514514
)
515515
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
516516
//= type=implication

‎AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystoreadmin/dafny_to_smithy.py

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -485,3 +485,11 @@ def aws_cryptography_keystoreadmin_KeyStoreReference(dafny_input):
485485

486486
def aws_cryptography_keystoreadmin_KmsClientReference(dafny_input):
487487
return dafny_input._impl
488+
489+
490+
def aws_cryptography_keystoreadmin_PrimitivesReference(dafny_input):
491+
from aws_cryptography_primitives.smithygenerated.aws_cryptography_primitives.client import (
492+
AwsCryptographicPrimitives,
493+
)
494+
495+
return AwsCryptographicPrimitives(config=None, dafny_client=dafny_input)

‎AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystoreadmin/smithy_to_dafny.py

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -754,3 +754,7 @@ def aws_cryptography_keystoreadmin_KmsClientReference(native_input):
754754
)
755755
client.value.impl = native_input
756756
return client.value
757+
758+
759+
def aws_cryptography_keystoreadmin_PrimitivesReference(native_input):
760+
return native_input._config.dafnyImplInterface.impl

0 commit comments

Comments
 (0)