From 982748a1def22e5f2b04b0b23463bf39bf3a3760 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 13 Aug 2024 19:02:02 -0400 Subject: [PATCH 1/2] fix: update error message --- DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy index 50ed595bb..8d44ee51e 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy @@ -118,7 +118,7 @@ module StructuredEncryptionFooter { //= specification/structured-encryption/footer.md#recipient-tag-verification //# Verification MUST fail unless at least one of the [Recipient Tags](#recipient-tags) //# matches a calculated recipient tag using the provided symmetricSigningKey. - :- Need(foundTag, E("No recipient tag matched.")); + :- Need(foundTag, E("Signature of record does not match the signature computed when the record was encrypted.")); :- Need(sig.Some? == mat.algorithmSuite.signature.ECDSA?, E("Internal error. Signature both does and does not exist.")); //= specification/structured-encryption/footer.md#signature-verification From 7597a1329d6bc595002b897fa53c5ba7282d2f74 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 13 Aug 2024 19:05:54 -0400 Subject: [PATCH 2/2] m --- .../DynamoDbEncryptionTransforms/test/QueryTransform.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy index 72f474bb1..382e6e0fc 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy @@ -172,7 +172,7 @@ module QueryTransformTest { expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors( [ - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "No recipient tag matched.")))), + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "Signature of record does not match the signature computed when the record was encrypted.")))), AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234; sortKey = 01020304") ], message := "Error(s) found decrypting Query results." @@ -191,7 +191,7 @@ module QueryTransformTest { expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors( [ - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "No recipient tag matched.")))), + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "Signature of record does not match the signature computed when the record was encrypted.")))), AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234; sortKey = 01020304"), AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 890; sortKey = 030104") ], @@ -209,7 +209,7 @@ module QueryTransformTest { expect transformed_scan.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors( [ - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "No recipient tag matched.")))), + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "Signature of record does not match the signature computed when the record was encrypted.")))), AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234; sortKey = 01020304"), AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 890; sortKey = 030104") ],