From 3235093f8a27dbdd2f371e2c9636065a4c163f49 Mon Sep 17 00:00:00 2001
From: texastony <5892063+texastony@users.noreply.github.com>
Date: Tue, 21 Jan 2025 14:09:03 -0800
Subject: [PATCH] fix(Mutations): KeyStoreAdmin Exceptions for Mutations when
 KMS Key is Disabled

---
 .../src/MutationErrorRefinement.dfy            | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy
index a6917dd71..25aecf34d 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy
@@ -166,7 +166,23 @@ module {:options "/functionSyntax:4" } MutationErrorRefinement {
               message := "Key Management through an exception."
               + " Mutation is halted. Check access to KMS."
               + "\n" + errorContext);
-
+      }
+    }
+    if (kmsWithMsg) {
+      var hasOriginalArn? := String.HasSubString(kmsErrorMessage?.value, item.KmsArn);
+      var hasTerminalArn? := String.HasSubString(kmsErrorMessage?.value, terminalKmsArn);
+      if (hasOriginalArn?.Some?) {
+        return Types.MutationFromException(
+            message := "Key Management denied access to the original KMS Key."
+            + " Mutation is halted. Check access to KMS ARN: " + item.KmsArn + "."
+            + "\n" + errorContext
+          );
+      } else if (hasTerminalArn?.Some?) {
+        return Types.MutationToException(
+            message := "Key Management denied access to the terminal KMS Key."
+            + " Mutation is halted. Check encrypt access to KMS ARN: " + terminalKmsArn + "."
+            + "\n" + errorContext
+          );
       }
     }
     return Types.KeyStoreAdminException(