From af315641d4d1228c8f0bed11bd773e2144da4927 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 10 Apr 2024 16:11:44 -0700 Subject: [PATCH] put flavor extracting concept inside else block --- ...raphyDbEncryptionSdkDynamoDbOperations.dfy | 69 ++++++++++--------- 1 file changed, 35 insertions(+), 34 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy index 20d1ef2ce..df28daede 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy @@ -85,42 +85,43 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt branchKeyVersion := None ); } + else { + :- Need(deserializedHeader.flavor == 0 || deserializedHeader.flavor == 1, E("Invalid format flavor.")); + var algorithmSuite; + //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior + //= type=implication + //# - This operation MUST extract the Format Flavor from the deserialize header. + if deserializedHeader.flavor == 0{ + algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384; + } else { + algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384; + } - :- Need(deserializedHeader.flavor == 0 || deserializedHeader.flavor == 1, E("Invalid format flavor.")); - var algorithmSuite; - //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior - //= type=implication - //# - This operation MUST extract the Format Flavor from the deserialize header. - if deserializedHeader.flavor == 0{ - algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384; - } else { - algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384; - } - - var extractedKeyProviderIdInfo :- UTF8.Decode(datakeys[i].keyProviderInfo).MapFailure(e => E(e)); + var extractedKeyProviderIdInfo :- UTF8.Decode(datakeys[i].keyProviderInfo).MapFailure(e => E(e)); - if extractedKeyProviderId == "aws-kms-hierarchy" { - var providerWrappedMaterial :- EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).MapFailure(e => AwsCryptographyMaterialProviders(e)); - var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH; - var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH; - :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index.")); - :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length.")); - var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX]; - var expectedBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e)); - singleDataKeyOutput := EncryptedDataKeyDescription( - keyProviderId := extractedKeyProviderId, - keyProviderInfo := Some(extractedKeyProviderIdInfo), - branchKeyId := Some(extractedKeyProviderIdInfo), - branchKeyVersion := Some(expectedBranchKeyVersion) - ); - } - else { - singleDataKeyOutput := EncryptedDataKeyDescription( - keyProviderId := extractedKeyProviderId, - keyProviderInfo := Some(extractedKeyProviderIdInfo), - branchKeyId := None, - branchKeyVersion := None - ); + if extractedKeyProviderId == "aws-kms-hierarchy" { + var providerWrappedMaterial :- EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).MapFailure(e => AwsCryptographyMaterialProviders(e)); + var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH; + var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH; + :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index.")); + :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length.")); + var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX]; + var expectedBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e)); + singleDataKeyOutput := EncryptedDataKeyDescription( + keyProviderId := extractedKeyProviderId, + keyProviderInfo := Some(extractedKeyProviderIdInfo), + branchKeyId := Some(extractedKeyProviderIdInfo), + branchKeyVersion := Some(expectedBranchKeyVersion) + ); + } + else { + singleDataKeyOutput := EncryptedDataKeyDescription( + keyProviderId := extractedKeyProviderId, + keyProviderInfo := Some(extractedKeyProviderIdInfo), + branchKeyId := None, + branchKeyVersion := None + ); + } } list := list + [singleDataKeyOutput]; }