diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy index 5aff73b03..25de33e48 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy @@ -82,13 +82,31 @@ module {:options "-functionSyntax:4"} TestVectors { && result.Success? && result.value.decryptionMaterials.plaintextDataKey == test.vector.expectedResult.plaintextDataKey && result.value.decryptionMaterials.symmetricSigningKey == test.vector.expectedResult.symmetricSigningKey - && result.value.decryptionMaterials.requiredEncryptionContextKeys == test.vector.expectedResult.requiredEncryptionContextKeys + && multiset(result.value.decryptionMaterials.requiredEncryptionContextKeys) == multiset(test.vector.expectedResult.requiredEncryptionContextKeys) case NegativeDecryptKeyringTest(_,_,_,_,_,_,_,_,_) => !result.Success?; if !output { - if test.vector.PositiveDecryptKeyringTest? && result.Failure? { - print result.error; + if test.vector.PositiveDecryptKeyringTest? { + if result.Failure? { + print "Error : ", result.error, "\n"; + } else { + if (result.value.decryptionMaterials.plaintextDataKey != test.vector.expectedResult.plaintextDataKey) { + print "Error : plaintextDataKey does not match.\n", + test.vector.expectedResult.plaintextDataKey, "\n", + result.value.decryptionMaterials.plaintextDataKey, "\n"; + } + if (result.value.decryptionMaterials.symmetricSigningKey != test.vector.expectedResult.symmetricSigningKey) { + print "Error : symmetricSigningKey does not match.\n", + test.vector.expectedResult.symmetricSigningKey, "\n", + result.value.decryptionMaterials.symmetricSigningKey, "\n"; + } + if (multiset(result.value.decryptionMaterials.requiredEncryptionContextKeys) != multiset(test.vector.expectedResult.requiredEncryptionContextKeys)) { + print "Error : requiredEncryptionContextKeys does not match.\n", |result.value.decryptionMaterials.requiredEncryptionContextKeys|, + " ", |test.vector.expectedResult.requiredEncryptionContextKeys|, "\n", test.vector.expectedResult.requiredEncryptionContextKeys, + "\n", result.value.decryptionMaterials.requiredEncryptionContextKeys, "\n"; + } + } } print "\nFAILED! <-----------\n"; }