Mutations/tony/decrypt encrypt strat

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy

@@ -291,6 +291,111 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
     return Success(reEncryptResponse);
   }
 
+  method VerifyViaDecryptEncryptKey(
+    ciphertext: seq<uint8>,
+    sourceEncryptionContext: Structure.BranchKeyContext,
+    destinationEncryptionContext: Structure.BranchKeyContext,
+    kmsConfiguration: Types.KMSConfiguration,
+    decryptGrantTokens: KMS.GrantTokenList,
+    decryptKmsClient: KMS.IKMSClient
+  )
+    returns (res: Result<KMS.EncryptResponse, KmsError>) 
+    requires
+      && Structure.BranchKeyContext?(sourceEncryptionContext)
+      && Structure.BranchKeyContext?(destinationEncryptionContext)
+    requires AttemptReEncrypt?(sourceEncryptionContext, destinationEncryptionContext)
+    requires AttemptKmsOperation?(kmsConfiguration, destinationEncryptionContext)
+    requires HasKeyId(kmsConfiguration) && KmsArn.ValidKmsArn?(GetKeyId(kmsConfiguration))
+    requires decryptKmsClient.ValidState()
+    modifies decryptKmsClient.Modifies
+    ensures  decryptKmsClient.ValidState()
+
+    ensures
+      res.Success?
+      ==>
+        // Proof for success when we decrypt
+        && KMS.IsValid_CiphertextType(ciphertext)
+        && |decryptKmsClient.History.Decrypt| == |old(decryptKmsClient.History.Decrypt)| + 1
+        && |decryptKmsClient.History.Encrypt| == |old(decryptKmsClient.History.Encrypt)| + 1
+        && var decryptInput := Seq.Last(decryptKmsClient.History.Decrypt).input;
+        && var decryptResponse := Seq.Last(decryptKmsClient.History.Decrypt).output;
+        && var kmsKeyArn := GetKeyId(kmsConfiguration);
+        && KMS.DecryptRequest(
+          CiphertextBlob := ciphertext,
+          EncryptionContext := Some(sourceEncryptionContext),
+          GrantTokens := Some(decryptGrantTokens),
+          KeyId := Some(kmsKeyArn)
+        ) == decryptInput
+        && var decryptResponse := Seq.Last(decryptKmsClient.History.Decrypt).output;
+        && decryptResponse.Success? && decryptResponse.value.Plaintext.Some?
+        && old(decryptKmsClient.History.Decrypt) < decryptKmsClient.History.Decrypt
+        // Proof for success when we encrypt
+        && var encryptInput := Seq.Last(decryptKmsClient.History.Encrypt).input;
+        && var encryptResponse := Seq.Last(decryptKmsClient.History.Encrypt).output;
+        && KMS.EncryptRequest(
+          KeyId := kmsKeyArn,
+          Plaintext := decryptResponse.value.Plaintext.value,
+          EncryptionContext := Some(destinationEncryptionContext),
+          GrantTokens := Some(decryptGrantTokens)
+        ) == encryptInput
+        && old(decryptKmsClient.History.Encrypt) < decryptKmsClient.History.Encrypt
+        && res.value.CiphertextBlob.Some?
+        && res.value.KeyId.Some?
+        && res.value.KeyId.value == kmsKeyArn
+        && KMS.IsValid_CiphertextType(res.value.CiphertextBlob.value)
+        && encryptResponse.Success?
+        && encryptResponse.value == res.value
+  {
+    :- Need(
+      KMS.IsValid_CiphertextType(ciphertext),
+      Types.KeyManagementException(
+        message := "Invalid KMS ciphertext.")
+    );
+
+    var kmsKeyArn := GetKeyId(kmsConfiguration);
+    var kmsDecryptRequest := KMS.DecryptRequest(
+      CiphertextBlob := ciphertext,
+      EncryptionContext := Some(sourceEncryptionContext),
+      GrantTokens := Some(decryptGrantTokens),
+      KeyId := Some(kmsKeyArn)
+    );
+
+    var decryptResponse? := decryptKmsClient.Decrypt(kmsDecryptRequest);
+    var decryptResponse :- decryptResponse?
+    .MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));
+
+    :- Need(
+      && decryptResponse.Plaintext.Some?
+      && decryptResponse.KeyId.Some?
+      && decryptResponse.KeyId.value == kmsKeyArn,
+      Types.KeyManagementException(
+        message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id"
+      ));
+
+    var kmsEncryptRequest := KMS.EncryptRequest(
+      KeyId := kmsKeyArn,
+      Plaintext := decryptResponse.Plaintext.value,
+      EncryptionContext := Some(destinationEncryptionContext),
+      GrantTokens := Some(decryptGrantTokens)
+    );
+
+    var encryptResponse? := decryptKmsClient.Encrypt(kmsEncryptRequest);
+    var encryptResponse :- encryptResponse?
+    .MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));
+
+    :- Need(
+      && encryptResponse.CiphertextBlob.Some?
+      && KMS.IsValid_CiphertextType(encryptResponse.CiphertextBlob.value)
+      && encryptResponse.KeyId.Some?
+      && encryptResponse.KeyId.value == kmsKeyArn,
+      Types.KeyManagementException(
+        message := "Invalid response from AWS KMS Encrypt :: Invalid KMS Key Id"
+    ));
+
+    return Success(encryptResponse);
+  }
+
+
   method MutateViaReEncrypt(
     ciphertext: seq<uint8>,
     sourceEncryptionContext: Structure.BranchKeyContext,

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy

@@ -665,7 +665,7 @@ module {:options "/functionSyntax:4" } Structure {
     ensures BRANCH_KEY_FIELD !in key.EncryptionContext
   {}
 
-  lemma EncryptionContextConstructorsAreCorrect(
+  lemma {:vcs_split_on_every_assert} EncryptionContextConstructorsAreCorrect(
     branchKeyId: string,
     branchKeyVersion: string,
     timestamp: string,

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy

@@ -302,6 +302,38 @@ module Fixtures {
       versionIndex := versionIndex + 1;
     }
   }
+
+  method CreateHappyCaseId2(
+    nameonly id: string,
+    nameonly kmsId: string := keyArn,
+    nameonly physicalName: string := branchKeyStoreName,
+    nameonly logicalName: string := logicalKeyStoreName,
+    nameonly versionCount: nat := 3,
+    nameonly customEC: Types.EncryptionContext := map[UTF8.EncodeAscii("Koda") := UTF8.EncodeAscii("Is a dog.")]
+  )
+    requires DDB.Types.IsValid_TableName(physicalName)
+    requires KMS.Types.IsValid_KeyIdType(kmsId)
+    requires 0 <= versionCount <= 5
+    requires 0 < |customEC| // requires some EC
+  {
+    var keyStore :- expect DefaultKeyStore(kmsId:=kmsId, physicalName:=physicalName, logicalName:=logicalName);
+    assume {:axiom} fresh(keyStore) && fresh(keyStore.Modifies);
+    var input := Types.CreateKeyInput(
+      branchKeyIdentifier := Some(id),
+      encryptionContext := Some(customEC)
+    );
+    var branchKeyId :- expect keyStore.CreateKey(input);
+
+    // If you need a new version
+    var inputV := Types.VersionKeyInput(
+      branchKeyIdentifier := id
+    );
+    var versionIndex := 0;
+    while versionIndex < versionCount {
+      var _ :- expect keyStore.VersionKey(inputV);
+      versionIndex := versionIndex + 1;
+    }
+  }
 
   method GetItemFromDDB(
     nameonly id: string,

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy

@@ -31,6 +31,10 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
   datatype ApplyMutationResult =
     | ContinueMutation(ContinueMutation: MutationToken)
     | CompleteMutation(CompleteMutation: MutationComplete)
+  datatype AwsKmsDecryptEncrypt = | AwsKmsDecryptEncrypt (
+    nameonly decrypt: Option<AwsCryptographyKeyStoreTypes.AwsKms> := Option.None ,
+    nameonly encrypt: Option<AwsCryptographyKeyStoreTypes.AwsKms> := Option.None
+  )
   datatype CreateKeyInput = | CreateKeyInput (
     nameonly Identifier: Option<string> := Option.None ,
     nameonly EncryptionContext: Option<AwsCryptographyKeyStoreTypes.EncryptionContext> := Option.None ,
@@ -64,6 +68,7 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
   )
   datatype KeyManagementStrategy =
     | AwsKmsReEncrypt(AwsKmsReEncrypt: AwsCryptographyKeyStoreTypes.AwsKms)
+    | AwsKmsDecryptEncrypt(AwsKmsDecryptEncrypt: AwsKmsDecryptEncrypt)
   class IKeyStoreAdminClientCallHistory {
     ghost constructor() {
       CreateKey := [];

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy

@@ -140,16 +140,14 @@ union SystemKey {
   trustStorage: TrustStorage
 }
 
-// TODO-Mutations-FF :
-// For GA of Mutations,  of Mutations, only ReEncrypt is allowed
-// structure AwsKmsDecryptEncrypt {
-//   @documentation("The KMS Client (and Grant Tokens) used to Decrypt Branch Key Store Items.")
-//   decrypt: aws.cryptography.keyStore#AwsKms
-//   @documentation(
-//     "The KMS Client (and Grant Tokens) used to Encrypt Branch Key Store Items
-//      and to Generate new Cryptographic Material.")
-//   encrypt: aws.cryptography.keyStore#AwsKms
-// }
+structure AwsKmsDecryptEncrypt {
+  @documentation("The KMS Client (and Grant Tokens) used to Decrypt Branch Key Store Items.")
+  decrypt: aws.cryptography.keyStore#AwsKms
+  @documentation(
+    "The KMS Client (and Grant Tokens) used to Encrypt Branch Key Store Items
+     and to Generate new Cryptographic Material.")
+  encrypt: aws.cryptography.keyStore#AwsKms
+}
 
 @documentation(
   "This configures which Key Management Operations will be used
@@ -160,20 +158,18 @@ union KeyManagementStrategy {
   executed with the provided Grant Tokens and KMS Client.
   This is one request to Key Management, as compared to two.
   But only one set of credentials can be used.")
-  AwsKmsReEncrypt: aws.cryptography.keyStore#AwsKms
-  // TODO-Mutations-FF :
-  // For GA of Mutations, only ReEncrypt is allowed
-  // @documentation(
-  //   "Key Store Items are authenticated and re-wrapped via a Decrypt and then Encrypt request.
-  //    This is two separate requests to Key Management, as compared to one. 
-  //    But the Decrypt requests will use the Decrypt KMS Client (and Grant Tokens),
-  //    while the Encrypt requests will use the Encrypt KMS Client (and Grant Tokens).
-  //    This option affords for different credentials to be utilized,
-  //    based on the operation.
-  //    When Generating new material,
-  //    KMS GenerateDataKeyWithoutPlaintext will be executed against
-  //    the Encrypt option.")
-  // AwsKmsDecryptEncrypt: AwsKmsDecryptEncrypt
+  AwsKmsReEncrypt: aws.cryptography.keyStore#AwsKms,
+  @documentation(
+    "Key Store Items are authenticated and re-wrapped via a Decrypt and then Encrypt request.
+     This is two separate requests to Key Management, as compared to one. 
+     But the Decrypt requests will use the Decrypt KMS Client (and Grant Tokens),
+     while the Encrypt requests will use the Encrypt KMS Client (and Grant Tokens).
+     This option affords for different credentials to be utilized,
+     based on the operation.
+     When Generating new material,
+     KMS GenerateDataKeyWithoutPlaintext will be executed against
+     the Encrypt option.")
+  AwsKmsDecryptEncrypt: AwsKmsDecryptEncrypt
 }
 
 

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/AwsCryptographyKeyStoreAdminOperations.dfy

@@ -135,12 +135,16 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
       case AwsKmsReEncrypt(kms) =>
         var tuple :- ResolveKmsInput(kms, config);
         return Success(KmsUtils.keyManagerStrat.reEncrypt(tuple));
-        // TODO-Mutations-FF :
-        // case AwsKmsDecryptEncrypt(kmsDecryptEncrypt) =>
-        //   // var decrypt :- ResolveKmsInput(kmsDecryptEncrypt.decrypt, config);
-        //   // var encrypt :- ResolveKmsInput(kmsDecryptEncrypt.encrypt, config);
-        //   // return Success(KmsUtils.keyManagerStrat.decryptEncrypt(decrypt, encrypt));
-        //   return Failure(Types.KeyStoreAdminException(message :="BETA :: Only Re Encrypt is supported!!"));
+      case AwsKmsDecryptEncrypt(kmsDecryptEncrypt) =>
+        :- Need(
+          && kmsDecryptEncrypt.decrypt.Some?
+          && kmsDecryptEncrypt.encrypt.Some?,
+          Types.KeyStoreAdminException(message := 
+          "MUST supply KMS clients to both decrypt and encrypt fields in AwsKmsDecryptEncrypt strategy."
+        ));
+        var decrypt :- ResolveKmsInput(kmsDecryptEncrypt.decrypt.value, config);
+        var encrypt :- ResolveKmsInput(kmsDecryptEncrypt.encrypt.value, config);
+        return Success(KmsUtils.keyManagerStrat.decryptEncrypt(decrypt, encrypt));
     }
   }
 
@@ -289,12 +293,16 @@ module AwsCryptographyKeyStoreAdminOperations refines AbstractAwsCryptographyKey
     returns (output: Result<InitializeMutationOutput, Error>)
   {
     var keyManagerStrat :- ResolveStrategy(input.Strategy, config);
-    :- Need(
-      keyManagerStrat.reEncrypt?,
-      Types.KeyStoreAdminException(message :="Only ReEncrypt is supported at this time.")
-    );
     // See Smithy-Dafny : https://github.com/smithy-lang/smithy-dafny/pull/543
-    assume {:axiom} keyManagerStrat.reEncrypt.kmsClient.Modifies < MutationLie();
+
+    if keyManagerStrat.reEncrypt? {
+      assume {:axiom} keyManagerStrat.reEncrypt.kmsClient.Modifies < MutationLie();
+    }
+
+    if keyManagerStrat.decryptEncrypt? {
+      assume {:axiom} keyManagerStrat.decrypt.kmsClient.Modifies < MutationLie();
+      assume {:axiom} keyManagerStrat.encrypt.kmsClient.Modifies < MutationLie();
+    }
 
     var internalInput := Mutations.InternalInitializeMutationInput(
       Identifier := input.Identifier,