File tree 2 files changed +5
-5
lines changed
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src
2 files changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -359,14 +359,14 @@ module {:options "/functionSyntax:4" } CreateKeys {
359
359
360
360
// get plaintext data key by calling kms::GenerateDataKey
361
361
var activePlaintextMaterial :- KMSKeystoreOperations. GetPlaintextDataKeyViaGenerateDataKey (
362
- branchKeyContext := ecToKMS,
362
+ encryptionContext := ecToKMS,
363
363
kmsConfiguration := kmsConfiguration,
364
364
keyManagerAndStorage := keyManagerAndStorage
365
365
);
366
366
367
367
// get beacon key by calling kms::GenerateDataKey
368
368
var beaconPlaintextMaterial :- KMSKeystoreOperations. GetPlaintextDataKeyViaGenerateDataKey (
369
- branchKeyContext := ecToKMS,
369
+ encryptionContext := ecToKMS,
370
370
kmsConfiguration := kmsConfiguration,
371
371
keyManagerAndStorage := keyManagerAndStorage
372
372
);
@@ -749,7 +749,7 @@ module {:options "/functionSyntax:4" } CreateKeys {
749
749
);
750
750
751
751
var newActivePlaintextMaterial :- KMSKeystoreOperations. GetPlaintextDataKeyViaGenerateDataKey (
752
- branchKeyContext := ecToKMS,
752
+ encryptionContext := ecToKMS,
753
753
kmsConfiguration := kmsConfiguration,
754
754
keyManagerAndStorage := keyManagerAndStorage
755
755
);
Original file line number Diff line number Diff line change @@ -149,7 +149,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
149
149
&& KMS. GenerateDataKeyRequest (
150
150
KeyId := kmsKeyArn,
151
151
NumberOfBytes := Some(32),
152
- EncryptionContext := Some (branchKeyContext ),
152
+ EncryptionContext := Some (encryptionContext ),
153
153
GrantTokens := Some (keyManagerAndStorage.keyManagerStrat.kmsSimple.grantTokens)
154
154
) == kmsGenerateDataKeyEvent. input
155
155
&& kmsGenerateDataKeyEvent. output. Success?
@@ -163,7 +163,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
163
163
var generateDataKeyInput := KMS. GenerateDataKeyRequest (
164
164
KeyId := kmsKeyArn,
165
165
NumberOfBytes := Some(32),
166
- EncryptionContext := Some (branchKeyContext ),
166
+ EncryptionContext := Some (encryptionContext ),
167
167
GrantTokens := Some (keyManagerAndStorage.keyManagerStrat.kmsSimple.grantTokens)
168
168
);
169
169
You can’t perform that action at this time.
0 commit comments